Samuel R. Buss.
"Towards (Non-)Separations in Propositional Proof Complexity"
February 27, 2014.
Download talk slides: PDF.
This talk will discuss recent progress in understanding the complexity of
propositional proof systems. The first part will discuss fragments of
resolution used by SAT solvers based on CDCL or DPLL
with clause learning. These SAT solvers are
essentially searching for resolution proofs, and it is known that,
with restarts, CDCL can polynomially simulate resolution.
Without, restarts this is an open question. Several candidates
have been proposed in recent years for separating CDCL and resolution,
including Stone tautologies and guarded graph principles.
However, it has recently been shown that none of these candidates all
have short CDCL refutations and do not provide the conjectured separation.
The second part of the talk will concern Frege and extended Frege proofs. These are "textbook" propositional proof systems based on modus ponens and schematic axioms, reasoning about either Boolean formulas or Boolean circuits, respectively. It has long been conjectured that Frege systems do not polynomially simulate extended Frege systems. Several conjectured separation principles had remained open since the mid-1990's. However, recent work of Hrubes and Tzameret, and the speaker and his collaborators, have now shown that these principles, including Frankl's theorem, do not provide superpolynomial separations. Thus, unlike in the computation complexity setting, we have no good separation conjectures for propositional proof systems based on Boolean formulas versus Boolean circuits.
The talk will be largely expository, and will cover the needed proof complexity background and connections to computational complexity.
Back to Sam Buss's publications page.