Let F_k(n, m) denote a Boolean formula in Conjunctive Normal Form (CNF) with m clauses over n variables, whose clauses are chosen uniformly, independently and without replacement among all 2~k (n k) non-trivial clauses of length k, i.e., clauses with k distinct, non-complementary literals. Say that a sequence of random events E_n occurs with high probability (w.h.p.) if lim_(n→∞) Pr[E_n] = 1. Franco and Paull pioneered the analysis of random k-CNF formulas in, where they noted that F_k(n, m) is w.h.p. unsatisfiable if m = rn and r≥2~5 ln2. Chao and Franco complemented this by proving that if r＜2~k/k, then Unit Clause Propagation (UCP) alone finds a satisfying truth assignment w.h.p., thus establishing m = Θ(n) as the most interesting range for random k-SAT.
展开▼
