Satisfiability Coding Lemma

We present and analyze two simple algorithms for finding satisfying assignments of /spl kappa/-CNFs (Boolean formulae in conjunctive normal form with at most /spl kappa/ literals per clause). The first is a randomized algorithm which, with probability approaching 1, finds a satisfying assignment of a satisfiable /spl kappa/-CNF formula F in time O(n/sup 2/|F|2/sup n-n//spl kappa//). The second algorithm is deterministic, and its running time approaches 2/sup n-n/2/spl kappa// for large n and /spl kappa/. The randomized algorithm is the best known algorithm for /spl kappa/>3; the deterministic algorithm is the best known deterministic algorithm for /spl kappa/>4. We also show an /spl Omega/(n/sup 1/4/2/sup /spl radic/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 /spl kappa/-CNF succinctly.

Authors

• Ramamohan Paturi
• Pavel Pudlák
• Francis Zane

Keywords

• Algorithm design and analysis
• Polynomials
• Upper bound
• Computer science
• Galois fields
• Input variables
• Switching circuits
• Circuit analysis computing
• Lower Bound
• Running Time
• OR Gate
• Permutation
• Greater Than Or Equal
• Efficient Algorithm
• Criterion Variables
• Variables In Order
• Random Permutations
• Short Description
• Probability Space
• Minimal Solution
• Successive Algorithm
• Induction Hypothesis
• Decoding Algorithm