Scalable algorithms for Boolean satisfiability enabled by problem structure.

The last few years have seen an increasing interest in Boolean Satisfiability (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 applications. Nevertheless, a number of practical SAT instances remain difficult to solve and continue to defy even the best available SAT solvers. 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 of hard SAT instances and show how to utilize these properties to produce SAT algorithms that can scale with the increasing complexity of today's SAT instances. 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 symmetry-breaking predicates to the SAT instance that significantly prune the search space. Second, we expose sparsity in SAT instances and show how to utilize that knowledge to efficiently identify orderings of variables that intelligently guide the decision engines in SAT solvers. Third, we observe that CNF constraints in a SAT instance exhibit self-similarity. In general, such constraints are explicitly represented which may exhaust available computer memory resulting in aborted runs. We address this problem by developing a backtrack search algorithm that implicitly represents the constraints using zero-suppressed binary decision diagrams. 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. We have validated these claims and showed that utilizing structure can substantially speed up the search process and reduce the memory requirements for many SAT instances.Ph.D.Applied SciencesComputer scienceElectrical engineeringUniversity of Michigan, Horace H. Rackham School of Graduate Studieshttp://deepblue.lib.umich.edu/bitstream/2027.42/123338/2/3079402.pd