DRAT proofs for XOR reasoning

DOI10.1007/978-3-319-48758-8_27zbMATH Open1483.68357OpenAlexW2545814918MaRDI QIDQ2835888FDOQ2835888

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

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (7)

• A flexible proof format for SAT solver-elaborator communication
• Non-clausal redundancy properties
• Extended resolution simulates \({\mathsf{DRAT}}\)
• Inconsistency proofs for ASP: the ASP-DRUPE format
• A theory of satisfiability-preserving proofs in SAT solving
• Title not available (Why is that?)
• Conflict-driven XOR-clause learning

Uses Software

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

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)