On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers

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

zbMATH Keywords

SAT solvingproof formatdynamic symmetry handlingUNSAT certificate

Mathematics Subject Classification ID

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)

On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers

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