Verifying Refutations with Extended Resolution

DOI10.1007/978-3-642-38574-2_24MaRDI QIDQ4928451zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

(30)

• Efficient, verified checking of propositional proofs
• A flexible proof format for SAT solver-elaborator communication
• Generating extended resolution proofs with a BDD-based SAT solver
• Random resolution refutations
• Solution validation and extraction for QBF preprocessing
• QMaxSATpb: a certified MaxSAT solver
• Super-blocked clauses
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• Expressing symmetry breaking in DRAT proofs
• Local redundancy in SAT: generalizations of blocked clauses
• The complexity of debate checking
• DRAT and propagation redundancy proofs without new variables
• A flexible proof format for SAT solver-elaborator communication
• Inconsistency proofs for ASP: the ASP-DRUPE format
• Mechanical verification of SAT refutations with extended resolution
• Generating Extended Resolution Proofs with a BDD-Based SAT Solver
• Never trust your solver: certification for SAT and QBF
• Certified dominance and symmetry breaking for combinatorial optimisation
• Certified Core-Guided MaxSAT Solving
• Clausal proofs for pseudo-Boolean reasoning
• Certified SAT solving with GPU accelerated inprocessing
• MaxSAT resolution with inclusion redundancy
• The relative strength of \#SAT proof systems
• Runtime vs. extracted proof size: an exponential gap for CDCL on QBFs
• Producing and verifying extremely large propositional refutations
• RAT elimination
• Certified MaxSAT preprocessing
• The relative strength of \#SAT proof systems
• On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers
• Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs

Describes a project that uses

Uses Software

• ACL2

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)