Satisfiability Coding Lemma

We present and analyze two simple algorithms for finding satisfying assignments of κ-CNFs (Boolean formulae in conjunctive normal form with at most κ literals per clause). The first is a randomized algorithm which, with probability approaching 1, finds a satisfying assignment of a satisfiable κ-CNF formula F in time O(n ²|F|2^n-nκ/). The second algorithm is deterministic, and its running time approaches 2^n-n/2κ for large n and κ. The randomized algorithm is the best known algorithm for κ>3; the deterministic algorithm is the best known deterministic algorithm for κ>4. We also show an Ω(n^1/42^√n) lower bound on the size of depth 3 circuits of AND and OR gates computing the parity function. This bound is tight up to a constant factor. The key idea used in these upper and lower bounds is what we call the Satisfiability Coding Lemma. This basic lemma shows how to encode satisfying solutions of a κ-CNF succinctly