Resolution over linear equations and multilinear proofs

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 [RT06]. Specifically, we show the following:

• Type: Journal
• Year: 2008
• Where: APAL
• Authors: Ran Raz, Iddo Tzameret
• Keywords: APAL 2008, Linear Equations, Pigeonhole Principle, Tseitin Graph Tautologies