Lower bounds for splittings by linear combinations

ABSTRACT. A typical DPLL algorithm for the Boolean satisfiability problem splits the input problem into two by assigning the two possible values to a variable; then it simplifies the two resulting formulas.

In this paper we consider an extension of the DPLL paradigm. Our algorithms can split by an arbitrary linear combination of variables modulo two. These algorithms quickly solve formulas that encode linear systems modulo two, which were used for proving exponential lower bounds for conventional DPLL algorithms.

We prove exponential lower bounds on the running time of DPLL with splitting by linear combinations on 2-fold Tseitin formulas and on formulas that encode the pigeonhole principle.

We introdice an extension of the resolution proof system that operates with disjunctions of linear equalities; we call this system Res-Lin. Tree-like proofs in Res-Lin are equivalent to the behaiviour of our algorithms on unsatisfiable instances. We prove that Res-Lin is implication complete and also prove that Res-Lin is polynomially equivalent to its semantic version.