<p>There are two kinds of &quot;best&quot; SAT solvers, one for theory, one for practice.</p>
<h3>Theory</h3>
<ul>
<li>Kazuo Iwama, Kazuhisa Seto, Tadashi Takai, Suguru Tamaki, &quot;<a href="http://dx.doi.org/10.1007/978-3-642-17517-6_9" rel="noreferrer">Improved Randomized Algorithms for 3-SAT</a>&quot;, ISAAC 2010.</li>
</ul>
<blockquote>
<p>randomized <span class="math-container">$O(1.32113^n)$</span> for 3SAT.</p>
</blockquote>
<ul>
<li>Timon Hertli, Robin A. Moser, Dominik Scheder, &quot;<a href="http://arxiv.org/abs/1009.4830" rel="noreferrer">Improving PPSZ for 3-SAT using Critical Variables</a>&quot;, 2011.</li>
</ul>
<blockquote>
<p>randomized <span class="math-container">$O(1.321^n)$</span> for 3SAT.</p>
</blockquote>
<ul>
<li>Konstantin Kutzkov, Dominik Scheder, &quot;<a href="http://arxiv.org/abs/1007.1166" rel="noreferrer">Using CSP To Improve Deterministic 3-SAT</a>&quot;, 2010.</li>
</ul>
<blockquote>
<p>deterministic <span class="math-container">$O(1.439^n)$</span> for 3SAT.</p>
</blockquote>
<h3>Practice</h3>
<p>Check <a href="http://www.satcompetition.org/" rel="noreferrer">SAT conference</a> for competition results for each year.</p>

