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: If C = 1 + epsilon, where epsilon > 0 is fixed and q(n) greater than or equal to 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 - epsilon and q(n) less than or equal to 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 --> infinity. So C = 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. (C) 1996 Academic Press, Inc.