In mathematics and theoretical computer science, entropy compression is an information theoretic method for proving that a random process terminates, originally used by Robin Moser to prove an algorithmic version of the Lovász local lemma.[1] [2]
To use this method, one proves that the history of the given process can be recorded in an efficient way, such that the state of the process at any past time can be recovered from the current state and this record, and such that the amount of additional information that is recorded at each step of the process is (on average) less than the amount of new information randomly generated at each step. The resulting growing discrepancy in total information content can never exceed the fixed amount of information in the current state, from which it follows that the process must eventually terminate. This principle can be formalized and made rigorous using Kolmogorov complexity.[3]
An example given by both Fortnow[3] and Tao concerns the Boolean satisfiability problem for Boolean formulas in conjunctive normal form, with uniform clause size. These problems can be parameterized by two numbers (k,t) where k is the number of variables per clause and t is the maximum number of different clauses that any variable can appear in. If the variables are assigned to be true or false randomly, then the event that a clause is unsatisfied happens with probability 2-k and each event is independent of all but r = k(t - 1) other events. It follows from the Lovász local lemma that, if t is small enough to make r < 2k/e (where e is the base of the natural logarithm) then a solution always exists. The following algorithm can be shown using entropy compression to find such a solution when r is smaller by a constant factor than this bound:
This algorithm cannot terminate unless the input formula is satisfiable, so a proof that it terminates is also a proof that a solution exists. Each iteration of the outer loop reduces the number of unsatisfied clauses (it causes C to become satisfied without making any other clause become unsatisfied) so the key question is whether the fix subroutine terminates or whether it can get into an infinite recursion.[3]
To answer this question, consider on the one hand the number of random bits generated in each iteration of the fix subroutine (k bits per clause) and on the other hand the number of bits needed to record the history of this algorithm in such a way that any past state can be generated. To record this history, we may store the current truth assignment (n bits), the sequence of initial arguments to the fix subroutine (m log m bits, where m is the number of clauses in the input), and then a sequence of records that either indicate that a recursive call to fix returned or that it in turn made another call to one of the r + 1 clauses (including C itself) that share a variable with C. There are r + 2 possible outcomes per record, so the number of bits needed to store a record is log r + O(1).[3]
This information can be used to recover the sequence of clauses given as recursive arguments to fix. The truth assignments at each stage of this process can then be recovered (without having to record any additional information) by progressing backwards through this sequence of clauses, using the fact that each clause was previously unsatisfiable to infer the values of all of its variables prior to each fix call. Thus, after f calls to fix, the algorithm will have generated fk random bits but its entire history (including those generated bits) can be recovered from a record that uses only m log m + n + f log r + O(f) bits. It follows that, when r is small enough to make log r + O(1) < k, the fix subroutine can only perform O(m log m + n) recursive calls over the course of the whole algorithm.[3]
The name "entropy compression" was given to this method in a blog posting by Terence Tao[4] and has since been used for it by other researchers.[5] [6] [7]
Moser's original version of the algorithmic Lovász local lemma, using this method, achieved weaker bounds than the original Lovász local lemma, which was originally formulated as an existence theorem without a constructive method for finding the object whose existence it proves. Later, Moser and Gábor Tardos used the same method to prove a version of the algorithmic Lovász local lemma that matches the bounds of the original lemma.[8]
Since the discovery of the entropy compression method, it has also been used to achieve stronger bounds for some problems than would be given by the Lovász local lemma. For example, for the problem of acyclic edge coloring of graphs with maximum degree Δ, it was first shown using the local lemma that there always exists a coloring with 64Δ colors, and later using a stronger version of the local lemma this was improved to 9.62Δ. However, a more direct argument using entropy compression shows that there exists a coloring using only 4(Δ - 1) colors, and moreover this coloring can be found in randomized polynomial time.[6]