Extending Clause Learning SAT Solvers with Complete Parity Reasoning (extended version)

TL;DR

This paper enhances SAT solvers with complete parity reasoning capabilities by introducing a new xor-reasoning module and matrix decomposition techniques, improving efficiency in solving combined SAT and parity constraint problems.

Contribution

It presents a novel xor-reasoning module using incremental Gauss-Jordan elimination and a matrix decomposition method to efficiently handle parity constraints in SAT solving.

Findings

Improved deduction of implied literals in SAT problems with parity constraints

Reduced size of parity matrices through decomposition techniques

Experimental validation shows enhanced solver performance

Abstract

Instances of logical cryptanalysis, circuit verification, and bounded model checking can often be succinctly represented as a combined satisfiability (SAT) problem where an instance is a combination of traditional clauses and parity constraints. This paper studies how such combined problems can be efficiently solved by augmenting a modern SAT solver with an xor-reasoning module in the DPLL(XOR) framework. A new xor-reasoning module that deduces all possible implied literals using incremental Gauss-Jordan elimination is presented. A decomposition technique that can greatly reduce the size of parity constraint matrices while allowing still to deduce all implied literals is presented. It is shown how to eliminate variables occuring only in parity constraints while preserving the decomposition. The proposed techniques are evaluated experimentally.