Resolution over linear equations modulo two

We consider an extension of the resolution proof system that operates with disjunctions of linear equalities over F-2; we denote this system by Res(circle plus). 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(circle plus)-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(circle plus)-proofs. We also show that resolution and tree-like Res(circle plus) do not simulate each other. We prove a space vs size tradeoff for Res(circle plus)-proofs. We prove that Res(circle plus) is implicationally complete and also that Res(circle plus) is polynomially equivalent to its semantic version. We consider the proof system Res (circle plus; <= k) that is a restricted version of Res(circle plus) operating with disjunctions of linear equalities such that at most k equalities depend on more than one variable. We simulate Res (circle plus; <= k) in the ODBB-based proof system with blowup 2(k) and in Polynomial Calculus Resolution with blowup 2(nH(2k/n))poly(n), where n is the number of variables and H(p) is the binary entropy; the latter result implies exponontial lower bounds on the size of Res (circle plus; <=delta n)-proofs for some constant delta > 0 Raz and Tzameret introduced the system R(lin) which operates with disjunctions of linear equalities with integer coefficients. We show that Res(circle plus) can be p-simulated in R(lin). (C) 2019 Elsevier B.V. All rights reserved.