# Why is there an enormous difference between SAT solvers?

SAT solvers are very important in algebraic attacks, for example walksat and minisat.

However, when solving the benchmark problems available here there is an enormous performance difference between the two - Walksat is much faster than minisat for these problems. Why is this?

This implementation of walksat appears to have some performance improvements - is there any reason it wasn't included in the international SAT Competitions?

• 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 Jul 21 '11 at 20:57
• 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 Jul 21 '11 at 21:20
• @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 Jul 21 '11 at 22:40
• Question cross-posted from Crypto.SE crypto.stackexchange.com/questions/153/… . – Mohammad Alaggan Jul 22 '11 at 16:20

## 2 Answers

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/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.

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 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.