TY - JOUR

T1 - Resolution over linear equations and multilinear proofs

AU - Raz, Ran

AU - Tzameret, Iddo

N1 - Funding Information:
We wish to thank Arist Kojevnikov for useful correspondence on his paper. We are grateful to the anonymous referees for very helpful comments that improved the presentation of this paper. The first author was supported by The Israel Science Foundation and The Minerva Foundation. The second author was supported by The Israel Science Foundation (grant no. 250/05).

PY - 2008/10

Y1 - 2008/10

N2 - 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 (monotone) interpolation 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 [Ran Raz, Iddo Tzameret, The strength of multilinear proofs. Comput. Complexity (in press)]. Specifically, we show the following: •Proofs operating with depth-3 multilinear formulas polynomially simulate a certain, considerably strong, fragment of resolution over linear equations.•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 functional pigeonhole principle. The latter are different from 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.

AB - 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 (monotone) interpolation 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 [Ran Raz, Iddo Tzameret, The strength of multilinear proofs. Comput. Complexity (in press)]. Specifically, we show the following: •Proofs operating with depth-3 multilinear formulas polynomially simulate a certain, considerably strong, fragment of resolution over linear equations.•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 functional pigeonhole principle. The latter are different from 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.

KW - Algebraic proof systems

KW - Cutting planes

KW - Feasible monotone interpolation

KW - Multilinear proofs

KW - Proof complexity

KW - Resolution

UR - http://www.scopus.com/inward/record.url?scp=52949148969&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=52949148969&partnerID=8YFLogxK

U2 - 10.1016/j.apal.2008.04.001

DO - 10.1016/j.apal.2008.04.001

M3 - Article

AN - SCOPUS:52949148969

VL - 155

SP - 194

EP - 224

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

SN - 0168-0072

IS - 3

ER -