9846

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.
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 .

THINGS TO TRY

SNAPSHOTS

  • [Snapshot]
  • [Snapshot]
  • [Snapshot]

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.
    • Share:

Embed Interactive Demonstration New!

Just copy and paste this snippet of JavaScript code into your website or blog to put the live Demonstration on your site. More details »

Files require Wolfram CDF Player or Mathematica.









 
RELATED RESOURCES
Mathematica »
The #1 tool for creating Demonstrations
and anything technical.
Wolfram|Alpha »
Explore anything with the first
computational knowledge engine.
MathWorld »
The web's most extensive
mathematics resource.
Course Assistant Apps »
An app for every course—
right in the palm of your hand.
Wolfram Blog »
Read our views on math,
science, and technology.
Computable Document Format »
The format that makes Demonstrations
(and any information) easy to share and
interact with.
STEM Initiative »
Programs & resources for
educators, schools & students.
Computerbasedmath.org »
Join the initiative for modernizing
math education.
Step-by-step Solutions »
Walk through homework problems one step at a time, with hints to help along the way.
Wolfram Problem Generator »
Unlimited random practice problems and answers with built-in Step-by-step solutions. Practice online or make a printable study sheet.
Wolfram Language »
Knowledge-based programming for everyone.
Powered by Wolfram Mathematica © 2014 Wolfram Demonstrations Project & Contributors  |  Terms of Use  |  Privacy Policy  |  RSS Give us your feedback
Note: To run this Demonstration you need Mathematica 7+ or the free Mathematica Player 7EX
Download or upgrade to Mathematica Player 7EX
I already have Mathematica Player or Mathematica 7+