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}$2:

HcT = 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 c1 $ \oplus$ c4 $ \oplus$ c7, where ci 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.