The phase transition in random horn satisfiability and its algorithmic implications
Gabriel Istrate · Random Structures and Algorithms · 2002
Abstract Letc> 0 be a constant, and Φ be a random Horn formula withnvariables andm=c· 2nclauses, chosen uniformly at random (with repetition) from the set of all nonempty Horn clauses in the given variables. By analyzing PUR, a natural implementation of positive unit resolution, we show that limn→∞Pr(Φ is satisfiable) = 1 −F(e−c), whereF(x) = (1 −x)(1 −x2)(1 −x4)(1 −x8) …. Our method also yields as a byproduct an average‐case analysis of this algorithm. Published 2002 Wiley Periodicals, Inc. Random Struct. Alg., 20: 483–506, 2002