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.

 

Back to Sam Buss's publications page.