A sharp threshold for the renameable-Horn and the q-Horn properties Original Research Article

The sharp Satisfiability threshold is well known for random image-SAT formulas and is due to certain minimality and monotonic properties mentioned in this manuscript and reported in Chandru and Hooker [J. Assoc. Comput. Mach. 38 (1991) 205–221]. Whereas the Satisfiability threshold is on the probability that a satisfying assignment exists, we find that sharp thresholds also may be determined for certain formula structures, for example, the probability that a particular kind of cycle exists in a random formula. Such structures often have a direct relationship on the hardness of a formula because it is often the case that the presence of such a structure disallows a formula from a known, easily solved class of Satisfiability problems. We develop tools that should assist in determining threshold sharpness for a variety of applications. We use the tools to show a sharp threshold for the q-Horn and renameable-Horn properties.