[porcoda]

Interesting post, but I’m not sure this really speaks to what goes into actually writing what would be considered a “fast” SAT solver. It seems more like a post about how SAT pops up in a lot of places if you look at them right. For the state of the art in what constitutes fast solvers, the annual SAT competition papers are quite interesting to read if you’re interested in the techniques people come up with to make them fast. A few years ago I was working through Knuth’s satisfiability book and writing my own solvers, and was always amazed how stunningly fast the SAT competition winners were compared to the ones I’d code up.

[dang]

Ok, we've taken the fast bit out of the title above. It's still a good post!

[ComplexSystems]

SAT turns up everywhere because it's almost universal kind of problem. Since it is NP complete, everything in NP can be transformed into an instance of SAT. Since P is a subset of NP, everything in P can be also be turned into an instance of SAT. Nobody knows if things in PSPACE can be, though.

[butokai]

Add to this that propositional logic (the language in which we express SAT) is a versatile language to code problems in. Finding cliques in a graph is also NP complete, but it is less natural to use it as a language to code other problems.

[riku_iki]

> Add to this that propositional logic (the language in which we express SAT) is a versatile language to code problems in

is it though? You can't express some basic loop in propositional logic, right?

[viraptor]

Loops are part of a coded solution, not the problem. With SAT you encode the problem / solution space itself.

[CaptainNegative]

> Since P is a subset of NP, everything in P can be also be turned into an instance of SAT.

This statement is kind of trivial. The same is true for any language (other than the empty language and the language containing all strings). The reduction is (1) hardcode the values of one string, y, that is in the language and another string, z, that is not in the language (2) solve the problem on the given input x in polynomial time poly(x) (3) return y if x is to be accepted and z otherwise.

The total running time is at most poly(x)+O(|y|+|z|) which is still poly(x) since |y| and |z| are hardcoded constant values.

[layer8]

One would assume there are some low-hanging fruits that make up the bulk of the speed-ups, but maybe it’s really a huge pile of small incremental improvements?

[ted_dunning]

My impression is that going from a very simple case like this to a moderately fast solver involves bringing in a fair number of intuitive improvements like memoization of anti-patterns and heuristic reordering of the search.

But getting a really fast solver requires multiple strategies that don't work well together (so they have to work semi-independently). This leads to other problems related to managing shared resources like how much you should let different strategies cache information at the expense of how much other strategies can cache information. Tuning all of these trade-offs is exceedingly difficult to do well since it depends a lot on the types of problems that you need to solve.