We consider boolean formulas in conjunctive normal form (CNF). If all clauses are large, it needs many clauses to obtain an unsatisfiable formula; moreover, these clauses have to interleave. We review quantitative results for the amount of interleaving required, many of which rely on the Lovász Local Lemma, a probabilistic lemma with many applications in combinatorics. In positive terms, we are interested in simple combinatorial conditions which guarantee for a CNF formula to be satisfiable. The criteria obtained are nontrivial in the sense that even though they are easy to check, it is by far not obvious how to compute a satisfying assignment efficiently in case the conditions are fulfilled; until recently, it was not known how to do so. It is also remarkable that while deciding satisfiability is trivial for formulas that satisfy the conditions, a slightest relaxation of the conditions leads us into the territory of NP-completeness. Several open problems remain, some of which we mention in the concluding section. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Gebauer, H., Moser, R. A., Scheder, D., & Welzl, E. (2009). The lovász local lemma and satisfiability. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5760 LNCS, pp. 30–54). https://doi.org/10.1007/978-3-642-03456-5_3
Mendeley helps you to discover research relevant for your work.