A continuous–discontinuous second‐order transition in the satisfiability of random Horn‐SAT formulas
Cristopher Moore, Gabriel Istrate, Δημήτριος Δημόπουλος, Moshe Y. Vardi · Random Structures and Algorithms · 2007
Abstract We compute the probability of satisfiability of a class of random Horn‐SAT formulae, motivated by a connection with the nonemptiness problem of finite tree automata. In particular, when the maximum clause length is three, this model displays a curve in its parameter space, along which the probability of satisfiability is discontinuous, ending in a second‐order phase transition where it is continuous but its derivative diverges. This is the first case in which a phase transition of this type has been rigorously established for a random constraint satisfaction problem. © 2007 Wiley Periodicals, Inc. Random Struct. Alg., 2007