Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
Unsatisfiable CNF Formulas contain Many Conflicts
verfasst von : Dominik Scheder
Erschienen in: Algorithms and Computation
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.