Unsatisfiable CNF Formulas contain Many Conflicts

Abstract

A pair of clauses in a CNF formula constitutes a conflict if there is a variable that occurs positively in one clause and negatively in the other. A CNF formula without any conflicts is satisfiable. The Lovász Local Lemma implies that a CNF formula with clauses of size exactly k (a k-CNF formula), is satisfiable unless some clause conflicts with at least $\frac{2^k}{e}$ clauses. It does not, however, give any good bound on how many conflicts an unsatisfiable formula has globally. We show here that every unsatisfiable k-CNF formula requires Ω(2.69^k) conflicts and there exist unsatisfiable k-CNF formulas with O(3.51^k) conflicts.