2013/11/18 by Tero Laitinen, Laitinen, Tero, Tommi Junttila +3
Computer Science · Engineering · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Radiation Effects in Electronics #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.1311.4289
openalex publication_date 2013/11/18 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.