Preliminary version of article:
Samuel R. Buss
"Polynomial-Size Frege and Resolution Proofs of st-Connectivity
and Hex Tautologies"
Theoretical Computer Science 357, 1-3 (2006) 35-52.
Download black and white version: postscript
or PDF.
Download color version:i
postscript
or PDF.
Software: C++ software StConn generates CNF formulations of the st-connectivity principle discussed in this paper.
Abstract:
A grid graph has rectangularly arranged
vertices with edges permitted only between orthogonally adjacent vertices. The st-connectivity
principle states that it is not possible to have a red path of edges and a
green path of edges which connect diagonally opposite corners of the grid graph
unless the paths cross somewhere.
We prove that the propositional tautologies which encode the st-connectivity
principle have polynomial size Frege proofs and polynomial size TC0-Frege
proofs. For bounded width grid graphs, the st-connectivity tautologies
have polynomial size resolution proofs. A key part of the proof is to show that
the group with two generators, both of order two, has word problem in
alternating logtime (Alogtime) and even in TC0.
Conversely, we show that constant depth Frege proofs of the st-connectivity
tautologies require near-exponential size. The proof uses a reduction from the
pigeonhole principle, via tautologies that express a ``directed single source''
principle SINK, which is related to Papadimitriou's search classes PPAD and
PPADS (or, PSK).
The st-connectivity principle is related to
Urquhart's propositional Hex tautologies, and we establish the same upper and
lower bounds on proof complexity for the Hex tautologies. In addition, the Hex
tautology is shown to be equivalent to the SINK tautologies and to the
one-to-one onto pigeonhole principle. '
Related talk:
"Propositional Proofs of Hex Tautologies and st-Connectivity";,
presented at Workshop on Proof Theory, Muenster, October
2003, On the occasion of W. Pohler's 60th Birthday.
and revised for the 12th Latin American Symposium on
Mathematical Logic, Costa Rica, January 2004.
Download color slides:
postscript or PDF.
Related talk:
"Bounded Arithmetic, Constant-Depth Proofs, and st-Connectivity";,
presented at UCLA Logic Meeting (Very Informal
Gathering), February, 2005.
Modified version of above talk, with a new result joint with
Chris Pollett.
Download color slides:
postscript or PDF.