Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Bottleneck behavior in CNF formulas

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

MPI-I-2005-2-001. February 2005, 35 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-2005-2-001.ps471 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  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},