Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
Hard satisfiable formulas for splittings by linear combinations. / Itsykson, Dmitry; Knop, Alexander.
Theory and Applications of Satisfiability Testing – SAT 2017 - 20th International Conference, Proceedings. ed. / Serge Gaspers; Toby Walsh. Springer Nature, 2017. p. 53-61 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10491 LNCS).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
}
TY - GEN
T1 - Hard satisfiable formulas for splittings by linear combinations
AU - Itsykson, Dmitry
AU - Knop, Alexander
PY - 2017/1/1
Y1 - 2017/1/1
N2 - Itsykson and Sokolov in 2014 introduced the class of DPLL(⊕) algorithms that solve Boolean satisfiability problem using the splitting by linear combinations of variables modulo 2. This class extends the class of DPLL algorithms that split by variables. DPLL(⊕) algorithms solve in polynomial time systems of linear equations modulo 2 that are hard for DPLL, PPSZ and CDCL algorithms. Itsykson and Sokolov have proved first exponential lower bounds for DPLL(⊕) algorithms on unsatisfiable formulas. In this paper we consider a subclass of DPLL(⊕) algorithms that arbitrary choose a linear form for splitting and randomly (with equal probabilities) choose a value to investigate first; we call such algorithms drunken DPLL(⊕). We give a construction of a family of satisfiable CNF formulas Ψn of size poly(n) such that any drunken DPLL(⊕) algorithm with probability at least 1-2-Ω(n) runs at least 2Ω(n) steps on Ψn; thus we solve an open question stated in the paper [12]. This lower bound extends the result of Alekhnovich, Hirsch and Itsykson [1] from drunken DPLL to drunken DPLL(⊕).
AB - Itsykson and Sokolov in 2014 introduced the class of DPLL(⊕) algorithms that solve Boolean satisfiability problem using the splitting by linear combinations of variables modulo 2. This class extends the class of DPLL algorithms that split by variables. DPLL(⊕) algorithms solve in polynomial time systems of linear equations modulo 2 that are hard for DPLL, PPSZ and CDCL algorithms. Itsykson and Sokolov have proved first exponential lower bounds for DPLL(⊕) algorithms on unsatisfiable formulas. In this paper we consider a subclass of DPLL(⊕) algorithms that arbitrary choose a linear form for splitting and randomly (with equal probabilities) choose a value to investigate first; we call such algorithms drunken DPLL(⊕). We give a construction of a family of satisfiable CNF formulas Ψn of size poly(n) such that any drunken DPLL(⊕) algorithm with probability at least 1-2-Ω(n) runs at least 2Ω(n) steps on Ψn; thus we solve an open question stated in the paper [12]. This lower bound extends the result of Alekhnovich, Hirsch and Itsykson [1] from drunken DPLL to drunken DPLL(⊕).
UR - http://www.scopus.com/inward/record.url?scp=85028719081&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-66263-3_4
DO - 10.1007/978-3-319-66263-3_4
M3 - Conference contribution
AN - SCOPUS:85028719081
SN - 9783319662626
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 53
EP - 61
BT - Theory and Applications of Satisfiability Testing – SAT 2017 - 20th International Conference, Proceedings
A2 - Gaspers, Serge
A2 - Walsh, Toby
PB - Springer Nature
T2 - 20th International Conference on Theory and Applications of Satisfiability Testing, SAT 2017
Y2 - 28 August 2017 through 1 September 2017
ER -
ID: 49785398