Unsatisfiable Linear CNF Formulas Are Large and Complex

Author Dominik Scheder



PDF
Thumbnail PDF

File

LIPIcs.STACS.2010.2490.pdf
  • Filesize: 319 kB
  • 12 pages

Document Identifiers

Author Details

Dominik Scheder

Cite As Get BibTex

Dominik Scheder. Unsatisfiable Linear CNF Formulas Are Large and Complex. In 27th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 5, pp. 621-632, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010) https://doi.org/10.4230/LIPIcs.STACS.2010.2490

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$.

Subject Classification

Keywords
  • Extremal combinatorics
  • proof complexity
  • probabilistic method

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail