Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
Lower bounds for splittings by linear combinations. / Itsykson, Dmitry; Sokolov, Dmitry.
Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Proceedings. PART 2. ed. Springer Nature, 2014. p. 372-383 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8635 LNCS, No. PART 2).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
}
TY - GEN
T1 - Lower bounds for splittings by linear combinations
AU - Itsykson, Dmitry
AU - Sokolov, Dmitry
PY - 2014/1/1
Y1 - 2014/1/1
N2 - 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 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 running time of DPLL with splitting by linear combinations on 2-fold Tseitin formulas and on formulas that encode the pigeonhole principle. Raz and Tzameret introduced a system R(lin) which operates with disjunctions of linear equalities with integer coefficients. We consider an extension of the resolution proof system that operates with disjunctions of linear equalities over; we call this system Res-Lin. Res-Lin can be p-simulated in R(lin) but currently we do not know any superpolynomial lower bounds in R(lin). Tree-like proofs in Res-Lin are equivalent to the behavior 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.
AB - 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 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 running time of DPLL with splitting by linear combinations on 2-fold Tseitin formulas and on formulas that encode the pigeonhole principle. Raz and Tzameret introduced a system R(lin) which operates with disjunctions of linear equalities with integer coefficients. We consider an extension of the resolution proof system that operates with disjunctions of linear equalities over; we call this system Res-Lin. Res-Lin can be p-simulated in R(lin) but currently we do not know any superpolynomial lower bounds in R(lin). Tree-like proofs in Res-Lin are equivalent to the behavior 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.
UR - http://www.scopus.com/inward/record.url?scp=84906239772&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-44465-8_32
DO - 10.1007/978-3-662-44465-8_32
M3 - Conference contribution
AN - SCOPUS:84906239772
SN - 9783662444641
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 372
EP - 383
BT - Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Proceedings
PB - Springer Nature
T2 - 39th International Symposium on Mathematical Foundations of Computer Science, MFCS 2014
Y2 - 25 August 2014 through 29 August 2014
ER -
ID: 49785815