TY - JOUR

T1 - Resolution over linear equations modulo two

AU - Itsykson, Dmitry

AU - Sokolov, Dmitry

N1 - Funding Information: The research presented in Sections 3.5 and 5 was supported by Russian Science Foundation (project 16-11-10123 ).

PY - 2020/1

Y1 - 2020/1

N2 - We consider an extension of the resolution proof system that operates with disjunctions of linear equalities over F2; 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 Res(⊕;⩽k) 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 Res(⊕;⩽k) in the OBDD-based proof system with blowup 2k and in Polynomial Calculus Resolution with blowup 2nH(2k/n)poly(n), where n is the number of variables and H(p) is the binary entropy; the latter result implies exponential lower bounds on the size of Res(⊕;⩽δn)-proofs for some constant δ>0. 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).

AB - We consider an extension of the resolution proof system that operates with disjunctions of linear equalities over F2; 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 Res(⊕;⩽k) 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 Res(⊕;⩽k) in the OBDD-based proof system with blowup 2k and in Polynomial Calculus Resolution with blowup 2nH(2k/n)poly(n), where n is the number of variables and H(p) is the binary entropy; the latter result implies exponential lower bounds on the size of Res(⊕;⩽δn)-proofs for some constant δ>0. 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).

KW - Lower bound

KW - Parity

KW - Pigeonhole principle

KW - Proof system

KW - Resolution

KW - POLYNOMIAL CALCULUS

KW - CONSTRAINT PROPAGATION

KW - LOWER BOUNDS

KW - HARD EXAMPLES

KW - COMPLEXITY

KW - TREE-LIKE

KW - SYSTEMS

KW - SEPARATION

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

UR - https://www.mendeley.com/catalogue/c7289fbc-18ba-38c4-9b8f-551dd413e60a/

U2 - 10.1016/j.apal.2019.102722

DO - 10.1016/j.apal.2019.102722

M3 - Article

AN - SCOPUS:85071464923

VL - 171

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

SN - 0168-0072

IS - 1

M1 - 102722

ER -