An extensible circuit-based SAT solver

摘要

In satisfiability (SAT) the task is to determine whether a propositional formula can evaluate to true under some assignment to its variables. The formula is either represented in CNF or in circuit form. Solvers are available for both representations with comparable performance. CNF-based approach, being simpler in encoding and solver design, is more popular, in which a circuit is translated into CNF and then solved. Translation to CNF, however, increases the size of the encoding, and is not practical for some constraints such as the cardinality constraint. Circuit-based approach lacks simplicity of implementation; however, circuit representation remains compact in size and also captures problem structure where domain-specific knowledge can be exploited. An important application of SAT solving is in the area of model-based diagnosis. Our contribution in this paper is twofold enhancing the state-of-the-art in SAT solving as well as model-based diagnosis. To simplify and encourage development in circuit-based approach, we propose a new solver which can be extended with minimal effort. The solver which has been built using object-oriented paradigm allows adding a new gate by simply inheriting from existing classes and overriding some functions, hiding great deal of complexity. Then, we demonstrate its effectiveness on the problem of computing minimum-cardinality diagnoses using ISCAS-85 circuit benchmarks. We show that the new solver can solve 28 more (out of 1000) cases than its CNF-based counterpart.