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.

We would like to start a community to help distribute knowledge about how to use and modify MiniSat. Any questions, comments, bugreports, bugfixes etc. should be directed to minisat@googlegroups.com. The archives can be browsed here. The source code repository for MiniSat 2.2 can be found at github.

— Niklas & Niklas

News

From newest to oldest...

A paper on how to compute localization abstractions using the incremental interface of MiniSat. View this as an example of a non-trivial incremental SAT application. A key feature of the algorithm is the use of analyzeFinal() to get the subset of assumptions used in the UNSAT proof.
Finally! A new release of MiniSat, downloads/minisat-2.2.0.tar.gz. For more info, see the release notes.
Paper on Cut-sweeping added, a light-weight alternative to SAT-sweeping useful for preprocessing AIGs before applying SAT.
Added slides for invited talk given by Niklas Een at FMCAD (Linux/Cygwin/Windows)
Paper on efficient CNF generation added (slides also available).
Bug-fix in MiniSat+ for trivially unsatisfiable instances.
MiniSat v.2.0 has been released.
Bug-fix to the proof-logging version of MiniSat (thanks to Georg Weißenbacher for reporting the problem!).
Bug-fix to the C-version of MiniSat.
Paper on MiniSat+ added.
Removed version 1.13 of MiniSat. It was an intermediate version that apperently was buggy.
Patch for Visual Studio users added.
Buggy v1.13 Cygwin binary replaced with working v1.14 binary. The bug did not affect the Linux version.
Fixed the output of MiniSat+ so that it is flushed properly when stdout is redirected to a file.
Fixed a silly bug in MiniSat that caused it to crash on the empty SAT problem if a random variable was picked by the branching heuristic.
Added slides for the invited talk given by Niklas Sörensson at ESCAR (under Papers).
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.