Hacker News Reader

Comment by keenerd | Hacker News Reader

I have not been too impressed with fancier SAT solvers. I'm currently drafting a blog post where I compare Minisat, Picosat, Cryptominisat, Lingeling and Glucose. (Those were all that I could easily get running on Linux. Open to more suggestions.)

The venerable Minisat was (for the most part) the fastest in my simple use case. What I did notice though was that the "smarter" solvers were more consistent. A poorly written CNF might take 50x longer than it should (when compared to N-1 and N+1 instances). Minisat (but moreso Picosat) would occasionally hit an edge case or something and slow way down. Fancier solvers produced a nice clean line on the graphs, without anomalous 50x spikes.

View on HN

For smaller problems, the fancier solvers are actually worse than MiniSat/Picosat. That's because of the overhead of creating and maintaining datastructures and the fancy preprocessing. The larger, more complex solvers are meant to have a better chance to solve more complex problems and will use hybrid strategies to make sure they don't accidentally go down into some rabbit hole. So I would expect them to have better consistency.

Note that winning in the competition, until 2017, meant you solved the most instances, each with a ~5000s timeout. So if you solved every single one within 4999s you won, you were the best... This obviously encouraged incredibly long startup times that are gained back over the overall 5000s timeout. It clearly does not mimic normal use-cases.

Thanks. That makes sense. Most of my stuff has (at most) a few million clauses and usually takes between 1-600 seconds.

One thing to try, especially with Glucose: turn off the preprocessing. The preprocessing seems to help with really "hard" instances like you see in SAT competitions, but takes time and doesn't really help with simpler ones.

We use SAT solvers extensively in the Phil[0] crossword construction tool, to figure out when the grid is overconstrained, and which letters have only a single value in all possible solutions. We ended up running Glucose (compiled to wasm and running in the browser) because the simpler solvers couldn't solve many instances quickly, and with preprocessing off but most other parameters at their defaults. I didn't do a careful evaluation of all solvers, but it might be interesting.

I really need to write this stuff up.

[0]: https://github.com/keiranking/Phil

Reply on news.ycombinator.com