TR07-078 Authors: Ran Raz, Iddo Tzameret

Publication: 14th August 2007 12:44

Downloads: 2500

Keywords:

We develop and study the complexity of propositional proof systems of varying strength extending resolution by allowing it to operate with disjunctions of linear equations instead of clauses. We demonstrate polynomial-size refutations for hard tautologies like the pigeonhole principle, Tseitin graph tautologies and the clique-coloring tautologies in these proof systems. Using the (monotone) interpolation by a communication game technique we establish an exponential-size lower bound on refutations in a certain, considerably strong, fragment of resolution over linear equations, as well as a general polynomial upper bound on (non-monotone) interpolants in this fragment.

We then apply these results to extend and improve previous results on

multilinear proofs (over fields of characteristic 0), as studied in

[RazTzameret06]. Specifically, we show the following:

1. Proofs operating with depth-3 multilinear formulas polynomially simulate a certain, considerably strong, fragment of resolution over linear equations.

2. Proofs operating with depth-3 multilinear formulas admit polynomial-size refutations of the pigeonhole principle and Tseitin graph tautologies. The former improve over a previous result that established small multilinear proofs only for the \emph{functional} pigeonhole principle. The latter are different than previous proofs, and apply to multilinear proofs of Tseitin mod p graph tautologies over any field of characteristic 0.

We conclude by connecting resolution over linear equations with extensions of the cutting planes proof system.