Simulating Parity Reasoning (extended version)

TL;DR

This paper explores how advanced parity reasoning techniques in SAT solving, especially within the DPLL(XOR) framework, can be simulated using simpler methods like resolution and unit propagation, aiming to improve solver efficiency.

Contribution

It demonstrates that stronger parity reasoning methods can be effectively simulated by simpler systems, informing the development of more efficient SAT solvers for parity constraints.

Findings

Simulation of parity reasoning techniques using resolution and unit propagation

Potential for developing next-generation SAT solvers with improved parity handling

Insights into the relationship between complex and simple reasoning systems

Abstract

Propositional satisfiability (SAT) solvers, which typically operate using conjunctive normal form (CNF), have been successfully applied in many domains. 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, extensions to the CNF-driven search with various parity reasoning engines ranging 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 example, for developing the next generation SAT solvers capable of handling parity constraints efficiently.