43
$\begingroup$

In another thread, 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?

$\endgroup$
  • 2
    $\begingroup$ I don't know about analytic results, but you can find experimental results here baldur.iti.uka.de/sat-race-2010/results.html (see the "HTML" links) $\endgroup$ – Radu GRIGore Sep 7 '10 at 19:10
  • 1
    $\begingroup$ this question title is a bit misleading, because of the existence of this question: cstheory.stackexchange.com/questions/1295/sat-solver-download . I think you might rephrase as 'Best Upper Bounds on SAT' ? $\endgroup$ – Suresh Venkat Sep 25 '10 at 13:30
  • $\begingroup$ @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? $\endgroup$ – M.S. Dousti Sep 25 '10 at 16:44
  • $\begingroup$ 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 :). $\endgroup$ – Suresh Venkat Sep 25 '10 at 18:00
  • 4
    $\begingroup$ 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. $\endgroup$ – András Salamon Sep 27 '10 at 17:19
38
$\begingroup$

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

Theory

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

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

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

Practice

Check SAT conference for competition results for each year.

$\endgroup$
  • $\begingroup$ I found a link to Iwama et al. paper. So, is $O(1.32113^n)$ really the latest and best result for solving SAT up until now? $\endgroup$ – M.S. Dousti Sep 9 '10 at 15:51
  • $\begingroup$ @ Sadeq: I think so, but just for 3-SAT, not SAT. $\endgroup$ – Tian Liu Sep 10 '10 at 0:20
  • 2
    $\begingroup$ Now the best algorithm is in $O(1.321^n)$ time by Timon Hertli, Robin A. Moser and Dominik Scheder. $\endgroup$ – Tian Liu Sep 28 '10 at 5:42
  • 10
    $\begingroup$ Yet another update: in FOCS 2011, Timon Hertli (arxiv.org/abs/1103.2165) proved that the PPSZ algorithm solves every 3SAT instance in $1.308^n$ time. $\endgroup$ – Ryan Williams Jan 7 '12 at 18:59
21
+50
$\begingroup$

I am not aware of any zero-error randomized algorithms (or coNE/Eadvice algorithms,
for that matter) for SAT that have better bounds than known deterministic algorithms,
regardless of whether or not there is promised to be at most one satisfying assignment.


"Problem 3-SAT is deterministically solvable in time $\overset{\sim}{O}(1.3303^n)$."


"For a uniquely satisfiable 3-CNF (resp. 4-CNF) on $n$ variables, the satisfying assignment
can be found in deterministic running time at most $O\hspace{.02 in}(1.3071^n)$ (resp. $O\hspace{.02 in}(1.4699^n)$)."


  1. "There exists a randomized algorithm for 3-SAT with
    one-sided error that runs in time $O\hspace{.02 in}(1.30704^n)$."
  2. "There exists a randomized algorithm for 4-SAT with
    one-sided error that runs in time $O\hspace{.02 in}(1.46899^n)$."


"There is a randomized algorithm for unique-3-SAT such that for $\: \epsilon = 1\hspace{-0.03 in}\big/\hspace{-0.06 in}\left(\hspace{-0.03 in}10^{\hspace{.02 in}24}\hspace{-0.04 in}\right) \:$ and
$S$ the real number that lets the previous paper's runtime bound for 3-SAT be expressed
as $\: O\hspace{-0.04 in}\left(2^{(S+o(1))\cdot n}\right) \:$, $\;$ the current paper's algorithm runs in time $\: O\hspace{-0.04 in}\left(2^{(S-\epsilon+o(1))\cdot n}\right)$ ."


