Expressing Symmetry Breaking in DRAT Proofs
From MaRDI portal
Publication:3454124
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
Related Items (13)
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 ⋮ Certified dominance and symmetry breaking for combinatorial optimisation ⋮ Functional Encryption for Inner Product with Full Function Privacy ⋮ Without loss of satisfaction ⋮ 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
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
