Haskell: binding to fast and simple SAT solver

5
votes

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?

2
haskellz3smtsatisfiabilitypicosat
Not trying to be snarky, but do you know to look at hackage? There are lots of SAT and SMT packages there already, just searching for "sat" yields 10 packages (some are bindings, some are plumbing and some are Haskell SAT implementations). Searching for "smt" yields a few others, and you can likely find one or two more by crawling around (ex: "picosat" is on hackage). – Thomas M. DuBuisson
I looked at hackage by category and searched in the browser, but apparently there is a text search feature. The other options on hackage are either binds that the SBV library already offers or not compare to picosat regarding speed. – mrsteve
Thomas, do you happpen to know if all hackage package libraries are suitable for trival multi-threaded programming? trivial in the sense that I don't my SAT problems are all stricly seperated and there is no need for shared memory or so, I just want to make n SAT calls of different problems at once. – mrsteve
I would guess that the libraries you are interested in are all thread safe. That said, this is not universally true for all Hackage packages. There is no quality assurance for uploads to hackage - all you need to do is request an account. As a result there is lots of stuff on hackage that might be deceptively not thread save (my latest example is secure-sockets, due to thread local storage used by OpenSSL). – Thomas M. DuBuisson
you say you're dealing with 2^20 problems - are they related in some way? perhaps it's just one QBF-SAT problem? fmv.jku.at/qbf2013 – d8d0d65b3f7cf42

2 Answers

6
votes

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.

5
votes

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.