In mathematics and theoretical computer science, entropy compression is an
information theoretic method for proving that a
random process
In probability theory and related fields, a stochastic () or random process is a mathematical object usually defined as a family of random variables in a probability space, where the index of the family often has the interpretation of time. Stoc ...
terminates, originally used by Robin Moser to prove an
algorithmic version of the
Lovász local lemma
In probability theory, if a large number of events are all independent of one another and each has probability less than 1, then there is a positive (possibly small) probability that none of the events will occur. The Lovász local lemma allows a s ...
.
[.]
Description
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
In algorithmic information theory (a subfield of computer science and mathematics), the Kolmogorov complexity of an object, such as a piece of text, is the length of a shortest computer program (in a predetermined programming language) that prod ...
.
[.]
Example
An example given by both Fortnow
and Tao
concerns the
Boolean satisfiability problem
In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) asks whether there exists an Interpretation (logic), interpretation that Satisf ...
for
Boolean formulas in
conjunctive normal form
In Boolean algebra, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs.
In au ...
, with uniform clause size. These problems can be
parameterized by two numbers
where
is the number of variables per clause and
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
and each event is independent of all but
other events. It follows from the
Lovász local lemma
In probability theory, if a large number of events are all independent of one another and each has probability less than 1, then there is a positive (possibly small) probability that none of the events will occur. The Lovász local lemma allows a s ...
that, if
is small enough to make
(where
is the base of the
natural logarithm
The natural logarithm of a number is its logarithm to the base of a logarithm, base of the e (mathematical constant), mathematical constant , which is an Irrational number, irrational and Transcendental number, transcendental number approxima ...
) then a solution always exists. The following algorithm can be shown using entropy compression to find such a solution for inputs that obey a constraint on
of a similar form.
*Choose a random truth assignment
*While there exists an unsatisfied clause
, call a recursive subroutine
fix
with
as its argument. This subroutine chooses a new random truth assignment for the variables in
, and then recursively calls the same subroutine on all unsatisfied clauses (possibly including
itself) that share a variable until none are left.
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
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
In computer science, recursion is a method of solving a computational problem where the solution depends on solutions to smaller instances of the same problem. Recursion solves such recursive problems by using functions that call themselves ...
.
To answer this question, consider on the one hand the number of random bits generated in each iteration of the
fix
subroutine (
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 (
bits), the sequence of arguments to the outermost calls to the
fix
subroutine (at most
bits, where
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 made a recursive call, and which of the
clauses sharing a variable with the current clause was passed as an argument to that recursive call. There are
possible outcomes per record, so the number of bits needed to store a record (using a compact encoding method such as
arithmetic coding
Arithmetic coding (AC) is a form of entropy encoding used in lossless data compression. Normally, a String (computer science), string of characters is represented using a fixed number of bits per character, as in the American Standard Code for In ...
that allows storage using a fractional number of bits per record)
This information is enough to recover the entire sequence of calls to
fix
, including the identity of the clause given as an argument to each call. To do so, progress forward through the call sequence using the stored outermost call arguments and stored records to infer the argument of each call in turn. Once the sequence of recursive calls and their arguments has been recovered, the truth assignments at each stage of this process can also be recovered from the same information. To do so, start from the final truth assignment and then progress backwards through the sequence of randomly reassigned clauses, using the fact that each clause was previously unsatisfiable to uniquely determine the values of all of its variables prior to its random reassignment. Thus, after
calls to
fix
, the algorithm will have generated
random bits but its entire history (including those generated bits) can be recovered from a record that uses only
bits. This is only possible when the number of stored bits is at least as large as the number of randomly generated bits. It follows that, when
is small enough to make