Take the 2-minute tour ×
Cryptography Stack Exchange is a question and answer site for software developers, mathematicians and others interested in cryptography. It's 100% free, no registration required.

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?

share|improve this question
4  
This would be better suited on CSTheory SE. I think it is on topic for Crypto, but you will certainly get a better response there. –  PulpSpy Jul 18 '11 at 16:28
add comment

2 Answers

up vote 5 down vote accepted

Walksat is an incomplete solver. This means that it tries to find a solution for a number of iterations. If it does find a solution it answers with the solution, otherwise it answers "don't know". Walksat uses a form of random walk to search for solutions with heuristics to guide its step.

Minisat on the other hand, given enough computational resources, gives you either a solution or answer that the problem is unsatisfiable (and by adding a proof-trace you also get a proof). Minsat uses a modern form of DPLL.

The short answer to your question is that it is easier to search for an answer, if it exists, than proving than no answer exists.

The longer answer is that walksat is only faster than minisat if there is a lot of solutions and their structure is of a special kind in the search space.

On the page with benchmarks I could not find any reference to walksat. Have you testet walksat on some benchmarks yourself? Have you tested walksat on benchmarks that are known to be unsatisfiable?

share|improve this answer
    
In answer to "Have you testet walksat on some benchmarks yourself?" Yes. and in answer to "Have you tested walksat on benchmarks that are known to be unsatisfiable?" no. –  ir01 Aug 3 '11 at 10:39
add comment

SAT solvers don't have a single approach -- not every approach works equally well for every problem. A SAT solver that performs well on a given problem will not necessarily work well in general.

Typically SAT solvers employ a whole bag of tricks -- deciding what heuristic to employ is one of the big differences between solvers. Different heuristics work well for different types of problems and a solver must identify traits of the problem at hand to decide which heuristic to use (unless the user specifies which heuristic to use, which one might, if one knows what to do, or for experimentation purposes).

As to why a given solver wasn't entered in the international SAT competition, you'd have to ask the creator of the solver! I'm pretty sure they could submit it if they wanted to...

share|improve this answer
add comment

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.