Conflict-Driven SAT Solving using XOR-OR-AND Normal Forms

Abstract

Background: Classical solvers for Boolean polynomial systems are usually based on the Conjunctive Normal Form (CNF) and the resolution calculus, or on the algebraic normal form (ANF) and the polynomial calculus, i.e., on Gröbner basis methods. Here we develop a new solver which is based on the XOR-OR-AND normal form (XNF) and the XLIN proof system. XNF formulae allow compact encodings of XOR-rich problems, which, for instance, occur naturally in cryptography. Objectives: The paper has the following goals: lay a solid complexity-theoretic foundation for the new propositional logic proof system XLIN, devise XLIN-based conflict learning methods for formulae in XNF, create a variant of this framework optimized for practical efficiency, implement it in an actual solver called Xorricane, and finally apply this solver to benchmark suites consisting of random examples and cryptographic examples to prove its viability. Methods: As a first step, we show that the new propositional logic proof system XLIN is polynomially equivalent equivalent to the well-studied proof systems RES(⊕) and SRES. It follows that there is an exponential separation between XLIN and the CNF-based resolution proof system RES. In the next step, we devise XLIN-based conflict-learning methods for formulae in XNF which are analogous to the CDCL methods of classical SAT solvers. Using Gaußian Constraint Propagation and a suitable version of conflict analysis, we obtain a conflict-driven framework CDXCL for XNF SAT-solving. To ensure practical efficiency, we also present a variant, called CDXCLlite, which uses a weaker propagation mechanism but retains the same learning method. Results: These theoretical advances result in Xorricane, an implementation of the latter XNF SAT-solving framework featuring novel lazy data structures. This implementation is compared to state-of-the-art algebraic and logic solving approaches on random and cryptographic benchmark suites. Although it still lacks several optimizations, it performs well on the benchmark problems and matches or outperforms modern CNF and CNF-XOR based SAT-solvers for XOR-rich problem instances. Conclusions: Solving Boolean polynomial systems, or equivalently, SAT-solving, based on the XNF and the XLIN proof system outperforms classical methods not only theoretically, but based on the new conflict-driven XNF clause learning methods developed here, it is possible to implement an XNF solver with good practical efficiency. The advantage of XNF-based SAT-solving is strongest for XOR-rich examples such as the ones derived from cryptographic attacks.