A sharp threshold for the phase transition of a restricted Satisfiability problem for Horn clauses

In this paper we examine a variant, k-HSAT, of the well-known Satisfiabilit y problem, wherein formula instances are limited to CNF formulae having exa ctly k literals in each clause at most one of which is un-negated. Such for mulae correspond to sets of Horn clauses, each of which involves exactly k propositional variables. Tn addition, rather than seeking instantiations of the propositional variables that satisfy the formula, satisfying instantia tions having at least k - 1 variables set to I are required (such instantia tions being referred to as acceptable). Viewing formulae as sets of Horn cl auses, 'acceptable' instantiations are exactly those that correspond to 'no n-trivial models, i.e., those in which at least one rule has a true anteced ent. We show, using analytic methods, that k-HSA T exhibits a phase transit ion whose behavior is significantly different from that of the classical k- SAT problem concerning which various researchers have presented empirical e vidence for the existence of a constant theta (k) such that randomly chosen instances of k-SAT on n variables having m(n) clauses are 'almost certainl y' satisfiable if m(n)/n < <theta>(k) and 'almost certainly' unsatisfiable if m(n)/n > theta (k). In this paper we prove a sharp threshold result for k-HSAT for all fixed k greater than or equal to 2. Specifically, for theta (k) = (k - 1) (k + 1)/k! it is proved that if phi is chosen uniformly at ra ndom from instances of k-HSAT on n variables and m(n) clauses then [GRAPHICS] (C) 2001 Elsevier Science Inc. All rights reserved.