<p>There is an enormous difference between sat <em>instances</em>.  SAT solver $A$ might perform well on the class $X$ of instances, but poorly on the class $Y$ of instances, while solver $B$ performs well on class $Y$ and poorly on class $X$.</p>

<p>A good paper to read on this topic is <a href="http://robotics.stanford.edu/~shoham/www%20papers/CP04randomsat.pdf" rel="noreferrer">this one</a> by Nudelman <em>et al</em>.  The whole point of the paper is to determine easy-to-compute features of SAT instances that can tell you which algorithms are likely to perform well and which aren't.  Using this technique it's possible to build a portfolio-based algorithm that will quickly analyze a problem instance, then solve the instance with the most appropriate algorithm.  There's a progression of papers that follows that one; googling SATzilla will turn up lots of reading material.</p>

<p>If you're wondering why SAT solver $A$ might be better than solver $B$ on <em>all</em> instances, well, I guess that's progress :).  If you want to know what specifically makes a solver good, the answer could probably be turned into several doctoral theses.  I suggest you start with <a href="http://robotics.stanford.edu/~shoham/www%20papers/CP04randomsat.pdf" rel="noreferrer">that paper of Nudelman <em>et al</em></a>.</p>

CC BY-SA 3.0
2011-07-21T22:18:35.140Z
2017-03-07T18:36:55.783Z
2017-03-07T18:36:55.783Z
James King
<p>Yes, there is a major difference between MiniSAT and WalkSAT. First, let's clarify - MiniSAT is a specific implementation of the generic class of <a href="http://en.wikipedia.org/wiki/DPLL_algorithm">DPLL</a>/CDCL algorithms which use backtracking and clause learning, whereas WalkSAT is the general name for an algorithm which alternates between greedy steps and random steps.</p>

<p>In general DPLL/CDCL is much faster on <em>structured</em> SAT instances while WalkSAT is faster on <em>random</em> k-SAT. Industrial and applied SAT instances tend to have a lot of structure, so DPLL/CDCL is dominant in most modern SAT solvers. Instance to instance one technique may win out, though, which is one reason why portfolio solvers have become popular.</p>

<p>I take a lot of issue with your claim that WalkSAT is much faster than MiniSAT on the instances on that page. For one thing, there are gigabytes of SAT instances there - how many did you try comparing them on? WalkSAT is not at all competitive on most structured instances which is why it's not often seen in competitions.</p>

<p>On a side note - Vijay is right that MiniSAT is still relevant. Actually, because it's open source and well-written, MiniSAT is <em>the</em> solver to beat in order to show that a given optimization has promise. Many people tweak MiniSAT itself to showcase their optimizations - take a look at the "MiniSAT hack" category in the recent SAT competitions.</p>

CC BY-SA 3.0
2011-07-22T00:17:00.137Z
2011-07-22T14:13:15.743Z
2011-07-22T14:13:15.743Z
Huck Bennett
<p>SAT solvers are very important in <a href="http://en.citizendium.org/wiki/Algebraic_attack">algebraic attacks</a>, for example <a href="http://en.wikipedia.org/wiki/WalkSAT">walksat</a> and <a href="http://minisat.se/">minisat</a>.</p>

<p>However, when solving the benchmark problems available <a href="http://www.satcompetition.org/">here</a> there is an enormous performance difference between the two - Walksat is much faster than minisat for these problems. Why is this?</p>

<p><a href="http://www.cs.rochester.edu/~kautz/walksat/">This</a> implementation of walksat appears to have some performance improvements - is there any reason it wasn't included in <a href="http://www.satcompetition.org/">the international SAT Competitions</a>?</p>

CC BY-SA 3.0
2011-07-21T20:57:46.190Z
Your second question, about why a certain algorithm was excluded from a certain competition, is probably out-of-scope for this site.  Your first question, about what makes one algorithm often faster than another, I think is fair game, but might need some rephrasing to make it more theory-friendly.
Lev Reyzin
CC BY-SA 3.0
2011-07-21T21:20:12.920Z
Short note: Minisat is quite old, does not seem maintained, and did not participate in the competition either. Also, what do you mean by "enormous" and which track are you referring to (random/crafted/application)?
Radu GRIGore
CC BY-SA 3.0
2011-07-21T22:40:59.073Z
@Radu: MiniSAT 2.2.0 was released in July 2010. I wouldn't say it isn't maintained. Also, the code is quite stable and clean, so the infrequent updates may not be an issue. I agree though that newer solvers better reflect the state of the art.
Vijay D
CC BY-SA 3.0
2011-07-22T16:20:01.563Z
Question cross-posted from Crypto.SE http://crypto.stackexchange.com/questions/153/why-is-there-an-enormous-difference-between-sat-solvers .
Mohammad Alaggan
<ds.algorithms><sat><big-picture>
Why is there an enormous difference between SAT solvers?
ir01
# Why is there an enormous difference between SAT solvers?

