Resolution over Linear Equations and Multilinear Proofs
Ran Raz, Iddo Tzameret

TL;DR
This paper introduces and analyzes proof systems extending resolution with linear equations, demonstrating their efficiency on certain tautologies and establishing bounds, while connecting them to multilinear proofs and cutting planes.
Contribution
It develops resolution over linear equations, proves polynomial-size refutations for key tautologies, and links these systems to multilinear proofs and cutting planes.
Findings
Polynomial-size refutations for pigeonhole principle and Tseitin tautologies.
Exponential lower bounds for certain fragments of resolution over linear equations.
Polynomial upper bounds for non-monotone interpolants in these fragments.
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge
