Randomness in proof complexity.
Published: 2005
Language: eng
Number of pages: 100
Description: 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.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.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 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 Chvatal and to Lovasz 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.
Notes: Thesis (Ph.D.)--University of Toronto, 2005.

Electronic version licensed for access by U. of T. users.

Source: Dissertation Abstracts International, Volume: 66-06, Section: B, page: 3221.