Announcing gophersat, a SAT and Pseudo-Boolean solver, v1.0.0

[Fabien]

Dear fellow gophers,

I'm happy to announce that gophersat, the SAT and pseudo-boolean solver written in Go by the Centre de Recherche en Informatique de Lens, now reached its first stable release (v1.0.0). It is available at https://github.com/crillab/gophersat and is released under the MIT license.

We chose to apply the "standard" go policy regarding versioning, meaning the whole API will be backward-compatible for all coming 1.x versions, but might break at versions 2.x and above. Minor versions will be used for new, backward-compatible features, and patches for bug fixes or performance improvements.

Gophersat is a reasonably efficient SAT solver, meaning it can solve NP-complete problems described as propositional formulas, described either in the standard DIMACS format or using a more user-friendly but proprietary format. It also natively deals with pseudo-boolean (PB) problems, which allow for a more compact representation of most problems. It can be used for decision problems ("is there a solution to this problem ?") and optimization problems ("what is the best possible solution, if any?"). It can be used as a standalone executable or as a go library.

If you would like to contribute to gophersat, would like to use it but don't know where to start, would like to understand how it works, or would like a new feature to be added to it, please let me know.

Fabien

[Damian Gryski]

How does it compare to https://github.com/IRIFrance/gini ?

[Fabien]

Short answer : according to the few tests I ran, they are pretty close. You can use any of them, or, even better, both of them.

Long answer :

I have only compared them on about a dozen industrial problems, so take it with a grain of salt, but it's hard to name a winner. Gini is usually a little faster, but when it is slower, it is way slower than Gophersat. Gini is very good (sometimes even better than state-of-the-art C++ solvers, like glucose) on some very easy problems (those that can be solved in about 10 to 50 ms), probably because it has a very good parser and low warmup costs. But it is not as good on harder problems, and it can only deal with pure SAT, CNF problems (and they can be exponentially bigger than their pseudo-boolean counterparts).

So, if you must solve hundreds of easy problems in a second, and if your problem is described as a CNF and you have no control over that, picking gini might be a good choice. If your problem is a little harder, or if you have the possibility to describe it as a pseudo-boolean problem, gophersat will probably be better.

Since they are not efficient on the same kinds of problems, using both of them concurrently might be interesting, too. Making them solve the same problem and stop them when an answer was found.

When solving pure CNF problems, the current version of gophersat suffers from the fact that it can natively deal with cardinality constraints and pseudo-boolean constraints: binary clauses take a lot of space in memory, and a lot of time is spent in the solver figuring out whether we are dealing with a clause or a more complex constraint. In the next future, we will probably include the ability to compile an optimized version of the solver for pure sat problems via build tags. Having generics in the language would solve that issue too ;)

[Damian Gryski]

Wow, thanks for the detailed answers!

Damian

[Mandolyte]

Fabien, you mention below that generics would help... I encourage you to make a fuller description of why/how generics would help and update this wiki page to point to it:

https://github.com/golang/go/wiki/ExperienceReports#generics

[Fabien]

Thanks for the link, I'll write a description of my problem.

[Scott Cotton]

Hi,

Gini was benchmarked on a reasonably sized set of randomly selected sat competition problems against minisat and picosat.  It did very well, before there was even gophersat.  SAT competition problems are much harder than many application use case problems because they are of interest as a challenge to solver developers.

Gophersat, last I checked said it was much slower than standard C sat solvers such as these.  Gini outperformed picosat and minisat (by minisat, I mean the core cdcl solver, not with preprocessing, which is not a cop-out because pre-processing has it's own problems for applications).

Also, Gini still has the issue of array bounds checking.  When I bench mark it, there is a package which I compile with bounds checking off, and it makes quite a significant difference on some problems.

So it seems to me, from the points above, that gophersat will probably be better, is questionable. 

My take is this:  anybody using SAT in an actual application needs to benchmark for that application.  It might well even be that 

any difference between solvers is simply irrelevant performance-wise.    

Don't take my word for it, or gophersat's authors word for it.  Bench mark.  You can use the tool "bench" with gini to easily do this for cnf at least for any solver.

(Also, Gini now supports cardinality constraints.  It uses a simple mechanism which is known to be effective for a wide number of use cases and has absolutely no overhead w.r.t. solving problems without cardinality constraints.  Handling cardinality constraints is also difficult to predict;  I recommend ignoring all expert opinions about who is better and simply benchmark).

Scott