Scalability for SAT-based combinatorial problem solving

Abstract

SAT solvers determine whether a given propositional formula is satisfiable. Today’s highly engineered SAT solvers can determine the satisfiability of huge formulas with millions of constraints and thousands of variables. Further, stat- ing other combinatorial problems in terms of propositional satisfiability allows the use of this great SAT-solving performance for a large range of combinatorial problems. Despite the great performance of SAT solvers, scalability becomes an issue whenever the instances become too large or too complex. For complex instances, the SAT solver may not be able to determine satisfiability in a reasonable amount of time and for large instances, the corresponding formula becomes too large, and solving becomes practically impossible. In this thesis, we propose different methods for overcoming these scalability issues. In particular, we discuss examples of efficient encoding design, scalability using a lazy approach, and embedding SAT-based methods into a heuristic approach using SAT-based local improvement (SLIM). These methods are discussed in the context of applications: we propose encodings for computing hypertree width and twin-width; a lazy approach to the directed feedback vertex problem; and SLIM approaches to graph coloring and decision tree induction.