Conflict-driven XOR-clause learning

DOI10.1007/978-3-642-31612-8_29MaRDI QIDQ2843342zbMATH OpenOpenAlexFDO

Authors Tero Laitinen, Tommi Junttila, Ilkka Niemelä

Publication date 12 August 2013

Published in Theory and Applications of Satisfiability Testing – SAT 2012 (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1407.6571

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20) Cryptography (94A60)

Abstract: Modern conflict-driven clause learning (CDCL) SAT solvers are very good in solving conjunctive normal form (CNF) formulas. However, some application problems involve lots of parity (xor) constraints which are not necessarily efficiently handled if translated into CNF. This paper studies solving CNF formulas augmented with xor-clauses in the DPLL(XOR) framework where a CDCL SAT solver is coupled with a separate xor-reasoning module. New techniques for analyzing xor-reasoning derivations are developed, allowing one to obtain smaller CNF clausal explanations for xor-implied literals and also to derive and learn new xor-clauses. It is proven that these new techniques allow very short unsatisfiability proofs for some formulas whose CNF translations do not have polynomial size resolution proofs, even when a very simple xor-reasoning module capable only of unit propagation is applied. The efficiency of the proposed techniques is evaluated on a set of challenging logical cryptanalysis instances.

Recommendations

• Extending clause learning DPLL with parity reasoning
• DRAT proofs for XOR reasoning
• On the power of clause-learning SAT solvers as resolution engines
• Learning from conflicts in propositional satisfiability
• What we can learn from conflicts in propositional satisfiability

Cited in

(13)

• Logical cryptanalysis with WDSat
• A game characterisation of tree-like Q-resolution size
• scientific article; zbMATH DE number 1696817 (Why is no real title available?)
• DRAT proofs for XOR reasoning
• Simulating parity reasoning
• Extending clause learning DPLL with parity reasoning
• Clause-learning for modular systems
• A Generalized Framework for Conflict Analysis
• Deciding floating-point logic with abstract conflict driven clause learning
• On SAT representations of XOR constraints
• Theory and Applications of Satisfiability Testing
• SAT solving using XOR-OR-AND normal forms.
• SAT, gadgets, Max2XOR, and quantum annealers

This page was built for publication: Conflict-driven XOR-clause learning

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