Expressing symmetry breaking in DRAT proofs

DOI10.1007/978-3-319-21401-6_40MaRDI QIDQ3454124zbMATH OpenOpenAlexFDO

Authors Marijn J. H. Heule, Warren A. jun. Hunt, Nathan D. Wetzler

Publication date 2 December 2015

Published in Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-21401-6_40

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Improved static symmetry breaking for SAT
• CDCLSym: introducing effective symmetry breaking in SAT solving
• Symmetry Breaking for Maximum Satisfiability
• On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers
• \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver

Cites work

• A SAT attack on the Erdős discrepancy conjecture
• Automated testing and debugging of SAT and QBF solvers
• Banishing the rule of substitution for functional variables
• Blocked clause elimination
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Dynamic Symmetry Breaking by Simulating Zykov Contraction
• Inprocessing rules
• Mechanical verification of SAT refutations with extended resolution
• On a generalization of extended resolution
• Simple second-order languages for which unification is undecidable
• Small Ramsey numbers
• Sorting nine inputs requires twenty-five comparisons
• The van der Waerden NumberW(2, 6) Is 1132
• Theory and Applications of Satisfiability Testing
• Verifying Refutations with Extended Resolution

Cited in

(16)

• On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• Functional encryption for inner product with full function privacy
• Improved static symmetry breaking for SAT
• Preprocessing of propagation redundant clauses
• Preprocessing of propagation redundant clauses
• Without loss of satisfaction
• Breaking symmetries with lex implications
• Speeding up SAT solver by exploring CNF symmetries: Revisited
• DRAT proofs for XOR reasoning
• The resolution of Keller's conjecture
• The resolution of Keller's conjecture
• Inconsistency proofs for ASP: the ASP-DRUPE format
• Strong extension-free proof systems
• Solution validation and extraction for QBF preprocessing
• Certified dominance and symmetry breaking for combinatorial optimisation

Describes a project that uses

Uses Software

• DRAT-trim
• PicoSAT
• MiniSat
• ACL2

This page was built for publication: Expressing symmetry breaking in DRAT proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3454124)