CC BY-SA 3.0
2012-01-07T18:59:14.663Z
Yet another update: in FOCS 2011, Timon Hertli (http://arxiv.org/abs/1103.2165) proved that the PPSZ algorithm solves every 3SAT instance in $1.308^n$ time.
Ryan Williams
CC BY-SA 2.5
2010-09-09T15:51:27.300Z
I found a link to [Iwama et al. paper](http://www.lab2.kuis.kyoto-u.ac.jp/~tamak/isaac2010.pdf). So, is $O(1.32113^n)$ really the latest and best result for solving SAT up until now?
Sadeq Dousti
CC BY-SA 2.5
2010-09-10T00:20:54.843Z
@ Sadeq: I think so, but just for 3-SAT, not SAT.
Tian Liu
CC BY-SA 2.5
2010-09-28T05:42:07.727Z
Now the best algorithm is in $O(1.321^n)$ time by Timon Hertli, Robin A. Moser and Dominik Scheder.
Tian Liu
CC BY-SA 3.0
2010-09-08T00:33:33.803Z
2014-02-11T03:09:03.980Z
2020-06-17T09:38:08.363Z
Tian Liu
<p>Schoening's algorithm is a probabilistic algorithm for k-SAT with running time $O(a^n)$, where $a = 2(k-1)/k$. This results in an $O(1.33334^n)$ algorithm for 3SAT, an $O(1.5^n)$ algorithm for 4SAT, etc.</p>

<p>The algorithm has also been (almost completely) derandomized by Moser and Scheder, who give a deterministic algorithm for solving kSAT running time $O((a+\epsilon)^n)$ where $a$ is the same constant as before, and $\epsilon>0$ can be made arbitrarily small.</p>

<p>Note: In this answer the big Oh notation hides poly(n) factors. I wanted to use the $O^*$ notation, but it isn't rendering properly.</p>

CC BY-SA 2.5
2010-09-07T23:45:26.047Z
Why do you say "almost completely"?  Did I miss something in the paper?
András Salamon
CC BY-SA 2.5
2010-09-08T00:06:34.413Z
There is a deterministic $O((2 - \frac{2}{k + 1})^n)$ algorithm for k-SAT by eight people, so please forgive me not mentioning all of them. Here is the link: http://linkinghub.elsevier.com/retrieve/pii/S0304397501001748. So for $k = 3$ we have $O(1.5^n)$ and it is not as good as other bounds for 3-SAT presented here, but for k-SAT it is the best, as far as I know.
Grigory Yaroslavtsev
CC BY-SA 2.5
2010-09-08T01:26:31.913Z
I said "almost completely" just to indicate that there's an epsilon factor there. I guess one would expect that a complete derandomization achieves the same run time (upto polynomial factors). Or maybe that's unreasonable to expect.
Robin Kothari
CC BY-SA 2.5
2010-09-08T01:28:38.510Z
@Grigory Yaroslavtsev: Isn't the Moser-Scheder deterministic algorithm for kSAT that I mentioned faster that the one you quoted? Am I missing something?
Robin Kothari
CC BY-SA 2.5
2010-09-08T03:15:44.300Z
I was just worried about this $\epsilon$ in your notation, so it is faster indeed. It looks like the paper appeared on arXiv just a few days ago: http://arxiv.org/PS_cache/arxiv/pdf/1008/1008.4067v1.pdf, so no wonder I didn't know about it.
Grigory Yaroslavtsev
CC BY-SA 2.5
2010-09-07T19:37:35.573Z
2010-09-07T19:37:35.573Z
Robin Kothari
<p>As was already mentioned, if you are interested in theoretical running time guarantees, this question is a duplicate.</p>

<p>But I'd like to point out that if you really want to solve a concrete problem (like the colouring problem that you mentioned), I think that it makes absolutely no sense at all to study theoretical upper bounds.</p>

<p>Even though you wanted to avoid "engineering" aspects, I'd suggest that you just take some popular SAT solvers, try them out, and see what happens (most of them can read the same DIMACS file format, so it is easy to try different solvers). You may have both positive and negative surprises. Recently I had a family of SAT instances; a bunch of instances with tens of thousands of variables and more than one million clauses turned out to be easy to solve, while seemingly much simpler instances with just hundreds of variables and thousands of clauses were far too difficult for any solver that I tried.</p>

CC BY-SA 2.5
2010-09-27T17:10:08.480Z
In addition to Jukka's summary, it is also worth noting that there are two main kinds of SAT solvers: those based on survey propagation, which work well for random SAT instances, and those which use clause learning combined with unit resolution, which tend to work well to discover combinatorial structure.  These have quite different behaviour.  The worst cases for SAT solvers tend to be instances that are not satisfiable, but where the space of nogoods has complex structure that does not allow much pruning.  Unfortunately instances from combinatorics tend to be of this kind.
András Salamon
CC BY-SA 2.5
2010-09-27T16:51:23.950Z
2010-09-27T16:51:23.950Z
Jukka Suomela
<ul>
<li>Timon Hertli, "<a href="http://arxiv.org/abs/1103.2165">3-SAT Faster and Simpler - Unique-SAT Bounds for PPSZ Hold in General</a>", FOCS 2011.</li>
</ul>

<blockquote>
  <p>deterministic $O(1.308^n)$ for 3SAT.</p>
</blockquote>

CC BY-SA 3.0
2014-02-09T01:52:40.583Z
I assume that when somebody comes up with a better upper bound they would cite this paper. There has been only once citation to this paper, which is "A Satisfiability Algorithm and Average-Case Hardness for Formulas over the Full Binary Basis" And they seem to talk about only certain types of formulas. Therefore, this seems to be the best Upper Bound thus far.
Tayfun Pay
CC BY-SA 3.0
2014-02-10T02:09:04.350Z
@RickyDemer Uhuh! is it a better bound than this? Notation is not so clear to me.
Tayfun Pay
CC BY-SA 3.0
2014-02-07T22:21:25.243Z
2014-02-11T03:10:06.577Z
2014-02-11T03:10:06.577Z
Kaveh
<p>It is impossible for 3SAT to have sub-exponential algorithms unless the <a href="http://en.wikipedia.org/wiki/Exponential_time_hypothesis" rel="nofollow">exponential time hypothesis</a> is false.</p>

<ul>
<li>Kazuo Iwama, Suguru Tamaki, <a href="http://portal.acm.org/citation.cfm?id=982838" rel="nofollow">Improved upper bounds for 3-SAT</a>, 2004.</li>
</ul>

<blockquote>
  <p>randomized algorithm with expected running time $O({1.324}^n)$ for 3SAT.</p>
</blockquote>

<ul>
<li>Daniel Rolf, <a href="http://eccc.hpi-web.de/report/2005/159/" rel="nofollow">Improved Bound for the PPSZ/Schoning-Algorithm for 3-SAT</a>, 2005.</li>
</ul>

<blockquote>
  <p>randomized algorithm with expected running time $O({1.32216}^n)$ for 3SAT.</p>
</blockquote>

CC BY-SA 2.5
2010-09-07T19:19:14.040Z
Isn’t that a tautology?
Tsuyoshi Ito
CC BY-SA 2.5
2010-09-07T19:59:02.727Z
Yes, that is a tautology: The exponential time hypothesis (ETH) is that 3SAT, the satisfiability problem of Boolean formulas in conjunctive normal form with at most three literals per clause and with n variables, cannot be solved in time $2^{o(n)}$. (See: [wikipedia](http://en.wikipedia.org/wiki/Time_complexity#Exponential_time_hypothesis)).
Sadeq Dousti
CC BY-SA 2.5
2010-09-07T20:14:08.927Z
The work of Kazuo Iwama et al. (2004) is newer than that of Schoening's (1999). I wonder if even more recent results are available.
Sadeq Dousti
CC BY-SA 2.5
2010-09-07T21:51:00.753Z
To avoid possibility of confusion, my last comment refers to the first sentence of the answer: “It is impossible for 3SAT to have sub-exponential algorithms unless the exponential time hypothesis (ETH) is false.”  My understanding is that the exponential-time hypothesis is the very hypothesis stating that there is no algorithm for 3SAT whose running time is subexponential (i.e. 2^{o(n)}) in the number of variables.
Tsuyoshi Ito
CC BY-SA 2.5
2010-09-08T01:29:54.543Z
And to avoid further confusion, I will add that when Tsuyoshi posted his comment, the answer only contained that one sentence, which made his comment very appropriate.
Robin Kothari
CC BY-SA 3.0
2010-09-07T19:15:40.080Z
2014-02-11T03:15:26.817Z
2014-02-11T03:15:26.817Z
Mohammad Al-Turkistany
<p>This <a href="https://cstheory.stackexchange.com/questions/1060/best-upper-bounds-on-sat">post</a> deals with upper bounds on SAT. This <a href="https://cstheory.stackexchange.com/questions/93/what-are-the-best-current-lower-bounds-on-3sat">one</a> deals with best lower bounds. This <a href="http://www.satcompetition.org/" rel="nofollow noreferrer">link</a> gives details of the annual competition comparing SAT solver implementations, which are all downloadable. For simplicity, you could start with <a href="http://www.sat4j.org/" rel="nofollow noreferrer">SAT4J</a>, a Java based library for SAT solving.</p>

CC BY-SA 2.5
2011-04-07T07:55:03.813Z
I'm not sure if I would recommend sat4J, not only it is significantly slower than the state-of-the-art but also somewhat more complex. It is true, however, that it is nicely customizable due to the object-oriented structure. MiniSat is very nicely written and 2.2 is state-of-the-art.
Mikolas
CC BY-SA 2.5
2010-09-27T14:55:42.790Z
Turns out this question *was* already asked before; I just didn't see it when I searched the website. Tian Liu's response on the upper bounds question is exactly what I was looking for. Thanks for the links, dave!
Daniel Apon
CC BY-SA 2.5
2010-09-27T14:59:47.120Z
This is evidence that I spend too much time here ;-)
Dave Clarke
CC BY-SA 2.5
2010-09-28T02:52:58.067Z
we're glad that you do :)
Suresh Venkat
CC BY-SA 2.5
2010-09-27T14:51:47.333Z
2010-09-27T14:51:47.333Z
2017-04-13T12:32:28.743Z
Dave Clarke
<p>The best deterministic algorithm for 3-SAT now has upper bound 1.32793^n, see <a href="https://arxiv.org/abs/1804.07901" rel="noreferrer">https://arxiv.org/abs/1804.07901</a> by Sixue Liu. Basically the upper bounds for all k-SAT have been improved in this paper.</p>

CC BY-SA 4.0
2018-09-21T01:41:57.093Z
2018-09-21T01:41:57.093Z
ON KI Wong
<p>The best algorithm for 3-SAT now has numerical upper bound <span class="math-container">$O^{*}(1.306995^n)$</span> on unique-3-SAT and on general-3-SAT it is also fastest but now the specific values have not been analyzed yet. </p>

<p>Authors say they <em>hope</em> the improved bounds for unique-3-SAT also apply directly to 3-SAT by using essentially the arguments of Hertli.</p>

<p>The algorithm is described in this paper:</p>

<blockquote>
  <p>Thomas Dueholm Hansen, Haim Kaplan, Or Zamir, Uri Zwick, <a href="https://doi.org/10.1145/3313276.3316359" rel="noreferrer">Faster k-SAT algorithms using biased-PPSZ</a>, 2019</p>
</blockquote>

<p>Simply speaking, it adds bias to the PPSZ algorithm to let some literals have a higher, lower or equal probability to turn to some value.</p>

<p>In the paper, they say that the derandomization of this algorithm may be not very hard and moreover, they believe this algorithm can achieve <span class="math-container">$O^{*}(1.30331^n)$</span> for 3-SAT.</p>

<p>For future work, they say there is a more challenging way to obtian further improvements by guessing more varibles biasedly <em>without</em> using a set of disjoint clauses as a scaffolding that simplifies analysis.</p>

<p>In the paper, the problem whether bound for k-SAT can be of form <span class="math-container">${2^{\left(1 - \frac{\omega (1)}{k}\right)n}}$</span> is proposed by authors and is <em>believed</em> to be more important than just giving a better constant bound for 3-SAT. </p>

CC BY-SA 4.0
2020-03-20T09:05:20.157Z
2020-04-15T01:26:40.183Z
2020-04-15T01:26:40.183Z
Bubble
<p>In <a href="https://cstheory.stackexchange.com/q/93/873">another thread</a>, Joe Fitzsimons asked about "the best current lower bounds on 3SAT."</p>

<p>I'd like to go the other way: What's the best current <b>upper</b> bounds on 3SAT? In other words, what is the time complexity of the most efficient SAT solver?</p>

<p>In particular, is it conceivable to find a sub-exponential (yet super-polynomial) algorithm for SAT?</p>

CC BY-SA 2.5
2011-03-21T20:35:16.853Z
**mod note**: merging [another question](http://cstheory.stackexchange.com/q/1719/) with this one. The comments under that question will also be transfered above as a result of the merge. I remove those comments which do not apply anymore.
Kaveh
CC BY-SA 2.5
2010-09-07T19:10:47.413Z
I don't know about analytic results, but you can find experimental results here http://baldur.iti.uka.de/sat-race-2010/results.html (see the "HTML" links)
Radu GRIGore
CC BY-SA 2.5
2010-09-25T13:30:49.787Z
this question title is a bit misleading, because of the existence of this question: http://cstheory.stackexchange.com/questions/1295/sat-solver-download . I think you might rephrase as 'Best Upper Bounds on SAT' ?
Suresh Venkat
CC BY-SA 2.5
2010-09-25T16:44:12.100Z
@Suresh: The question you are referring to relates to "#SAT", while this one corresponds to SAT. In addition, that question was asked about a week after this one. Anyhow, do you still suggest changing this ones' title?
Sadeq Dousti
CC BY-SA 2.5
2010-09-25T18:00:02.983Z
yes, because a "SAT Solver" is a specific well known object - an actual codebase for solving SAT. Google will get confused and redirect people looking for code over here :).
Suresh Venkat
CC BY-SA 2.5
2010-09-26T02:27:47.287Z
Well, I didn't see it from that viewpoint! I agree with you, and changed the the title accordingly. Yet, there are links below to "actual codebases for solving SAT," such as http://www.satcompetition.org/
Sadeq Dousti
CC BY-SA 2.5
2010-09-27T17:19:57.900Z
Regarding the motivation for this question, I thought several people had tried SAT solvers on the 17x17 instances.  It seems to be the frontier of what can be handled with a SAT solver.  You could instead try a parallel solver, but I was under the impression based on Bill Gasarch's posts that you would need a large-scale effort.  You could also apply an SMT solver with a suitable theory, or use a constraint solver that implements a global constraint that has an efficient propagator.  In each of these cases the new idea would be to express an important property that is hard to do using clauses.
András Salamon
CC BY-SA 2.5
2010-09-27T18:31:39.697Z
Interesting insights, thanks Andras. I agree that it will take a large-scale effort.
Daniel Apon
<cc.complexity-theory><ds.algorithms><sat><upper-bounds>
Best Upper Bounds on SAT
Sadeq Dousti
# Best Upper Bounds on SAT

(Asked by: username_0 on 2010-09-07)

In [another thread](https://cstheory.stackexchange.com/q/93/873), Joe Fitzsimons asked about "the best current lower bounds on 3SAT."

I'd like to go the other way: What's the best current **upper** bounds on 3SAT? In other words, what is the time complexity of the most efficient SAT solver?

In particular, is it conceivable to find a sub-exponential (yet super-polynomial) algorithm for SAT?

**Tags:** cc.complexity-theory, ds.algorithms, sat, upper-bounds
> **Comments:**
> **username_2**: I don't know about analytic results, but you can find experimental results here http://baldur.iti.uka.de/sat-race-2010/results.html (see the "HTML" links)  
> **username_3**: this question title is a bit misleading, because of the existence of this question: http://cstheory.stackexchange.com/questions/1295/sat-solver-download . I think you might rephrase as 'Best Upper Bounds on SAT' ?  
> **username_0**: @Suresh: The question you are referring to relates to "#SAT", while this one corresponds to SAT. In addition, that question was asked about a week after this one. Anyhow, do you still suggest changing this ones' title?  
> **username_3**: yes, because a "SAT Solver" is a specific well known object - an actual codebase for solving SAT. Google will get confused and redirect people looking for code over here :).  
> **username_0**: Well, I didn't see it from that viewpoint! I agree with you, and changed the the title accordingly. Yet, there are links below to "actual codebases for solving SAT," such as http://www.satcompetition.org/  
> **username_4**: Regarding the motivation for this question, I thought several people had tried SAT solvers on the 17x17 instances.  It seems to be the frontier of what can be handled with a SAT solver.  You could instead try a parallel solver, but I was under the impression based on Bill Gasarch's posts that you would need a large-scale effort.  You could also apply an SMT solver with a suitable theory, or use a constraint solver that implements a global constraint that has an efficient propagator.  In each of these cases the new idea would be to express an important property that is hard to do using clauses.  
> **username_5**: Interesting insights, thanks Andras. I agree that it will take a large-scale effort.  
> **username_1**: **mod note**: merging [another question](http://cstheory.stackexchange.com/q/1719/) with this one. The comments under that question will also be transfered above as a result of the merge. I remove those comments which do not apply anymore.  

---

## 8 answers

### Answer by username_17 on 2020-03-20. Score: 15 | Accepted answer

The best algorithm for 3-SAT now has numerical upper bound $O^{\*}(1.306995^n)$ on unique-3-SAT and on general-3-SAT it is also fastest but now the specific values have not been analyzed yet.

Authors say they *hope* the improved bounds for unique-3-SAT also apply directly to 3-SAT by using essentially the arguments of Hertli.

The algorithm is described in this paper:

> Thomas Dueholm Hansen, Haim Kaplan, Or Zamir, Uri Zwick, [Faster k-SAT algorithms using biased-PPSZ](https://doi.org/10.1145/3313276.3316359), 2019

Simply speaking, it adds bias to the PPSZ algorithm to let some literals have a higher, lower or equal probability to turn to some value.

In the paper, they say that the derandomization of this algorithm may be not very hard and moreover, they believe this algorithm can achieve $O^{\*}(1.30331^n)$ for 3-SAT.

For future work, they say there is a more challenging way to obtian further improvements by guessing more varibles biasedly *without* using a set of disjoint clauses as a scaffolding that simplifies analysis.

In the paper, the problem whether bound for k-SAT can be of form ${2^{\left(1 - \frac{\omega (1)}{k}\right)n}}$ is proposed by authors and is *believed* to be more important than just giving a better constant bound for 3-SAT.


---

### Answer by username_6 on 2010-09-08. Score: 42

There are two kinds of "best" SAT solvers, one for theory, one for practice.

### Theory

* Kazuo Iwama, Kazuhisa Seto, Tadashi Takai, Suguru Tamaki, "[Improved Randomized Algorithms for 3-SAT](http://dx.doi.org/10.1007/978-3-642-17517-6_9)", ISAAC 2010.

> randomized $O(1.32113^n)$ for 3SAT.

* Timon Hertli, Robin A. Moser, Dominik Scheder, "[Improving PPSZ for 3-SAT using Critical Variables](http://arxiv.org/abs/1009.4830)", 2011.

> randomized $O(1.321^n)$ for 3SAT.

* Konstantin Kutzkov, Dominik Scheder, "[Using CSP To Improve Deterministic 3-SAT](http://arxiv.org/abs/1007.1166)", 2010.

> deterministic $O(1.439^n)$ for 3SAT.

### Practice

Check [SAT conference](http://www.satcompetition.org/) for competition results for each year.

> **Comments:**
> **username_0**: I found a link to [Iwama et al. paper](http://www.lab2.kuis.kyoto-u.ac.jp/~tamak/isaac2010.pdf). So, is $O(1.32113^n)$ really the latest and best result for solving SAT up until now?  
> **username_6**: @ Sadeq: I think so, but just for 3-SAT, not SAT.  
> **username_6**: Now the best algorithm is in $O(1.321^n)$ time by Timon Hertli, Robin A. Moser and Dominik Scheder.  
> **username_7**: Yet another update: in FOCS 2011, Timon Hertli (http://arxiv.org/abs/1103.2165) proved that the PPSZ algorithm solves every 3SAT instance in $1.308^n$ time.  

---

### Answer by username_8 on 2010-09-07. Score: 18

Schoening's algorithm is a probabilistic algorithm for k-SAT with running time $O(a^n)$, where $a = 2(k-1)/k$. This results in an $O(1.33334^n)$ algorithm for 3SAT, an $O(1.5^n)$ algorithm for 4SAT, etc.

The algorithm has also been (almost completely) derandomized by Moser and Scheder, who give a deterministic algorithm for solving kSAT running time $O((a+\epsilon)^n)$ where $a$ is the same constant as before, and $\epsilon>0$ can be made arbitrarily small.

Note: In this answer the big Oh notation hides poly(n) factors. I wanted to use the $O^\*$ notation, but it isn't rendering properly.

> **Comments:**
> **username_4**: Why do you say "almost completely"?  Did I miss something in the paper?  
> **username_9**: There is a deterministic $O((2 - \frac{2}{k + 1})^n)$ algorithm for k-SAT by eight people, so please forgive me not mentioning all of them. Here is the link: http://linkinghub.elsevier.com/retrieve/pii/S0304397501001748. So for $k = 3$ we have $O(1.5^n)$ and it is not as good as other bounds for 3-SAT presented here, but for k-SAT it is the best, as far as I know.  
> **username_8**: I said "almost completely" just to indicate that there's an epsilon factor there. I guess one would expect that a complete derandomization achieves the same run time (upto polynomial factors). Or maybe that's unreasonable to expect.  
> **username_8**: @Grigory Yaroslavtsev: Isn't the Moser-Scheder deterministic algorithm for kSAT that I mentioned faster that the one you quoted? Am I missing something?  
> **username_9**: I was just worried about this $\epsilon$ in your notation, so it is faster indeed. It looks like the paper appeared on arXiv just a few days ago: http://arxiv.org/PS_cache/arxiv/pdf/1008/1008.4067v1.pdf, so no wonder I didn't know about it.  

---

### Answer by username_10 on 2010-09-27. Score: 13

As was already mentioned, if you are interested in theoretical running time guarantees, this question is a duplicate.

But I'd like to point out that if you really want to solve a concrete problem (like the colouring problem that you mentioned), I think that it makes absolutely no sense at all to study theoretical upper bounds.

Even though you wanted to avoid "engineering" aspects, I'd suggest that you just take some popular SAT solvers, try them out, and see what happens (most of them can read the same DIMACS file format, so it is easy to try different solvers). You may have both positive and negative surprises. Recently I had a family of SAT instances; a bunch of instances with tens of thousands of variables and more than one million clauses turned out to be easy to solve, while seemingly much simpler instances with just hundreds of variables and thousands of clauses were far too difficult for any solver that I tried.

> **Comments:**
> **username_4**: In addition to Jukka's summary, it is also worth noting that there are two main kinds of SAT solvers: those based on survey propagation, which work well for random SAT instances, and those which use clause learning combined with unit resolution, which tend to work well to discover combinatorial structure.  These have quite different behaviour.  The worst cases for SAT solvers tend to be instances that are not satisfiable, but where the space of nogoods has complex structure that does not allow much pruning.  Unfortunately instances from combinatorics tend to be of this kind.  

---

### Answer by username_1 on 2014-02-07. Score: 12

* Timon Hertli, "[3-SAT Faster and Simpler - Unique-SAT Bounds for PPSZ Hold in General](http://arxiv.org/abs/1103.2165)", FOCS 2011.

> deterministic $O(1.308^n)$ for 3SAT.

> **Comments:**
> **username_11**: I assume that when somebody comes up with a better upper bound they would cite this paper. There has been only once citation to this paper, which is "A Satisfiability Algorithm and Average-Case Hardness for Formulas over the Full Binary Basis" And they seem to talk about only certain types of formulas. Therefore, this seems to be the best Upper Bound thus far.  
> **username_11**: @RickyDemer Uhuh! is it a better bound than this? Notation is not so clear to me.  

---

### Answer by username_12 on 2010-09-07. Score: 9

It is impossible for 3SAT to have sub-exponential algorithms unless the [exponential time hypothesis](http://en.wikipedia.org/wiki/Exponential_time_hypothesis) is false.

* Kazuo Iwama, Suguru Tamaki, [Improved upper bounds for 3-SAT](http://portal.acm.org/citation.cfm?id=982838), 2004.

> randomized algorithm with expected running time $O({1.324}^n)$ for 3SAT.

* Daniel Rolf, [Improved Bound for the PPSZ/Schoning-Algorithm for 3-SAT](http://eccc.hpi-web.de/report/2005/159/), 2005.

> randomized algorithm with expected running time $O({1.32216}^n)$ for 3SAT.

> **Comments:**
> **username_13**: Isn’t that a tautology?  
> **username_0**: Yes, that is a tautology: The exponential time hypothesis (ETH) is that 3SAT, the satisfiability problem of Boolean formulas in conjunctive normal form with at most three literals per clause and with n variables, cannot be solved in time $2^{o(n)}$. (See: [wikipedia](http://en.wikipedia.org/wiki/Time_complexity#Exponential_time_hypothesis)).  
> **username_0**: The work of Kazuo Iwama et al. (2004) is newer than that of Schoening's (1999). I wonder if even more recent results are available.  
> **username_13**: To avoid possibility of confusion, my last comment refers to the first sentence of the answer: “It is impossible for 3SAT to have sub-exponential algorithms unless the exponential time hypothesis (ETH) is false.”  My understanding is that the exponential-time hypothesis is the very hypothesis stating that there is no algorithm for 3SAT whose running time is subexponential (i.e. 2^{o(n)}) in the number of variables.  
> **username_8**: And to avoid further confusion, I will add that when Tsuyoshi posted his comment, the answer only contained that one sentence, which made his comment very appropriate.  

---

### Answer by username_14 on 2010-09-27. Score: 8

This [post](https://cstheory.stackexchange.com/questions/1060/best-upper-bounds-on-sat) deals with upper bounds on SAT. This [one](https://cstheory.stackexchange.com/questions/93/what-are-the-best-current-lower-bounds-on-3sat) deals with best lower bounds. This [link](http://www.satcompetition.org/) gives details of the annual competition comparing SAT solver implementations, which are all downloadable. For simplicity, you could start with [SAT4J](http://www.sat4j.org/), a Java based library for SAT solving.

> **Comments:**
> **username_5**: Turns out this question *was* already asked before; I just didn't see it when I searched the website. Tian Liu's response on the upper bounds question is exactly what I was looking for. Thanks for the links, dave!  
> **username_14**: This is evidence that I spend too much time here ;-)  
> **username_3**: we're glad that you do :)  
> **username_15**: I'm not sure if I would recommend sat4J, not only it is significantly slower than the state-of-the-art but also somewhat more complex. It is true, however, that it is nicely customizable due to the object-oriented structure. MiniSat is very nicely written and 2.2 is state-of-the-art.  

---

### Answer by username_16 on 2018-09-21. Score: 4

The best deterministic algorithm for 3-SAT now has upper bound 1.32793^n, see <https://arxiv.org/abs/1804.07901> by Sixue Liu. Basically the upper bounds for all k-SAT have been improved in this paper.


---

