Wikimore

Summary

DescriptionSatComplexity.pdf	English: Exponential complexity of SAT solving vs variable count (for 3-SAT), clause count, and formula length (i.e., total literal count).
Date	25 September 2025
Source	Own work
Author	Jochen Burghardt
Other versions	File:SatComplexity.pdf * File:SatComplexity svg.svg

Gnuplot source code

set xrange [1979:2025]
set yrange [1.05:1.65]
set encoding iso_8859_1
set xtics 5 font "Sans Serif,15"
set ytics 1.05, 0.05, 1.70 font "Sans Serif,15"
set mxtics 5
set mytics 5
set format y "%4.2f"
set xlabel "Year" font "Sans Serif,15"
set ylabel "Base" font "Sans Serif,15"
set grid
set title "Exponential complexity of SAT solving vs ..." offset 65,0
set key top right

# variable count, for 3-SAT:
$dataN <<EOFn
#1985   2   
1985    1.6181                  "Monien, Speckenmeyer   "               ""
1992    1.6181
1992    1.579                   "Schiermeyer   "                        ""
1999    1.579
1999    1.505                   ""              "   Kullmann"
2002    1.505
2002    1.5                     "Dantsin, Goerdt, Hirsch, Kannan, ...   "               ""
#2002   1.5                     ""              "   Dantsin, Goerdt, Hirsch, Kannan, Kleinberg, Papadimitriou, Raghavan, Schöning"
2004    1.5 
2004    1.473                   ""              "   Brüggemann, Kern"
2008    1.473
2008    1.465                   ""              "   Scheder"
2011    1.465
2011    1.33334                 ""              "   Moser, Scheder"
2013    1.33334
2013    1.3303                  ""              "   Makino, Tamaki, Yamamoto"
2018    1.3303
2018    1.3279                  ""              "   Liu"
2026    1.3279
EOFn

# clause count:
$dataM <<EOFm
#1980   2   
1980    1.2599210499            ""              "   Monien, Speckenmeyer"
#1980   1.2599210499            ""              "   Monien, Speckenmeyer, Vornberger"
1998    1.2599210499
1998    1.2388                  ""              "   Hirsch"
2005    1.2388
2005    1.234                   ""              "   Yamamoto"
2021    1.234
2021    1.2226                  ""              "   Chu, Xiao, ..."
#2021   1.2226                  ""              "   Chu, Xiao, Zhang"
2026    1.2226
EOFm

# formula length:
$dataL <<EOFl
#1988   2   
1988    1.0927                  ""              "   Van Gelder"
1997    1.0927
1997    1.0800597389            ""              "   Kullmann, Luckhardt"
1998    1.0800597389
1998    1.07577                 ""              "   Hirsch"
2000    1.07577
2000    1.074                   ""              "   Hirsch"
2005    1.074
2005    1.0663                  ""              "   Wahlström"
2009    1.0663
2009    1.0652                  ""              "   Chen, Liu"
2022    1.0652
2022    1.0638                  ""              "   Peng, Xiao"
2026    1.0638
EOFl

  plot $dataN using 1:2   title '... variable count (3-SAT only)' with linespoints lc 6 lw 3 pt 7
replot $dataN using 1:2:4 title ''                                with labels rotate by 60 left  font "Sans Serif,15" tc rgbcolor 0x0072b2
replot $dataN using 1:2:3 title ''                                with labels rotate by 60 right font "Sans Serif,15" tc rgbcolor 0x0072b2

replot $dataM using 1:2   title '... clause count'                with linespoints lc 7 lw 3 pt 7
replot $dataM using 1:2:4 title ''                                with labels rotate by 60 left  font "Sans Serif,15" tc rgbcolor 0xe51e10
replot $dataM using 1:2:3 title ''                                with labels rotate by 60 right font "Sans Serif,15" tc rgbcolor 0xe51e10

replot $dataL using 1:2   title '... formula length'              with linespoints lc 2 lw 3 pt 7
replot $dataL using 1:2:4 title ''                                with labels rotate by 60 left  font "Sans Serif,15" tc rgbcolor 0x009e73
replot $dataL using 1:2:3 title ''                                with labels rotate by 60 right font "Sans Serif,15" tc rgbcolor 0x009e73

pause -1

Cited papers

Variable count

Burkhard Monien and Ewald Speckenmeyer (1985). "Solving satisfiability in less than $2^{n}$ steps". Discrete Applied Mathematics 10: 287–295.

Ingo Schiermeyer (1992) "International Workshop on Computer Science Logic" in Solving 3-Satisfiability in Less than $1.579^{n}$ Steps, LNCS, 702, Springer, pp. 379–394

Oliver Kullmann (1999). "New Methods for 3-SAT Decision and Worst-Case Analysis". Theoretical Computer Science 223: 1–72.

