Resolution over linear equations modulo two |
| |
Affiliation: | St. Petersburg Department of Steklov Mathematical Institute of Russian Academy of Sciences, 27 Fontanka, St. Petersburg, 191023, Russia |
| |
Abstract: | We consider an extension of the resolution proof system that operates with disjunctions of linear equalities over ; we denote this system by Res(⊕). It is well known that tree-like resolution is equivalent in behavior to DPLL algorithms for the Boolean satisfiability problem. Every DPLL algorithm splits the input problem into two by assigning two possible values to a variable; then it simplifies the two resulting formulas and makes two recursive calls. Tree-like Res(⊕)-proofs correspond to an extension of the DPLL paradigm, in which we can split by an arbitrary linear combination of variables modulo two. These algorithms quickly solve formulas that explicitly encode linear systems modulo two which were used for proving exponential lower bounds for conventional DPLL algorithms.We prove exponential lower bounds on the size of tree-like Res(⊕)-proofs. We also show that resolution and tree-like Res(⊕) do not simulate each other.We prove a space vs size tradeoff for Res(⊕)-proofs. We prove that Res(⊕) is implicationally complete and also that Res(⊕) is polynomially equivalent to its semantic version.We consider the proof system that is a restricted version of Res(⊕) operating with disjunctions of linear equalities such that at most k equalities depend on more than one variable. We simulate in the OBDD-based proof system with blowup and in Polynomial Calculus Resolution with blowup , where n is the number of variables and is the binary entropy; the latter result implies exponential lower bounds on the size of -proofs for some constant . Raz and Tzameret introduced the system R(lin) which operates with disjunctions of linear equalities with integer coefficients. We show that Res(⊕) can be p-simulated in R(lin). |
| |
Keywords: | Resolution Proof system Lower bound Parity Pigeonhole principle |
本文献已被 ScienceDirect 等数据库收录! |
|