Randomness in proof complexity
Joshua Buresh-Oppenheim · 2005
This thesis focuses on the topic of propositional proof complexity, which is an area of study with deep connections to both mathematical logic and complexity theory. Three common propositional proof systems (or subsystems thereof) are considered: Resolution, bounded-depth Frege and Cutting Planes. Two uses of randomness for achieving lower bounds on these systems are explored, namely, using randomly generated tautologies as inputs to the proof systems, and using random restrictions to reason about the complexity of proofs of these tautologies. In particular, there are three main results. The first is an almost-complete characterization, in terms of relative size-complexity, of the six most popular refinements of Resolution. These refinements are important, both practically and theoretically, for automated theorem proving. The second main result represents substantial progress towards our understanding of the most fundamental tautology in proof complexity: the pigeonhole principle. The pigeonhole principle with parameters m and n states that m pigeons cannot be placed in n holes without collisions whenever m? n. As m gets bigger relative to n, the statement gets weaker and therefore easier to prove. We show that this tautology requires superpolynomial-size proofs in bounded-depth Frege whenever m is at most (1 + 1=polylog n) times n. The third main result analyzes cutting planes procedures, which are used primarily in combinatorial optimization, as propositional proof systems. It is shown that many rounds of the procedures due to Gomory and Chvátal and to Lovász and Schrijver are required to prove the unsatisfiability of many CNF formulas, including random kCNFs and the (negation of the) Tseitin Tautologies. It follows that many rounds of these procedures are required to well-approximate the optimization problem MAXSAT.