Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
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?
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.
