Unsatisfiable Linear CNF Formulas Are Large and Complex

TL;DR

This paper investigates the size and complexity of unsatisfiable linear CNF formulas, establishing bounds on their clause counts, and demonstrating their structural complexity and difficulty for certain algorithms.

Contribution

It provides probabilistic bounds on the size of unsatisfiable linear k-CNF formulas and shows their inherent structural complexity compared to general formulas.

Findings

Existence of unsatisfiable linear k-CNF formulas with at most 4k^2 4^k clauses

Any linear k-CNF with fewer than 4^k/(8e^2k^2) clauses is satisfiable

Small unsatisfiable linear formulas are hard for Davis-Putnam style algorithms

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.