MiniSat+

MiniSat+ is a two-week hack done to enable MiniSat to compete in the new categories of the SAT 2005 competition. Initially, we intended to support both Pseudo-Boolean constraints (i.e. linear constraints over boolean variables) and circuit based SAT input (as opposed to CNF). However, after we finished the conversion of PB-constraints to SAT, we ran out of steam and never finished the other part.

However, the PB part is, arguably, the more interesting one. A number of generalizations of SAT solvers to PB solvers have been proposed (Pueblo, Galena, OPBDP and more), but we felt that the other approach — converting the problem to SAT — had not been invesigated adequately. Our hope was to provide a point of reference for the proper generalizations of SAT to PB, so that the merit of such an approach could be evaluated. Therefore MiniSat+ provides multiple ways of translating PB constraints to clauses.

For the PB evaluation 2005, we provided a top-level heuristic to choose between the translation methods. To our surprise, MiniSat+ solved more problem than any of the other 6 dedicated PB solvers did, and also seemed to one of the few solvers not being visibly buggy (modulo giving the wrong exitcode for SATISFIABLE instances without a goal function).

We are working on a paper describing the translation methods used in MiniSat+. In the meantime you can download the source-code and/or binaries and play around with it. Bear in mind, though, that the source is a quick hack, and very much provided on an "AS IS"-basis...

To download the source code and statically linked Linux binaries, click here.