License: Creative Commons Attribution-NoDerivs 3.0 Unported license (CC BY-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2010.2490
URN: urn:nbn:de:0030-drops-24901
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2490/
Go to the corresponding LIPIcs Volume Portal

Scheder, Dominik

Unsatisfiable Linear CNF Formulas Are Large and Complex

pdf-format:
1001.SchederDominik.2490.pdf (0.3 MB)

Abstract

We call a CNF formula {\em linear} if any two clauses have at most one variable in common. We show that there exist unsatisfiable linear $k$-CNF formulas with at most $4k^24^k$ clauses, and on the other hand, any linear $k$-CNF formula with at most $\frac{4^k}{8e^2k^2}$ clauses is satisfiable. The upper bound uses probabilistic means, and we have no explicit construction coming even close to it. One reason for this is that unsatisfiable linear formulas exhibit a more complex structure than general (non-linear) formulas: First, any treelike resolution refutation of any unsatisfiable linear $k$-CNF formula has size at least $2^{2^{\frac{k}{2}-1}}$. This implies that small unsatisfiable linear $k$-CNF formulas are hard instances for Davis-Putnam style splitting algorithms. Second, if we require that the formula $F$ have a {\em strict} resolution tree, i.e. every clause of $F$ is used only once in the resolution tree, then we need at least $a^{a^{\iddots^a}}$ clauses, where $a \approx 2$ and the height of this tower is roughly $k$.

BibTeX - Entry

@InProceedings{scheder:LIPIcs:2010:2490,
  author =	{Dominik Scheder},
  title =	{{Unsatisfiable Linear CNF Formulas Are Large and Complex}},
  booktitle =	{27th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{621--632},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-16-3},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{5},
  editor =	{Jean-Yves Marion and Thomas Schwentick},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2490},
  URN =		{urn:nbn:de:0030-drops-24901},
  doi =		{10.4230/LIPIcs.STACS.2010.2490},
  annote =	{Keywords: Extremal combinatorics, proof complexity, probabilistic method}
}

Keywords: Extremal combinatorics, proof complexity, probabilistic method
Collection: 27th International Symposium on Theoretical Aspects of Computer Science
Issue Date: 2010
Date of publication: 09.03.2010

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI