Conflict-Driven XOR-Clause Learning (extended version)

TL;DR

This paper introduces new methods for integrating XOR reasoning into conflict-driven clause learning SAT solvers, enabling more efficient solving of formulas with XOR constraints, especially in cryptanalysis applications.

Contribution

It develops techniques for analyzing XOR reasoning derivations, producing smaller explanations and learning new XOR-clauses, improving proof efficiency in DPLL(XOR) frameworks.

Findings

Shorter unsatisfiability proofs for complex XOR formulas

Enhanced XOR reasoning reduces solving complexity

Effective in cryptanalysis problem instances

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.