Polynomial-size Frege and resolution proofs of st-connectivity and Hex tautologies

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.