Simulating Parity Reasoning (extended version)?

Abstract. Propositional satisfiability (SAT) solvers, which typically operate us-ing conjunctive normal form (CNF), have been successfully applied in many do-mains. However, in some application areas such as circuit verification, bounded model checking, and logical cryptanalysis, instances can have many parity (xor) constraints which may not be handled efficiently if translated to CNF. Thus, ex-tensions to the CNF-driven search with various parity reasoning engines rang-ing from equivalence reasoning to incremental Gaussian elimination have been proposed. This paper studies how stronger parity reasoning techniques in the DPLL(XOR) framework can be simulated by simpler systems: resolution, unit propagation, and parity explanations. Such simulations are interesting, for exam-ple, for developing the next generation SAT solvers capable of handling parity constraints efficiently.