Verifying Refutations with Extended Resolution
From MaRDI portal
Publication:4928451
DOI10.1007/978-3-642-38574-2_24zbMATH Open1381.68270OpenAlexW2215982992MaRDI QIDQ4928451FDOQ4928451
Authors: Marijn J. H. Heule, Warren A. jun. Hunt, Nathan D. Wetzler
Publication date: 14 June 2013
Published in: Automated Deduction – CADE-24 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-38574-2_24
Recommendations
- Mechanical verification of SAT refutations with extended resolution
- Resolution lower bounds for refutation statements
- Producing and verifying extremely large propositional refutations
- Verification in argument-incomplete argumentation frameworks
- scientific article; zbMATH DE number 1948189
- Verification in incomplete argumentation frameworks
- Extending resolution to resolution logics
- Random resolution refutations
- Random resolution refutations
Cited In (24)
- Local redundancy in SAT: generalizations of blocked clauses
- On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- Certified SAT solving with GPU accelerated inprocessing
- Producing and verifying extremely large propositional refutations
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Expressing symmetry breaking in DRAT proofs
- Title not available (Why is that?)
- Title not available (Why is that?)
- A flexible proof format for SAT solver-elaborator communication
- Generating extended resolution proofs with a BDD-based SAT solver
- Generating Extended Resolution Proofs with a BDD-Based SAT Solver
- Super-blocked clauses
- Inconsistency proofs for ASP: the ASP-DRUPE format
- Certified Core-Guided MaxSAT Solving
- Solution validation and extraction for QBF preprocessing
- The complexity of debate checking
- Efficient, verified checking of propositional proofs
- Mechanical verification of SAT refutations with extended resolution
- QMaxSATpb: a certified MaxSAT solver
- Clausal proofs for pseudo-Boolean reasoning
- Random resolution refutations
- Certified dominance and symmetry breaking for combinatorial optimisation
- Never trust your solver: certification for SAT and QBF
Uses Software
This page was built for publication: Verifying Refutations with Extended Resolution
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4928451)