Simulating parity reasoning

DOI10.1007/978-3-642-45221-5_38MaRDI QIDQ2870154zbMATH OpenOpenAlexFDO

Authors Tero Laitinen, Tommi Junttila, Ilkka Niemelä

Publication date 17 January 2014

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1311.4289

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

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.

Recommendations

• Extending clause learning DPLL with parity reasoning
• Conflict-driven XOR-clause learning
• Towards an efficient library for SAT: A manifesto
• Propositional SAT solving
• scientific article; zbMATH DE number 5510692

Cited in

(2)

• Simulating without Negation
• Extending clause learning DPLL with parity reasoning

This page was built for publication: Simulating parity reasoning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2870154)