Tell me more ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.
up vote 23 down vote favorite
9

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?

share|improve this question
2  
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) – Radu GRIGore Sep 7 '10 at 19:10
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' ? – Suresh Venkat♦ Sep 25 '10 at 13:30
@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 Sep 25 '10 at 16:44
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♦ Sep 25 '10 at 18:00
3  
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 Sep 27 '10 at 17:19
show 3 more comments

5 Answers

up vote 20 down vote accepted

There are two kinds of "best" SAT solvers, one for theory, one for practice. For theory one, first please check the accepted papers in ISAAC 2010 by Iwama et al, this paper gives a new randomized algorithm which solves 3-SAT in time $O(1.32113^n)$. Recently, Hertli, Moser and Scheder have an $O(1.321^n)$ algorithm. Second, Kutzkov and Schederfor have a deterministic algorithm for 3-SAT in time $O(1.439^n)$. For practice one, please check SAT conference homepages for competetion results in each year or here and above link in first comment/answer. (maybe I should ignore the practice one, since this is a "theory" web.)

share|improve this answer
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? – Sadeq Dousti Sep 9 '10 at 15:51
@ Sadeq: I think so, but just for 3-SAT, not SAT. – Tian Liu Sep 10 '10 at 0:20
1  
Now the best algorithm is in $O(1.321^n)$ time by Timon Hertli, Robin A. Moser and Dominik Scheder. – Tian Liu Sep 28 '10 at 5:42
2  
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. – Ryan Williams Jan 7 '12 at 18:59
up vote 8 down vote

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.

share|improve this answer
Why do you say "almost completely"? Did I miss something in the paper? – András Salamon Sep 7 '10 at 23:45
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. – Grigory Yaroslavtsev Sep 8 '10 at 0:06
2  
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 Sep 8 '10 at 1:26
@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 Sep 8 '10 at 1:28
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. – Grigory Yaroslavtsev Sep 8 '10 at 3:15
up vote 6 down vote

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.

share|improve this answer
7  
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 Sep 27 '10 at 17:10
up vote 4 down vote

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

For the Upper bound, 3-SAT has randomized algorithm with expected running time $O({1.324}^n)$

Improved upper bounds for 3-SAT, Kazuo Iwama, Suguru Tamaki, foo

Actually, Daniel Rolf improved Kazuo Iwama, Suguru Tamaki result to $O({1.32216}^n)$

Improved Bound for the PPSZ/Schoning-Algorithm for 3-SAT, Daniel Rolf,

share|improve this answer
13  
Isn’t that a tautology? – Tsuyoshi Ito Sep 7 '10 at 19:19
1  
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). – Sadeq Dousti Sep 7 '10 at 19:59
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 Sep 7 '10 at 20:14
6  
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 Sep 7 '10 at 21:51
4  
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 Sep 8 '10 at 1:29
up vote 4 down vote

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.

share|improve this answer
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 Sep 27 '10 at 14:55
1  
This is evidence that I spend too much time here ;-) – Dave Clarke♦ Sep 27 '10 at 14:59
we're glad that you do :) – Suresh Venkat♦ Sep 28 '10 at 2:52
1  
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 Apr 7 '11 at 7:55

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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