The Satisfiability Threshold
The Satisfiability Threshold
The emergence of the so-called satisfiability threshold can be discerned by plotting closed-form formulas for , the proportion of satisfiable conjunctive normal form (CNF) formulas with clauses containing literals over variables, for . It is to be expected that random CNF formulas with more clauses (constraints) are more likely to be unsatisfiable, but perhaps what is more surprising is how quickly such a transition occurs. The 3-SAT threshold conjecture asserts that, roughly, for clauses with three literals and sufficiently large , virtually all CNF formulas with less than clauses will be satisfiable, whereas for CNF formulas with more than clauses, virtually all will be unsatisfiable.
k,m
n
m
k
n
n=2,3,4
n
~4.2n
~4.2n
The threshold conjecture is illustrated with the thick red line and involves fixing , the clause size. Observe however, the emergence of "orthogonal thresholds" that arise instead from fixing the normalized clause number , the number of clauses as a multiple of .
k
c
n