DRAT Proofs for XOR Reasoning

DOI10.1007/978-3-319-48758-8_27zbMath1483.68357OpenAlexW2545814918MaRDI QIDQ2835888

Adrián Rebola-Pardo, Tobias Philipp

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)

Related Items

Inconsistency Proofs for ASP: The ASP - DRUPE Format, Non-clausal redundancy properties

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers
• Inprocessing Rules
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Extended Resolution Proofs for Conjoining BDDs
• Expressing Symmetry Breaking in DRAT Proofs
• Compositional Propositional Proofs
• Graph-Based Algorithms for Boolean Function Manipulation
• Theory and Applications of Satisfiability Testing
• On SAT Representations of XOR Constraints
• Algebraic Cryptanalysis of the Data Encryption Standard
• A machine program for theorem-proving
• Theory and Applications of Satisfiability Testing