Abstract published by ACM STOC Symposium

A constructive proof of the Lovasz Local Lemma

Robin A. Moser

The Lovasz Local Lemma 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 nother 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, Beck demonstrated that if the neighbourhood of
each clause\nbe restricted to O(2^k/48), a polynomial time algorithm
for the search problem exists. Alon simplified and randomized his
procedure and improved the bound to O(2^k/8). Srinivasan presented a
variant that achieves a bound of essentially O(2^k/4). In an earlier
publication, we improved this to O(2^k/2). In the present paper, we
give a randomized algorithm that finds a satisfying assignment to
every k-CNF formula in which each clause has a neighbourhood of at
most the asymptotic optimum of 2^k−5−1 other
clauses and that runs in expected time polynomial in the size of the
formula, irrespective of k. If k is considered a constant, we can also
give a deterministic variant. In contrast to all previous approaches,
our analysis does not anymore invoke the standard non-constructive
versions of the Local Lemma and can therefore be considered an
alternative, constructive proof of it.

Source: ACM STOC Abstracts

ACM Stock Symposium