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

[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," J

*ournal of the American Mathematical Society*,

**12**(4), 1999 pp. 1017–1054.