The satisfiability problem for propositional logic (SAT) has been a central topic in computer science for many decades. It is arguably the canonical NP-complete problem: reductions from many other problems in NP to SAT are often straightforward. As a consequence, a reasonable strategy when trying to solve a problem in NP is to reduce it to SAT and to try to solve the resulting SAT problem instead. This strategy turns out to be surprisingly effective thanks to the effectiveness of implementations of heuristic algorithms for SAT, commonly known as SAT solvers. Those solvers are expected to output proofs to certify their answers, and in this sense they are proof search algorithms. Proof complexity, the branch of computational complexity that studies the lengths of proofs in propositional proof systems, offers a way to analyze the performance of SAT solvers.

This thesis explores the interplay between SAT solving and proof complexity. On the theoretical side, we investigate the power of weak, resolution-based proof systems that incorporate restricted forms of the extension rule often used in SAT solvers. We provide a complete characterization of their relative strengths. In particular, we present a general recipe for constructing formulas that yield exponential separation results, showing that none of these systems subsumes another in expressivity. We also establish new exponential lower bounds for some of those systems, pinpointing the inherent limitations of various clause addition rules. The key insights for those separations come from the notion of an effective simulation. We leverage these insights to better understand the complexity of proof search: for example, we show that even a seemingly weaker system like regular resolution can effectively simulate general resolution, which has the corollary that significantly faster algorithms for finding regular resolution proofs would also speed up general resolution proof search.

On the practical side, we demonstrate how advances in SAT solving can aid in mathematical discovery. We develop an automated approach to the Collatz conjecture, a notorious open problem in number theory, by encoding it as a search for a termination proof in a rewriting system. We show how the Collatz function can be expressed as a string rewriting system that terminates if and only if the conjecture holds, and we use state-of-the-art automated reasoning tools to verify partial results. Notably, we automatically prove several weakened forms of the Collatz conjecture, and we analyze why certain approaches (such as natural matrix interpretations) are bound to fail in finding a termination proof for those problems. This case study showcases the current power of SAT solvers in tackling challenging problems beyond NP, as well as the obstacles for fully automated resolution of deep conjectures.

155 pages

Thesis Committee:
Marijn J.H. Heule (Chair)
Jeremy Avigad
Ryan O'Donnell
Samuel R. Buss (University of California San Diego)

Jignesh Patel, Interim Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Creative Commons: CC-BY (Attribution)

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu