Unsatisfiable Linear CNF Formulas Are Large, and Difficult to Construct Explicitely

Dominik Scheder 1, *
Abstract : We call a CNF formula 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^2 4^k clauses, and on the other hand, any linear k-CNF formula with at most 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^(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 strict resolution tree, i.e. every clause of F is used only once in the resolution tree, then we need at least a^a^...^a clauses, where a is approximately 2 and the height of this tower is roughly k.
Document type :
Conference papers
Jean-Yves Marion and Thomas Schwentick. 27th International Symposium on Theoretical Aspects of Computer Science - STACS 2010, Mar 2010, Nancy, France. pp.621-632, 2010, Proceedings of the 27th Annual Symposium on the Theoretical Aspects of Computer Science
Liste complète des métadonnées


https://hal.inria.fr/inria-00455809
Contributor : Publications Loria <>
Submitted on : Thursday, February 11, 2010 - 11:50:29 AM
Last modification on : Thursday, February 11, 2010 - 12:57:50 PM
Document(s) archivé(s) le : Friday, June 18, 2010 - 8:13:58 PM

File

scheder.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00455809, version 1

Collections

Citation

Dominik Scheder. Unsatisfiable Linear CNF Formulas Are Large, and Difficult to Construct Explicitely. Jean-Yves Marion and Thomas Schwentick. 27th International Symposium on Theoretical Aspects of Computer Science - STACS 2010, Mar 2010, Nancy, France. pp.621-632, 2010, Proceedings of the 27th Annual Symposium on the Theoretical Aspects of Computer Science. <inria-00455809>

Share

Metrics

Record views

157

Document downloads

108