The central problem in complexity theory is to understand which problems can be solved efficiently. The central problem in propositional proof complexity is to understand which tautologies have efficient proofs in standard proof systems. There are many interconnections between these two lines of research, and in the last decade exciting new results have been obtained by combining and mixing ideas from both fields. The overall aim of this research project is to make progress in both of these areas (circuit complexity and proof complexity) with emphasis on proving lower bounds for propositional proof systems. A focus is the complexity of algebraic proof systems: these are natural proof systems derived from the Grobner basis algorithm. To illustrate their fundamental nature, there have already been several applications of algebraic lower bounds, including lower bounds for NP-search problems, lower bounds for bounded depth Frege proofs, and new algorithms for satisfiability testing. Related problems investigated include: the complexity of random formulas, the proof-theoretic strength required to resolve the P=?NP question, and connections to algebraic circuit lower bounds.
A complementary facet of the theoretical work described above is to build good algorithms for satisfiability testing. There has been an increasing trend to solve many problems, particular in AI domains, with heuristics for satisfiability. These algorithms are typically variations of standard proof search methods (i.e., randomized versions of resolution) and perform quite well empirically. However, almost no analytical results are known as to how, why and under which conditions the heuristics work well. A goal of this research is to provide analytical results that are meaningful, and to develop new algorithms for SAT and SSAT (stochastic SAT) that improve upon existing state-of-the-art algorithms.
