A threshold for unsatisfiability

Abstract

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: If C = 1 + ε, wheree ε > 0 is fixed and q(n) ≥ C · n, then almost all formulas in 2-CNF with q(n) different clauses, where n is the number of variables, are unsatisfiable. If C = 1 - ε and q(n) ≤ C · n, then almost all formulas with q(n) clauses are satisfiable. By "almost all" we mean that the probability of the set of unsatisfiable or satisfiable formulas among all formulas with q(n) clauses approaches 1 as n → ∞. So C = 1 gives us a threshold separating satisfiability and unsatisflability 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 tech niques from the theory of random graphs. © 1996 Academic Press, Inc.