An Improved Bound on the Number of Conflicts in Unsatisfiable k-CNF Formulas
Dominik Scheder, Philipp Zumstein · 2008
Abstract. In a CNF formula, we say that a pair C, D of clauses constitutes a conflict if there is a variable that occurs positively in one clause and negatively in the other. We show that any a k-CNF formula with less than O ` 2.69 k ´ conflicts is satisfiable. 1