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

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

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

(20)

• On a generalization of extended resolution
• Flexible proof production in an industrial-strength SMT solver
• DRAT proofs, propagation redundancy, and extended resolution
• Simulating strong practical proof systems with extended resolution
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
• Strong extension-free proof systems
• What a difference a variable makes
• Extended resolution simulates binary decision diagrams
• DRAT proofs for XOR reasoning
• DRAT and propagation redundancy proofs without new variables
• Inconsistency proofs for ASP: the ASP-DRUPE format
• The proof complexity of SMT solvers
• Certified dominance and symmetry breaking for combinatorial optimisation
• Trusted scalable SAT solving with on-the-fly LRAT checking
• The strength of the dominance rule
• MaxSAT resolution with inclusion redundancy
• The relative strength of \#SAT proof systems
• RAT elimination
• Sometimes hoarding is harder than cleaning: NP-hardness of maximum blocked-clause addition
• Circuits, proofs and propositional model counting

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)