Abstract
Propositional conflictdriven clauselearning (CDCL) satisfy ability (SAT) solvers have been successfully applied in a number of industrial domains. In some application areas such as circuit verification, bounded model checking, logical cryptanalysis, and approximate model counting, some requirements can be succinctly captured with parity (xor) constraints. However, satisfy ability solvers that typically operate in conjunctive normal form (CNF) may perform poorly with straightforward translation of parity constraints to CNF. This work studies how CDCL SAT solvers can be enhanced to handle problems with parity constraints using the recently introduced DPLL (XOR) framework where the SAT solver is coupled with a parity constraint solver module. Different xordeduction systems ranging from plain unit propagation through equivalence reasoning to complete incremental GaussJordan elimination are presented. Techniques to analyze xordeduction system derivations are developed, allowing one to obtain smaller clausal explanations for implied literals and also to learn new parity constraints in the conflict analysis process. It is proven that these techniques can be used to simulate a complete xordeduction system on a restricted class of instances and allow very short unsatisfiability proofs for some formulas whose CNF translations are hard for resolution. Fast approximating tests to detect whether unit propagation or equivalence reasoning is enough to deduce all implied literals are presented. Methods to decompose sets of parity constraints into sub problems that can be handled separately are developed. The decomposition methods can greatly reduce the size of parity constraint matrices when using GaussJordan elimination on dense matrices and allow one to choose appropriate xordeduction system for each sub problem. Efficient translations to simulate equivalence reasoning and stronger parity reasoning are developed. It is shown that equivalence reasoning can be simulated by adding a polynomial amount of redundant parity constraints to the problem, but without using additional variables, an exponential number of parity constraints are needed in the worst case. It is proven that resolution simulates equivalence reasoning efficiently. The presented techniques are experimentally evaluated on a variety of challenging problems originating from a number of encryption ciphers and from SAT Competition benchmark instances.
Translated title of the contribution  Lauselogiikan toteutuvuustarkistimen laajentaminen pariteettipäättelyllä 

Original language  English 
Qualification  Doctor's degree 
Awarding Institution 

Supervisors/Advisors 

Publisher  
Print ISBNs  9789526059440 
Electronic ISBNs  9789526059457 
Publication status  Published  2014 
MoE publication type  G5 Doctoral dissertation (article) 
Keywords
 propositional satisfiability
 parity reasoning
Fingerprint Dive into the research topics of 'Extending SAT Solver with Parity Reasoning'. Together they form a unique fingerprint.
Cite this
Laitinen, T. (2014). Extending SAT Solver with Parity Reasoning. Aalto University. http://urn.fi/URN:ISBN:9789526059457