MPI-INF Logo
MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments

MPI-I-2005-2-001

Bottleneck behavior in CNF formulas

Hoffmann, Jörg and Gomes, Carla and Selman, Bart

February 2005, 35 pages.

.
Status: available - back from printing

Recent research has revealed that CNF formulas encoding applications often contain very small backdoors, i.e. subsets of variables branching over which suffices to decide satisfiability with a DPLL procedure. We shed light on what kinds of problem structure {\em cause} the existence of such small backdoors. We examine carefully crafted synthetic domains, clean enough to allow a rigorous analysis of DPLL search spaces, yet meaningful enough to allow conclusions about more practical domains. The synthetic CNF encodings are parameterized not only in their size, but also by a structure parameter controlling the extent of an intuitive bottleneck behavior in the underlying task. We investigate the size of the smallest possible backdoors as a function of the structure parameter. We prove upper bounds that, in certain cases, decrease {\em exponentially} in that parameter. We empirically verified the upper bounds as lower bounds in formulas small enough for full empirical exploration, and we conjecture that the upper bounds are exact in general. We present empirical results indicating that our notion of bottleneck behavior is relevant not only in our synthetic domains, but also in more practical domains.

  • MPI-I-2005-2-001.ps
  • Attachement: MPI-I-2005-2-001.ps (471 KBytes)

URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2005-2-001

Hide details for BibTeXBibTeX
@TECHREPORT{HoffmannGomesSelman2005,
  AUTHOR = {Hoffmann, J{\"o}rg and Gomes, Carla and Selman, Bart},
  TITLE = {Bottleneck behavior in CNF formulas},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-2005-2-001},
  MONTH = {February},
  YEAR = {2005},
  ISSN = {0946-011X},
}