Haskell: binding to fast and simple SAT solver

Question

Today I wanted too look into options on SAT solving in haskell. First I tought about writing my own interface to the picosat solver.

Then I found out there is the SBV library. It's interfaces to Z3, Yices, CVC4 and Boolector.

Also, I did a google search on github and it turs out there is even Picosat binding availiable.

Are there any other haskell bindings to SAT solvers that are worth looking at given the constraint of fast/high performance. Carification: that are as suitable for high performance SAT-solving (e.g., problems that run for days, as well as problems that need to finish as fast as possible as I check 2^20 or more SAT problems). For example, what I am particularly missing on hackage is a binding to a fast parrallel SAT solver like Plingeling. (Also, I found out about the current updated picosat binding on github more by accident and I very well might miss other options)

The default option of the SBV library is the Z3 SMT solver. Am I right in my educated guess that picosat is faster for plain SAT-solving than Z3?

Answer 1

Disclosure, I'm the author of the Haskell picosat bindings you mentioned.

SBV is really robust library that's been around for a while, it's good if you want an interface to external SMT or SAT solvers like Yices or Z3. Picosat is a much simpler library that I wrote simply because I wanted a library that could be installed simply without external dependencies.

Am I right in my educated guess that picosat is faster for plain SAT-solving than Z3?

I don't know what your performance constraints are, but as far as underlying solver libraries go you're not going to notice a significant difference between Z3 or Picosat until you hit really enormous problems ( billions of variables ). Both are very heavily optimized libraries and the bottleneck ( at least from the Haskell side ) is likely going to be marshalling data between the library and Haskell's runtime.

Answer 2

SBV is thread-safe.

Comparing Z3 and Lingeling for SAT performance is not an easy task. I'd hazard a guess that they would be more or less the same unless you take your time to figure out the exact parameters to fine tune their internal heuristics.

The good thing is that SBV provides a common interface, so you can change the solver by merely importing a different bridge:

import Data.SBV.Bridge.Z3

vs

import Data.SBV.Bridge.Boolector

and if you compile boolector to use lingeling, then you can test performance easily by merely changing one line of Haskell.