$\endgroup$
16
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ Why do you say "almost completely"? Did I miss something in the paper? $\endgroup$ – András Salamon Sep 7 '10 at 23:45
  • 1
    $\begingroup$ 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: 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. $\endgroup$ – Grigory Yaroslavtsev Sep 8 '10 at 0:06
  • 4
    $\begingroup$ 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. $\endgroup$ – Robin Kothari Sep 8 '10 at 1:26
  • 1
    $\begingroup$ @Grigory Yaroslavtsev: Isn't the Moser-Scheder deterministic algorithm for kSAT that I mentioned faster that the one you quoted? Am I missing something? $\endgroup$ – Robin Kothari Sep 8 '10 at 1:28
  • 1
    $\begingroup$ 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: arxiv.org/PS_cache/arxiv/pdf/1008/1008.4067v1.pdf, so no wonder I didn't know about it. $\endgroup$ – Grigory Yaroslavtsev Sep 8 '10 at 3:15
12
$\begingroup$

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.

$\endgroup$
  • 8
    $\begingroup$ 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. $\endgroup$ – András Salamon Sep 27 '10 at 17:10
11
$\begingroup$

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

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Tayfun Pay Feb 9 '14 at 1:52
  • $\begingroup$ @TayfunPay : $\:$ The bottom paper in my answer cites that paper. $\;\;\;\;$ $\endgroup$ – user6973 Feb 9 '14 at 8:03
  • $\begingroup$ @RickyDemer Uhuh! is it a better bound than this? Notation is not so clear to me. $\endgroup$ – Tayfun Pay Feb 10 '14 at 2:09
  • $\begingroup$ @TayfunPay : $\:$ Yes, and you can hunt through the two papers as described in the following. $\:$ On page 5 of the general 3-SAT paper, they give the value of $S_3$, report the PPSZ algorithm's runtime for unique k-SAT in terms of $S_k$, and say that they have the same bound for general k-SAT. $\:$ At the top of page 11, that paper says their algorithm gives the same bound as PPSZ, which means they did not show anything more than I mentioned in my previous sentence. $\:$ (continued ...) $\hspace{.35 in}$ $\endgroup$ – user6973 Feb 10 '14 at 5:33
  • $\begingroup$ (... continued) $\:$ On page 2 of the unique 3-SAT paper, they give the value of $S$ and say that their algorithm gives a bound that is better than $2^{S\cdot n}$ by an explicit exponential amount. $\:$ Since $S$ from my previous sentence is equal to $S_3$ from the sentence before that, the unique 3-SAT paper's bound is exponentially better than the general 3-SAT paper's bound. $\;\;\;$ $\endgroup$ – user6973 Feb 10 '14 at 5:34
8
$\begingroup$

It is impossible for 3SAT to have sub-exponential algorithms unless the exponential time hypothesis is false.

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

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

$\endgroup$
  • 15
    $\begingroup$ Isn’t that a tautology? $\endgroup$ – Tsuyoshi Ito Sep 7 '10 at 19:19
  • 1
    $\begingroup$ 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). $\endgroup$ – M.S. Dousti Sep 7 '10 at 19:59
  • $\begingroup$ 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. $\endgroup$ – M.S. Dousti Sep 7 '10 at 20:14
  • 8
    $\begingroup$ 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. $\endgroup$ – Tsuyoshi Ito Sep 7 '10 at 21:51
  • 10
    $\begingroup$ 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. $\endgroup$ – Robin Kothari Sep 8 '10 at 1:29
7
$\begingroup$

This post deals with upper bounds on SAT. This one deals with best lower bounds. This link gives details of the annual competition comparing SAT solver implementations, which are all downloadable. For simplicity, you could start with SAT4J, a Java based library for SAT solving.

$\endgroup$
  • $\begingroup$ 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! $\endgroup$ – Daniel Apon Sep 27 '10 at 14:55
  • 1
    $\begingroup$ This is evidence that I spend too much time here ;-) $\endgroup$ – Dave Clarke Sep 27 '10 at 14:59
  • $\begingroup$ we're glad that you do :) $\endgroup$ – Suresh Venkat Sep 28 '10 at 2:52
  • 2
    $\begingroup$ 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. $\endgroup$ – Mikolas Apr 7 '11 at 7:55
3
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.