2026-07-23T06:18:08Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2490 2024-03-06T10:33:26Z ddc:004 open_access

Unsatisfiable Linear CNF Formulas Are Large and Complex Scheder, Dominik Extremal combinatorics proof complexity probabilistic method 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$. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Dominik Scheder 2010 Is Part Of LIPIcs, Volume 5, 27th International Symposium on Theoretical Aspects of Computer Science (2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2010.2490 urn:nbn:de:0030-drops-24901 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2010.2490 eng https://creativecommons.org/licenses/by-nd/3.0/legalcode