Evgeny Dantsin and Andreas Goerdt and Edward A. Hirsch and Ravi Kannan and Jon Kleinberg and Christos Papadimitriou and Prabhakar Raghavan and Uwe Schöning (Oct 2002). "A Deterministic $(2-2/(k+1))^{n}$ Algorithm for $k$ -SAT Based on Local Search". Theoretical Computer Science 289: 69–83.

Tobias Brüggemann and Walter Kern (2004). "An Improved Deterministic Local Search Algorithm for $3$ -SAT". Theoretical Computer Science 329: 303–313.

Dominik Scheder (2008) "3rd Latin American Theoretical Informatics Symposium (LATIN)" in Guided Search and a Faster Deterministic Algorithm for 3-SAT, pp. 60–71 DOI: 10.1007/978-3-540-78773-0_6.

Robin A. Moser and Dominik Scheder (Jun 2011) "Proc. 43rd Ann. Symp. on Theory of Computing, STOC" in Lance Fortnow and Sadil Vadhan, ed. A Full Derandomization of Schöning's $k$ -SAT Algorithm, pp. 245–252 DOI: 10.1145/1993636.1993670.

Kazuhisa Makino and Suguru Tamaki and Masaki Yamamoto (2013). "Derandomizing the HSSW Algorithm for 3-SAT". Algorithmica 67: 112–124. DOI:10.1007/s00453-012-9741-4.
S. Liu (Jul 2018) "Proc. ICALP" in I. Chatzigiannakis and C. Kaklamanis and D. Marx and D. Sannella, ed. Chain, Generalization of Covering Code, and Deterministic Algorithm for $k$ -SAT, LIPIcs, 107, Schloss Dagstuhl, pp. 88:1–13 DOI: 10.4230/LIPIcs.ICALP.2018.88.

Clause count

Burkhard Monien and Ewald Speckenmeyer (1980). Upper bounds for covering problems (Reihe Theoretische Informatik). Universität-Gesamthochschule-Paderborn.

Edward A. Hirsch (Jan 1998) "Proceedings of the Ninth Annual ACM-SIAM Symposium on Discrete Algorithms" in H. J. Karloff, ed. Two New Upper Bounds for SAT, ACM/SIAM, pp. 521–530

M. Yamamoto (2005) "Algorithms and Computation, Proc. 16th International Symposium, ISAAC" in X. Deng and D. Du, ed. An Improved $O(1.234^{m})$ -Time Deterministic Algorithm for SAT, Lecture Notes in Computer Science, 3827, Springer, pp. 644–653 DOI: 10.1007/11602613_65.

Huairui Chu and Mingyu Xiao and Zhe Zhang (Jul 2020). An improved upper bound for SAT (Technical Report). arxiv. arXiv:2007.03829.

Huairui Chu and Mingyu Xiao and Zhe Zhang (Oct 2021). "An improved upper bound for SAT". Theoretical Computer Science 887: 51–62. DOI:10.1016/j.tcs.2021.06.045.

Formula length

A. Van Gelder (1988). "A Satisfiability Tester for Non-Clausal Propositional Calculus". Inf. Comput. 79: 1–21. DOI:10.1016/0890-5401(88)90014-4.

O. Kullmann and H. Luckhardt (1997). "Deciding propositional tautologies: Algorithms and their complexity". Information and Computation. [Remark: was submitted for Information and Computation, but didn't appear there]

Hirsch 1998, see above

Edward A. Hirsch (May 2000). "New worst-case upper bounds for SAT". J. Autom. Reason. 24: 397–420. DOI:10.1023/A:1006340920104.

Magnus Wahlström (Oct 2005) "Algorithms – Proc. 13th Ann. European Symp. (ESA)" in G.S. Brodal and S. Leonardi, ed. An Algorithm for the SAT Problem for Formulae of Linear Length, Lecture Notes in Computer Science, 3669, Springer, pp. 107–118 DOI: 10.1007/11561071_12.

Magnus Wahlström (Mar 2007) Algorithms, Measures and Upper Bounds for Satisfiability and Related Problems (Ph.D. thesis), ISBN ISBN 978-91-85715-55-8

Jianer Chen and Yang Liu (Aug 2009) "Algorithms and Data Structures, Proc. 11th International Symposium (WADS)" in F.K.H.A. Dehne and M.L. Gavrilova and J. Sack and C.D. Toth, ed. An improved SAT algorithm in terms of formula length, Lecture Notes in Computer Science, 5664, Springer, pp. 144–155 DOI: 10.1007/978-3-642-03367-4_13.

Junqiang Peng and Mingyu Xiao (Aug 2022). Further improvements for SAT in terms of formula length (Technical Report). arXiv. arXiv:2105.06131.

Licensing

I, the copyright holder of this work, hereby publish it under the following license:

	This file is made available under the Creative Commons CC0 1.0 Universal Public Domain Dedication.
	The person who associated a work with this deed has dedicated the work to the public domain by waiving all of their rights to the work worldwide under copyright law, including all related and neighboring rights, to the extent allowed by law. You can copy, modify, distribute and perform the work, even for commercial purposes, all without asking permission. CC0falsefalse