Doctoral Thesis Oral Defense - Emre Yolcu
— 3:30pm
Location:
In Person
-
ASA Conference Room, Gates Hillman 6115
Speaker:
EMRE YOLCU,
Ph.D. Candidate
Computer Science Department
Carnegie Mellon University
https://www.cs.cmu.edu/~eyolcu/
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.
Thesis Committee
Marijn Heule (Chair)
Jeremy Avigad
Ryan O'Donnell
Sam Buss (University of California San Diego)
For More Information:
matthewstewart@cmu.edu