Registered 2009-01-23 by Paulo Trezentos

Minisat+ is a solver based on 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 an objective function).

Project information

Paulo Trezentos
Not yet selected
MIT / X / Expat Licence

RDF metadata

View full history Series and milestones

trunk series is the current focus of development.

All code Code

Version control system:

All packages Packages in Distributions

Get Involved

  • warning
    Report a bug
  • warning
    Ask a question
  • warning
    Help translate


minisat+ does not have any download files registered with Launchpad.