Introduction

MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT. It is released under the MIT licence, and is currently used in a number of projects (see "Links"). On this page you will find binaries, sources, documentation and projects related to MiniSat, including the Pseudo-boolean solver MiniSat+ and the CNF minimizer/preprocessor SatELite. Together with SatELite, MiniSat was recently awarded in the three industrial categories and one of the "crafted" categories of the SAT 2005 competition (see picture).

Some key features of MiniSat:

• Easy to modify. MiniSat is small and well-documented, and possibly also well-designed, making it an ideal starting point for adapting SAT based techniques to domain specific problems.
• Highly efficient. Winning all the industrial categories of the SAT 2005 competition, MiniSat is a good starting point both for future research in SAT, and for applications using SAT.
• Designed for integration. MiniSat supports incremental SAT and has mechanisms for adding non-clausal constraints. By virtue of being easy to modify, it is a good choice for integrating as a backend to another tool, such as a model checker or a more generic constraint solver.

Remember! MiniSat is open-source, so please contribute to this page by submitting bugfixes, extensions, comments, links, or any other material you produce, or know of, that relates to MiniSat!

News

From newest to oldest...

• A C version of MiniSat v1.14 released.
• The cleaned up version v1.14 of the competing solver released, now including proof logging.
• Source code for MiniSat v1.13 and SatELite 1.0, competing in SAT 2005 released.
• The PB solver MiniSat+ v0.99 released.
• MiniSat and SatELite won the industrial categories of the SAT 2005 competition.
• All MiniSat related information finally collected into a web page.