Extended resolution simulates DRAT

DOI10.1007/978-3-319-94205-6_34MaRDI QIDQ1799112zbMATH OpenOpenAlexFDO

Authors Benjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule

Publication date 18 October 2018

Full work available at URL https://doi.org/10.1007/978-3-319-94205-6_34

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Recommendations

• Simulating strong practical proof systems with extended resolution
• DRAT proofs, propagation redundancy, and extended resolution
• Extended resolution simulates binary decision diagrams
• What a difference a variable makes
• DRAT proofs for XOR reasoning

Cited in

(13)

• Certified dominance and symmetry breaking for combinatorial optimisation
• On a generalization of extended resolution
• DRAT proofs, propagation redundancy, and extended resolution
• Simulating strong practical proof systems with extended resolution
• Extended resolution simulates binary decision diagrams
• Strong extension-free proof systems
• What a difference a variable makes
• Flexible proof production in an industrial-strength SMT solver
• The proof complexity of SMT solvers
• Inconsistency proofs for ASP: the ASP-DRUPE format
• DRAT proofs for XOR reasoning
• scientific article; zbMATH DE number 7350778 (Why is no real title available?)
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML

Describes a project that uses

Uses Software

• DRAT-trim

This page was built for publication: Extended resolution simulates \({\mathsf{DRAT}}\)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1799112)