Unsatisfiable CNF Formulas need many Conflicts

TL;DR

This paper investigates the relationship between conflicts in CNF formulas and their satisfiability, establishing lower and upper bounds on the number of conflicts in unsatisfiable formulas.

Contribution

It provides the first non-trivial bounds on the minimum and maximum number of conflicts in unsatisfiable k-CNF formulas.

Findings

Unsatisfiable k-CNF formulas require at least 2.69^k conflicts.

There exist unsatisfiable k-CNF formulas with up to 3.51^k 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 Lovasz Local Lemma implies that a k-CNF formula is satisfiable if each clause conflicts with at most 2^k/e-1 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 3.51^k conflicts.