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(⊕).

Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing – SAT 2017 - 20th International Conference, Proceedings
EditorsSerge Gaspers, Toby Walsh
PublisherSpringer Nature
Pages53-61
Number of pages9
ISBN (Print)9783319662626
DOIs
StatePublished - 1 Jan 2017
Event20th International Conference on Theory and Applications of Satisfiability Testing, SAT 2017 - Melbourne, Australia
Duration: 28 Aug 20171 Sep 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10491 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference20th International Conference on Theory and Applications of Satisfiability Testing, SAT 2017
Country/TerritoryAustralia
CityMelbourne
Period28/08/171/09/17

    Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

ID: 49785398