Talk slides.
Samuel R. Buss.
"Towards (Non-)Separations in Propositional Proof Complexity"
Stanford University.
February 27, 2014.
Download talk slides: PDF.
Abstract:
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.