(Asked by: username_0 on 2011-07-21)

SAT solvers are very important in [algebraic attacks](http://en.citizendium.org/wiki/Algebraic_attack), for example [walksat](http://en.wikipedia.org/wiki/WalkSAT) and [minisat](http://minisat.se/).

However, when solving the benchmark problems available [here](http://www.satcompetition.org/) there is an enormous performance difference between the two - Walksat is much faster than minisat for these problems. Why is this?

[This](http://www.cs.rochester.edu/~kautz/walksat/) implementation of walksat appears to have some performance improvements - is there any reason it wasn't included in [the international SAT Competitions](http://www.satcompetition.org/)?

**Tags:** ds.algorithms, sat, big-picture

> **Comments:**
> **username_1**: Your second question, about why a certain algorithm was excluded from a certain competition, is probably out-of-scope for this site.  Your first question, about what makes one algorithm often faster than another, I think is fair game, but might need some rephrasing to make it more theory-friendly.  
> **username_2**: Short note: Minisat is quite old, does not seem maintained, and did not participate in the competition either. Also, what do you mean by "enormous" and which track are you referring to (random/crafted/application)?  
> **username_3**: @Radu: MiniSAT 2.2.0 was released in July 2010. I wouldn't say it isn't maintained. Also, the code is quite stable and clean, so the infrequent updates may not be an issue. I agree though that newer solvers better reflect the state of the art.  
> **username_4**: Question cross-posted from Crypto.SE http://crypto.stackexchange.com/questions/153/why-is-there-an-enormous-difference-between-sat-solvers .  

---

## 2 answers

### Answer by username_6 on 2011-07-22. Score: 39 | Accepted answer

Yes, there is a major difference between MiniSAT and WalkSAT. First, let's clarify - MiniSAT is a specific implementation of the generic class of [DPLL](http://en.wikipedia.org/wiki/DPLL_algorithm)/CDCL algorithms which use backtracking and clause learning, whereas WalkSAT is the general name for an algorithm which alternates between greedy steps and random steps.

In general DPLL/CDCL is much faster on *structured* SAT instances while WalkSAT is faster on *random* k-SAT. Industrial and applied SAT instances tend to have a lot of structure, so DPLL/CDCL is dominant in most modern SAT solvers. Instance to instance one technique may win out, though, which is one reason why portfolio solvers have become popular.

I take a lot of issue with your claim that WalkSAT is much faster than MiniSAT on the instances on that page. For one thing, there are gigabytes of SAT instances there - how many did you try comparing them on? WalkSAT is not at all competitive on most structured instances which is why it's not often seen in competitions.

On a side note - Vijay is right that MiniSAT is still relevant. Actually, because it's open source and well-written, MiniSAT is *the* solver to beat in order to show that a given optimization has promise. Many people tweak MiniSAT itself to showcase their optimizations - take a look at the "MiniSAT hack" category in the recent SAT competitions.


---

### Answer by username_5 on 2011-07-21. Score: 23

There is an enormous difference between sat *instances*. SAT solver $A$ might perform well on the class $X$ of instances, but poorly on the class $Y$ of instances, while solver $B$ performs well on class $Y$ and poorly on class $X$.

A good paper to read on this topic is [this one](http://robotics.stanford.edu/~shoham/www%20papers/CP04randomsat.pdf) by Nudelman *et al*. The whole point of the paper is to determine easy-to-compute features of SAT instances that can tell you which algorithms are likely to perform well and which aren't. Using this technique it's possible to build a portfolio-based algorithm that will quickly analyze a problem instance, then solve the instance with the most appropriate algorithm. There's a progression of papers that follows that one; googling SATzilla will turn up lots of reading material.

If you're wondering why SAT solver $A$ might be better than solver $B$ on *all* instances, well, I guess that's progress :). If you want to know what specifically makes a solver good, the answer could probably be turned into several doctoral theses. I suggest you start with [that paper of Nudelman *et al*](http://robotics.stanford.edu/~shoham/www%20papers/CP04randomsat.pdf).


---

