DRAT proofs for XOR reasoning

DOI10.1007/978-3-319-48758-8_27MaRDI QIDQ2835888zbMATH OpenOpenAlexFDO

Authors Tobias Philipp, Adrián Rebola-Pardo

Publication date 30 November 2016

Published in Logics in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL http://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-3026

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Conflict-driven XOR-clause learning
• Extended resolution simulates \({\mathsf{DRAT}}\)
• Towards a Semantics of Unsatisfiability Proofs with Inprocessing
• DRAT-based bit-vector proofs in CVC4
• A flexible proof format for SAT solver-elaborator communication

Cites work

• scientific article; zbMATH DE number 5139161 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• A machine program for theorem-proving
• Algebraic Cryptanalysis of the Data Encryption Standard
• Compositional propositional proofs
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Expressing symmetry breaking in DRAT proofs
• Extended Resolution Proofs for Conjoining BDDs
• Graph-Based Algorithms for Boolean Function Manipulation
• Inprocessing rules
• On SAT representations of XOR constraints
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• SpyBug: automated bug detection in the configuration space of SAT solvers
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

Cited in

(9)

• A flexible proof format for SAT solver-elaborator communication
• Non-clausal redundancy properties
• Clausal congruence closure
• The relative strength of \#SAT proof systems
• Extended resolution simulates \({\mathsf{DRAT}}\)
• Inconsistency proofs for ASP: the ASP-DRUPE format
• A theory of satisfiability-preserving proofs in SAT solving
• scientific article; zbMATH DE number 1696817 (Why is no real title available?)
• Conflict-driven XOR-clause learning

Describes a project that uses

Uses Software

• Lingeling
• Spybug
• Coprocessor
• DRAT-trim
• CryptoMiniSat
• MiniSat

This page was built for publication: DRAT proofs for XOR reasoning

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