A constructive proof of the Lovasz Local Lemma

Understand

The Lovasz Local Lemma [EL75] is a powerful tool to prove the existence of combinatorial objects meeting a prescribed collection of criteria.

• The technique can directly be applied to the satisfiability problem, yielding that a k-CNF formula in which each clause has common variables with at most 2^(k-2) other clauses is always satisfiable.
• All hitherto known proofs of the Local Lemma are non-constructive and do thus not provide a recipe as to how a satisfying assignment to such a formula can be efficiently found.
• In his breakthrough paper [Bec91], Beck demonstrated that if the neighbourhood of each clause be restricted to O(2^(k/48)), a polynomial time algorithm for the search problem exists.