Scalable Algorithms for Boolean Satisfiability Enabled by Problem Structure

Boolean Satisfiability (SAT) is a core problem in mathematical logic and computational theory. The last few years have seen an increasing interest in SAT, spurred in part by the recent availability of powerful SAT solvers that are sufficiently efficient and robust to deal with large-scale SAT problem instances. This has led to the successful deployment of SAT technology into diverse electronic design automation (EDA) applications such as verification, testing, and routing. Nevertheless, a number of practical SAT instances remain difficult to solve and continue to defy even the best available SAT solvers. The overall goal of our research is to develop efficient SAT algorithms that can scale with the increasing
complexity of today's SAT instances.
While the general SAT problem is intractable, our premise in this thesis is that SAT instances arising from real-world applications possess an innate structure that, once uncovered, can drastically simplify the instance. Motivated by this observation, we develop robust methods for detecting various structural properties, such as symmetry, sparsity, and self-similarity, of hard SAT instances and show how to utilize these properties to produce scalable SAT algorithms.
First, we show how to identify and break syntactic symmetries in SAT instances expressed in conjunctive normal form (CNF). The symmetries are broken by adding appropriate symmetry-breaking predicates (SBPs) to the SAT instance that significantly prune the search space. In essence, SBPs act as a filter that confines the search to non-symmetric regions of the space without affecting the satisfiability of the instance.
Abstract cont.. Second, we expose sparsity in SAT instances and show how to utilize that knowledge to efficiently identify orderings of variables which reduce the CNF formula's cutwidth and intelligently guide the decision engines in SAT solvers. Such orderings place "connected" variables and constraints next to each other thus minimizing the amount of backtracking and speeding up search.
Third, we observe that CNF constraints in a SAT instance exhibit self-similarity. In general, such constraints are explicitly represented and manipulated which may exhaust available computer memory resulting in aborted runs. We address this problem by developing a backtrack search algorithm that implicitly represents the CNF constraints using zero-suppressed binary decision diagrams (ZBDDs). This allows the processing of sets of, rather than single, constraints.
Finally, we observe that real-world SAT instances typically consist of specific structured CNF constraints, such as counting constraints, that can be efficiently encoded using pseudo-Boolean (PB) constraints. The use of PB constraints extends the application of SAT solvers to handle Boolean decision and optimization problems. We develop effective techniques for handling PB constraints, either by converting them to a compact set of equivalent CNF constraints, or by efficiently extending SAT solvers to handle PB constraints directly. We also describe various efficient approaches for handling Boolean optimization problems in SAT solvers.
We have validated these claims and showed that utilizing structure can substantially speed up the search process and reduce the memory requirements for many benchmark instances.