Expressing symmetry breaking in DRAT proofs
From MaRDI portal
Publication:3454124
DOI10.1007/978-3-319-21401-6_40zbMATH Open1465.68285OpenAlexW2236514805MaRDI QIDQ3454124FDOQ3454124
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
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
- Theory and Applications of Satisfiability Testing
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Inprocessing rules
- Automated testing and debugging of SAT and QBF solvers
- Small Ramsey numbers
- Blocked clause elimination
- Sorting nine inputs requires twenty-five comparisons
- On a generalization of extended resolution
- The van der Waerden NumberW(2, 6) Is 1132
- Verifying Refutations with Extended Resolution
- A SAT attack on the Erdős discrepancy conjecture
- Banishing the rule of substitution for functional variables
- Simple second-order languages for which unification is undecidable
- Mechanical verification of SAT refutations with extended resolution
- Dynamic Symmetry Breaking by Simulating Zykov Contraction
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
- The resolution of Keller's conjecture
- The resolution of Keller's conjecture
- DRAT proofs for XOR reasoning
- 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
Uses Software
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)
