Extending SAT solver with parity constraints

Abstract

Current methods for solving Boolean satisfiability problem (SAT) are scalable enough to solve discrete nonlinear problems involving hundreds of thousands of variables. However, modern SAT solvers scale poorly with problems involving parity constraints (linear equations modulo 2). Gaussian elimination can be used to solve a system of linear equation effectively but it cannot be applied as such when the problem description also contains nonlinear constraints. A SAT solver typically reads the problem description in conjunctive normal form (CNF). Representing parity constraints in CNF results in an inefficient encoding which partly makes solving the problem harder. Also, the deduction methods used in SAT solvers are not efficient when solving problems involving parity constraints.

This report develops an efficient xor-reasoning module for deciding the satisfiability of a conjunction of parity constraints and studies alternative ways to integrate the xor-reasoning module into a modern conflict-driven clause learning SAT solver. The novelty of the approach is the combination of conflict-driven clause learning techniques (CDCL) with equivalence reasoning enhancing deduction capabilities of CDCL SAT solvers beyond unit propagation on the CNF formula. The presented proof system and the abstract model for computing clausal explanations for inconsistent valuations of variables allow for different possible implementations. Key design principles along with alternative ways to compute clausal explanations and to integrate the xor-reasoning module into a SAT solver are presented, analyzed, and compared. We have integrated the xor-reasoning module into a state-of-the-art CDCL SAT solver, minisat. The applicability of the hybrid approach is evaluated experimentally and compared with a number of modern SAT solvers on three challenging benchmarks: randomly generated regular linear problems, a known keystream attack on the stream cipher Trivium, and a known plaintext attack on the block cipher DES. The results are promising: the number of heuristics decisions needed typically decreases without causing unbearable computational overhead. Larger problem instances may even be solved faster by minisat with the xor-reasoning module than by the unmodified version.