The Satisfiability Threshold

Initializing live version
Download to Desktop

Requires a Wolfram Notebook System

Interact on desktop, mobile and cloud with the free Wolfram Player or other Wolfram Language products.

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.

[more]

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 .

[less]

Contributed by: Ronald Monson (November 2012)
Open content licensed under CC BY-NC-SA


Snapshots


Details

Satisfiability is the canonical NP-complete problem and has received an intense amount of attention from researchers in theoretical computer science, probabilistic combinatorics, statistical physics, and artificial intelligence.

The overriding motivation for studying these thresholds comes from the observation that hard, random SAT formulas tend to congregate at this threshold. Consequently, hard random instances can be readily harvested as part of trying to unravel the complexity of general heuristic search procedures.

This threshold was first observed statistically in the early 1990's by inferring the value of from the proportion of satisfiable formulas in randomly generated samples (as determined by complete SAT solvers and often involving hundreds of variables). The graphs here, on the other hand, are exact and continuous in coming from closed-form formulas, although naturally for much smaller values of . In fact, the complexity of the generating algorithm suggests that obtaining closed-form formulas for will be extremely difficult and almost certainly impossible for *.

Nonetheless, this Demonstration illustrates that exact formulations of even the smallest values of can reveal structures of relevance to higher-dimensional problems, as well as opening the possibility of leveraging analytical tools to further understand such structures.

*Two different algorithms for generating closed-form formulas for each value of appear independently in Harris (2002) (with formulas for ) and in Monson (2003) & (2004) (with formulas for ). Harris's (2002) algorithm is derived from certain computer science machinery while Monson's (2004) algorithm incorporates results from discrete mathematics (the output of which is the one used in this Demonstration).

References

[1] M. Harris, Thresholds and Symmetries in Propositional Formulas, PhD thesis, University of Illinois, Urbana-Champaign, 2002.

[2] R. Monson, "Generating Closed-Form Formulae that Count Satisfiable Instances of k-SAT," in Challenging the Boundaries of Symbolic Computation, Proceedings of the Fifth International Mathematica Symposium, London: Imperial College, 2003 pp. 279–287.

[3] R. Monson, The Computer-Aided Verification of Mathematical Reasoning in Education and the Counting of Satisfiable Instances of k-SAT, PhD thesis, University of Western Australia, Australia, 2004.

[4] S. Kirkpatrick and B Selman, "Critical Behaviour in the Satisfiability of Random Boolean Expressions," Science, 264(5163), 1994 pp. 1297–1301.

[5] P. Cheeseman, B Kanefsky, and W.M. Taylor, "Where the Really Hard Problems Are," in Proceedings of the 12th IJCAI, Morgan Kaufmann, 1991 pp. 331–337.

[6] M. Molloy, "Thresholds for Colourability and Satisfiability for Random Graphs and Boolean Formulae," Surveys in Combinatorics (J. Hirschfield, ed.), New York: Cambridge University Press, 2001 pp. 165–197.

[7] R Monasson and R. Zecchina, "Statistical Mechanics of the Random K-Satisfiability Model," Physical Review E, 56(2), 1997 pp. 1357–1370.

[8] E. Friedgut, "Sharp Thresholds of Graph Properties, and the k-SAT Problem," Journal of the American Mathematical Society, 12(4), 1999 pp. 1017–1054.



Feedback (field required)
Email (field required) Name
Occupation Organization
Note: Your message & contact information may be shared with the author of any specific Demonstration for which you give feedback.
Send