Theory and Applications of Satisfiability Testing - SAT 2008 : 11th International Conference, SAT 2008, Guangzhou, China, May 12 - 15, 2008; proceedings
The title of a journal, publication series:
Lecture Notes in Computer Science
Volume:
4996
Page range:
246-256
Conference title:
SAT 2008 - 11th International Conference on Theory and Applications of Satisfiability Testing
satisfiability , unsatisfiable formulas, conflict graph, Lovász Local Lemma
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. Clearly, a CNF formula has to have conflicts in order to be unsatisfiable—in fact, there have to be many conflicts, and it is the goal of this paper to quantify how many.
An unsatisfiable k-CNF has at least 2^k clauses; a lower bound of 2^k for the number of conflicts follows easily. We improve on this trivial bound by showing that an unsatisfiable k-CNF formula requires Ω(2.32^k) conflicts. On the other hand there exist unsatisfiable k-CNF formulas with O((4^k(log k)^3)/k) conflicts. This improves the simple bound O(4^k) arising from the unsatisfiable k-CNF formula with the minimum number of clauses.
Additional information:
The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-540-79719-7_23
Das Dokument wird vom Publikationsserver der Universitätsbibliothek Mannheim bereitgestellt.
Dieser Datensatz wurde nicht während einer Tätigkeit an der Universität Mannheim veröffentlicht, dies ist eine Externe Publikation.
Search Authors in
