Extended resolution simulates DRAT

DOI10.1007/978-3-319-94205-6_34zbMATH Open1441.68278OpenAlexW2811000330MaRDI QIDQ1799112FDOQ1799112

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

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

Mathematics Subject Classification ID

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

Cited In (13)

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

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)