首页    期刊浏览 2024年10月06日 星期日
登录注册

文章基本信息

  • 标题:Hard satisfiable formulas for splittings by linear combinations
  • 本地全文:下载
  • 作者:Dmitry Itsykson ; Alexander Knop
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2017
  • 卷号:2017
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:

    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 two 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 of Itsykson and Sokolov. This lower bound extends the result of Alekhnovich, Hirsch and Itsykson (2005) from drunken DPLL to drunken DPLL( ).

  • 关键词:DPLL ; lower bounds ; Resolution over linear equations ; SAT ; satisfiable formulas
国家哲学社会科学文献中心版权所有