Solving Hard Problems Using Logic

Ronald de Haan

There are many connections between logic and computational complexity. For example, the canonical NP-complete problem is that of satisfiability for propositional logic (SAT), and the canonical PSPACE-complete problem is deciding truth for quantified Boolean formulas. These connections are not only useful for the theory of computational complexity. They can also be used to develop (often well-performing) algorithms for computationally intractable problems. For example, NP-complete problems can be solved by (i) a translation into propositional logic, and (ii) using an optimized SAT solving algorithm to solve the problem.

In this tutorial, we start with the basic connections between logic problems and computational complexity. We will see how these connections can be used to construct algorithms for computationally hard problems. We will look at several examples, related to propositional logic, quantified Boolean formulas, logic programming, and monadic second-order logic.