高级算法 (Fall 2016)/''Lovász'' Local Lemma: Difference between revisions
imported>Etone |
imported>Etone |
||
Line 178: | Line 178: | ||
# If a '''Fix'''(<math>C</math>) is being called, the values of variables in <math>C</math> are uniquely determined. | # If a '''Fix'''(<math>C</math>) is being called, the values of variables in <math>C</math> are uniquely determined. | ||
}} | }} | ||
Revision as of 07:32, 9 October 2016
Under construction.
Lovász Local Lemma
Assume that
The dependency graph
The notion of mutual independence between an event and a set of events is formally defined as follows.
Definition (mutual independence) - An event
is said to be mutually independent of events , if for any disjoint , it holds that .
- An event
Given a sequence of events
Definition (dependency graph) - Let
be a sequence of events. A graph on the set of vertices is called a dependency graph for the events if for each , , the event is mutually independent of all the events . - Furthermore, for each event
:- define
as the neighborhood of event in the dependency graph; - define
as the inclusive neighborhood of , i.e. the set of events adjacent to in the dependency graph, including itself.
- define
- Let
- Example
- Let
be a set of mutually independent random variables. Each event is a predicate defined on a number of variables among . Let be the unique smallest set of variables which determine . The dependency graph is defined by iff .
The local lemma
The following lemma, known as the Lovász local lemma, first proved by Erdős and Lovász in 1975, is an extremely powerful tool, as it supplies a way for dealing with rare events.
Lovász Local Lemma (symmetric case) - Let
be a set of events, and assume that there is a such that the followings are satisfied:- for all
, ; - the maximum degree of the dependency graph for the events
is , and
.
- for all
- Then
.
- Let
The following is a general asymmetric version of the local lemma. This generalization is due to Spencer.
Lovász Local Lemma (general case) - Let
be a sequence of events. Suppose there exist real numbers such that and for all , .
- Then
.
- Let
To see that the general LLL implies symmetric LLL, we set
Assume the condition in the symmetric LLL:
- for all
, ; ;
- for all
then it is easy to verify that for all
.
Due to the general LLL, we have
.
This proves the symmetric LLL.
Alternatively, by setting
Lovász Local Lemma (symmetric case, alternative form) - Let
be a set of events, and assume that there is a such that the followings are satisfied:- for all
, ; - the maximum degree of the dependency graph for the events
is , and
.
- for all
- Then
.
- Let
The original proof of the Lovász Local Lemma is by induction. See this note for the original non-constructive proof of Lovász Local Lemma.
Random Search for -SAT
We start by giving the definition of
Definition (exact- -CNF)- A logic expression
defined on Boolean variables is said to be a conjunctive normal form (CNF) if: can be written as a conjunction(AND) of clauses as ;- each clause
is a disjunction(OR) of literals; - each literal
is either a variable or the negation of a variable.
- We call a CNF formula
-CNF, or more precisely an exact- -CNF, if every clause consists of exact distinct literals.
- A logic expression
For example:
is a
- Remark
- The notion of
-CNF defined here is slightly more restrictive than the standard definition of -CNF, where each clause consists of at most variables. See here for a discussion of the subtle differences between these two definitions.
A logic expression
The
-SAT- Input: a
-CNF formula . - Determines whether
is satisfiable.
- Input: a
It is well known that
Satisfiability of -CNF
As in the Lovasz local lemma, we consider the dependencies between clauses in a CNF formula.
We say that a CNF formula
By the Lovasz local lemma, we almost immediately have the following theorem for the satisfiability of
Theorem - Let
be a -CNF formula with maximum degree at most . If then is always satisfiable.
- Let
Proof. Let
be Boolean random variables sampled uniformly and independently from . We are going to show that is satisfied by this random assignment with positive probability. Due to the probabilistic method, this will prove the existence of a satisfying assignment for .Suppose there are
clauses in . Let denote the bad event that is not satisfied by the random assignment . Clearly, each is dependent with at most other 's, which means the maximum degree of the dependency graph for is at most .Recall that in a
-CNF , every clause consists of precisely variable, and is violated by only one assignment among all assignments of the variables in . Therefore, the probability of being violated is .If
, that is, , then due to Lovasz local lemma (symmetric case, alternative form), it holds that .
The existence of satisfying assignment follows by the probabilistic method.
Moser's recursive fix algorithm
The above theorem basically says that for a CNF if every individual clause is easy to satisfy and is dependent with few other clauses then the CNF should be always satisfiable. However, the theorem only states the existence of a satisfying solution, but does not gives a way to find such solution.
In 2009, Moser gave a very simple randomized algorithm which efficiently finds a satisfying assignment with high probability under the condition
We need the following notations. Given as input a CNF formula
- let
be the Boolean variables on which is defined, and the set of clauses in ; - for each clause
, we denote by the set of variables on which is defined; - we also abuse the notation and denote by
the neighborhood of , i.e. the set of other clauses in that shares variables with , and the inclusive neighborhood of , i.e. the set of all clauses, including itself, that share variables with .
The algorithm consists of two components: the main function Solve() and a sub-routine Fix().
Solve(CNF )- Pick values of
uniformly and independently at random; - While there is an unsatisfied clause
in- Fix(
);
- Fix(
- Pick values of
The sub-routine Fix() is a recursive procedure:
Fix(Clause )- Replace the values of variables in
with new uniform and independent random values; - While there is unsatisfied clause
- Fix(
);
- Fix(
- Replace the values of variables in
It is an amazing discovery that this simple algorithm works well as long as the condition of Lovasz local lemma is satisfied. Here we prove a slightly weaker statement for the convenience of analysis.
Theorem - Let
be a -CNF formula with maximum degree at most . - There is a universal constant
, such that if then the algorithm Solve( ) finds a satisfying assignment for in time with high probability.
- Let
The analysis is based on a technique called entropy compression. This is a very clever idea and may be very different from what you might have seen so far about algorithm analysis. We first give a high-level description of this idea:
- We use
to abstractly denote an algorithm running on an input with random bits . For an algorithm with no access to the random bits , once the input is fixed, the behavior of the algorithm as well as its output is deterministic. But for randomized algorithms, the behavior of is a random variable even when the input is fixed. - Fix an arbitrary (worst-case) input
. We try to construct a succinct representation of the behavior of in such a manner that the random bits can always be fully recovered from this succinct representation . In other words, gives an encoding (a 1-1 mapping) of the random bits to a succinct representation . - It is a fundamental law that random bits cannot be compressed significantly by any encoding. Therefore if a longer running time of
would imply that the random bits can be encoded to a succinct representation which is much shorter than , then we prove the running time of the algorithm cannot be too long.
- A natural way to reach this last contradiction is to have the following situation: As the running time of
grows, naturally both lengths of random bits and the succinct representation of the behavior of grow. So if the former grows much faster than the latter as the running time grows, then a large running time may cause the length of significantly greater than the length of .
- A natural way to reach this last contradiction is to have the following situation: As the running time of
We now proceed to the analysis of
From now on we assume that the input instance
- Let
denote the total number of time the function is being called (including both the calls in and the recursive calls). - Let
.
Note that
The reason we consider
We start by making the following simple observations:
- A clause
in will be satisfied after Fix( ) returned and will remain as being satisfied afterwards. - At the moment a Fix(
) being called, the clause must be unsatisfied.
Proposition - There are at most
top-level callings to Fix(), where is the total number of clauses in . - If a Fix(
) is being called, the values of variables in are uniquely determined.
- There are at most