A Threshold for Unsatisfiability

摘要

A propositional formula is in 2-CNF (2-conjunctive normalform) iff it is the conjunction of clauses each of which has exactly two literals. We show: IfC=1+ε, whereε>0 is fixed andq(n)⩾C·n, then almost all formulas in 2-CNF withq(n) different clauses, wherenis the number of variables, are unsatisfiable. IfC=1−εandq(n)⩽C·n, then almost all formulas withq(n) clauses are satisfiable. By “almost all” we mean that the probability of the set of unsatisfiable or satisfiable formulas among all formulas withq(n) clauses approaches 1 asn→∞. SoC=1 gives us a threshold separating satisfiability and unsatisfiability of formulas in 2-CNF in a probabilistic, asymptotic sense. To prove our result we translate the satisfiability problem for formulas in 2-CNF into a graph theoretical question. Then we apply techniques from the theory of random graphs.