Boolean Satisfiability

There is an interesting link between maximum likelihood decoding and boolean formula satisfiability. Specifically, given a noise-corrupted input z, the problem of maximum-likelihood decoding on a binary channel is to find the vector c closest in Hamming distance to z which satisfies the following parity-check equation over $\mathbb {F}$₂:

Hc^T = 0. (9)

We can translate Equation (4.1) into a satisfiability problem by associating each row in H with a clause of XOR'ed literals. Thus a row [1, 0, 0, 1, 0, 0, 1] might correspond to c₁ $\oplus$ c₄ $\oplus$ c₇, where c_i refers to the value of the i-th input symbol and $\oplus$ denotes XOR. Finding a maximum-likelihood decoding is thus akin to finding the fewest bit flips of z needed to satisfy the conjunction of the negation of these clauses. This translation into the realm of boolean formulae opens the door to a vast array of literature in computer science.