Abstract:

Boolean Satisfiability (SAT) is probably one of the most well studied combinatorial decision/optimization problems. Researchers have devoted significant effort to developing efficient SAT solvers. SAT has seen many successful applications in various fields such as Electronic Design Automation (EDA) and Artificial Intelligence (AI). For decades, EDA, and in particular synthesis and verification, has been one of the major drivers for SAT research. This thesis presents the following research contributions to improve both the capability and applicability of contemporary SAT solvers.

The partial maximum Boolean satisfiability problem (PM-SAT). PM-SAT is an extension of the SAT problem. In this extension certain clauses are marked as relaxable and the rest are non-relaxable. The objective is to find a variable assignment that satisfies all non-relaxable clauses together with the maximum number of relaxable ones. This thesis proposes a novel diagnosis based algorithm that iteratively analyzes the UNSAT core of the current SAT instance and eliminates the core through a modification of the problem instance by adding relaxation variables. This approach is compared with alternative solutions to this problem.

The minimum cost Boolean satisfiability problem (MinCostSAT). MinCostSAT is an extension of the SAT problem with a cost function for each satisfying assignment. The goal is to find the assignment that satisfies the problem instance with minimum cost or determine that none exists. This thesis first points out the challenges in using existing SAT solvers for MinCostSAT and then presents techniques to overcome these challenges. The resulting solver MinCostChaff shows an order of magnitude improvement over several current best known branch-and-bound solvers for a large number of instances derived from diverse applications such as Minimum Test Pattern Generation, Bounded Model Checking, Graph Coloring and Planning.

Exploiting circuit observability don't cares in Boolean satisfiability. A given circuit signal, under certain conditions, may not be observable at the circuit outputs. These conditions are known as circuit observability don't care conditions (Cir-ODC) for this signal. This thesis proposes a new approach to take such don't care information from a logic circuit into consideration in a SAT solver that uses the Conjunctive Normal Form (CNF) representation for the SAT instance. It does so by adding certain don't care literals to clauses in the CNF representation. These don't care literals are treated differently at different times during the solution process, much like don't cares in logic synthesis. The major merit of this scheme, unlike other recently proposed techniques, is that the solver can continue to use this don't care information during the learning process, which is an important part of contemporary SAT solvers.

Extracting logic circuit structure from conjunctive normal form descriptions. In this part an efficient algorithm (CNF2CKT) is developed and tested for extracting circuit information from CNF instances using the reverse of the Tseitin transformation. One application of this is that the Cir-ODC techniques can be applied to non-circuit generated instances. CNF2CKT is optimal in the sense that it extracts a maximum acyclic combinational circuit from any given CNF by reversing the Tseitin transformation and using the logic gates pre-specified in a given library. The extracted circuit structure is valuable in various ways, particularly when the CNF is not encoded from the circuit, or the circuit description is not readily available. As an example, we show that the extracted circuit structure can be used to derive Circuit Observability Don't Cares for speeding up CNF-based SAT.