Title
Hard satisfiable formulas for splittings by linear combinations.
Abstract
Itsykson and Sokolov in 2014 introduced the class of DPLL(circle plus) 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(circle plus) 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(circle plus) algorithms on unsatisfiable formulas. In this paper we consider a subclass of DPLL(circle plus) 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(circle plus). We give a construction of a family of satisfiable CNF formulas Psi(n) of size poly(n) such that any drunken DPLL(circle plus) algorithm with probability at least 1 - 2(-Omega(n)) runs at least 2(Omega(n)) steps on Psi(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(circle plus).
Year
DOI
Venue
2017
10.1007/978-3-319-66263-3_4
Lecture Notes in Computer Science
DocType
Volume
ISSN
Conference
10491
0302-9743
Citations 
PageRank 
References 
0
0.34
10
Authors
2
Name
Order
Citations
PageRank
Dmitry Itsykson13310.09
Alexander Knop235.69