Scheder, Dominik
Unsatisfiable Linear CNF Formulas Are Large and Complex
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 (nonlinear) 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 DavisPutnam 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 = {621632},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897163},
ISSN = {18688969},
year = {2010},
volume = {5},
editor = {JeanYves Marion and Thomas Schwentick},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2010/2490},
URN = {urn:nbn:de:0030drops24901},
doi = {http://dx.doi.org/10.4230/LIPIcs.STACS.2010.2490},
annote = {Keywords: Extremal combinatorics, proof complexity, probabilistic method}
}
Keywords: 

Extremal combinatorics, proof complexity, probabilistic method 
Seminar: 

27th International Symposium on Theoretical Aspects of Computer Science

Issue date: 

2010 
Date of publication: 

09.03.2010 