On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers
From MaRDI portal
Publication:823775
DOI10.1007/s10601-020-09313-2OpenAlexW3096659223MaRDI QIDQ823775
Rodrigue Konan Tchinda, Clémentin Tayou Djamegni
Publication date: 16 December 2021
Published in: Constraints (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10601-020-09313-2
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- SAT race 2015
- Short proofs for tricky formulas
- On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers
- Efficient SAT-based bounded model checking for software verification
- The intractability of resolution
- Symmetric explanation learning: effective dynamic symmetry handling for SAT
- On a generalization of extended resolution
- The symmetry rule in propositional logic
- Improved Static Symmetry Breaking for SAT
- Inprocessing Rules
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Extended Resolution Proofs for Conjoining BDDs
- Expressing Symmetry Breaking in DRAT Proofs
- Verifying Refutations with Extended Resolution
- SATO: An efficient propositional prover
- Theory and Applications of Satisfiability Testing
- The complexity of theorem-proving procedures
- The Number of Transitivity Sets of Boolean Functions
- Bounded model checking using satisfiability solving
This page was built for publication: On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers
