Expressing Symmetry Breaking in DRAT Proofs

DOI10.1007/978-3-319-21401-6_40zbMath1465.68285OpenAlexW2236514805MaRDI QIDQ3454124

Warren A. jun. Hunt, Marijn J. H. Heule, 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)

Related Items (11)

On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers ⋮ Solution validation and extraction for QBF preprocessing ⋮ Inconsistency Proofs for ASP: The ASP - DRUPE Format ⋮ Preprocessing of propagation redundant clauses ⋮ Functional Encryption for Inner Product with Full Function Privacy ⋮ The resolution of Keller's conjecture ⋮ Strong extension-free proof systems ⋮ Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer ⋮ DRAT Proofs for XOR Reasoning ⋮ The resolution of Keller's conjecture ⋮ Preprocessing of propagation redundant clauses

Uses Software

• ACL2
• MiniSat
• PicoSAT
• DRAT-trim

Cites Work

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

This page was built for publication: Expressing Symmetry Breaking in DRAT Proofs