Doctoral Thesis Proposal - Emre Yolcu

— 3:30pm

Location:
In Person - Gordon Bell Conference, Gates Hillman 5117

Speaker:
EMRE YOLCU, Ph.D. Student, Computer Science Department, Carnegie Mellon University
https://www.cs.cmu.edu/~eyolcu/

Weak Extended Resolution and Nonautomatability in Proof Complexity

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. 

In this thesis proposal, we focus on proof complexity theoretic problems from two "contrasting" ends of a spectrum: those motivated by SAT solving, aiming to improve heuristic proof search, and those arising from computational complexity, aiming to show that proof search is hard in the worst case. In particular, we focus on the following two lines of research: proof complexity of a family of systems that we refer to as weak extended resolution systems and the automatability problem from computational complexity. The first involves proof systems that formalize restricted versions of the ability to make assumptions that hold without loss of generality, commonly used informally to shorten proofs. The second is the question of whether efficient proof search is possible in the worst case. We give a complete description of the relative strengths of core weak extended resolution systems by introducing a high-level recipe for proving separations. We introduce a technique to reduce the hardness of automatability between proof systems in a black-box manner; we give an example application and propose an approach to lift hardness results from weaker to stronger proof systems. 

Thesis Committee 

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

Additional Information