by Niklas Eén, Niklas Sörensson
MiniSat
MiniSat started out 2003 as an effort to help people get into the SAT community by providing a small, yet efficient, SAT solver with good documentation (through the following paper). The first version was just above 600 lines, not counting comments and empty lines, while still containing all the features of the current state-of-the-art solvers in 2003 (conflict-clause recording, conflict-driven backjumping, VSIDS dynamic variable order, two-literal watch scheme), and even extensions for incremental SAT and for non-clausal constraints over boolean variables.
In later versions, the code base has grown a bit to emcompass recent improvements, but is still quite small and hopefully readable. In the SAT competition 2005, version 1.13 proved that MiniSat still is state-of-the-art; at least for publically available solvers.
Below we provide a set of different versions of MiniSat to suit the needs of different applications. We encourage you to submit bugfixes, extensions and suggestions for improvements, as well as basing products on MiniSat. The solver is available under the MIT licence, a strictly freer licence than the LGPL, basically allowing you to use the code as you like.
| Source code... | |||
| minisat-2.2.0.tar.gz | - | The first public release after a period of inactivity. Similar in performance to the version that won in SAT-Race 2008 but with some clean-ups and minor feature additions. For more info, see the release notes. | |
| minisat2-070721.zip | - | This is the first release of MiniSat 2, featuring variable elimination style simplification natively. It is a cleaned up version of the winning entry of SAT-Race 2006 and is intended to subsume SatELite and SatELiteGTI. Documentation is scarce at the moment, but feel free to send questions to the mailinglist (minisat@googlegroups.com). | |
| MiniSat_v1.14_src.zip | - | The cleaned-up verison of "v1.13" with the last minute hacks properly implemented (e.g. the hack in "simplifyDB()"), and the worst code abuse removed. Names and comments have also been improved. It performs just as good as the 1.13, but due to the small changes, it may perform differently on individual problems. | |
| MiniSat-p_v1.14.src.zip | - | Proof-logging version. This is a new feature, but there is a risk that it works. To simplify the code a bit, the binary-clause trick in the non-proof-logging version has been removed, making it a constant 10-20% slower. But if you need proof-logging, here it is. | |
| MiniSat-C_v1.14.1.src.zip | - | If you despise C++, here is an experimental C version by Niklas Sörensson | |
| MiniSat_v1.12b_src.zip | - | This version still supports non-clausal constraints. The new improved variable order from version 1.13 is backported to this "b"-version of 1.12. | |
| sat2005_submission.zip | - | This archive contains the SAT 2005 competition version. It's hacked up and a bit ugly, but it is fast and it works. | |
| MiniSat_v1.14_VC-080206.patch | - | A patch for MiniSat v1.14 to compile under MS Visual Studio (based on submission by Jean Gressmann). | |
| MiniSat_v1.14_gcc41.patch | - | A patch to the "friends" declaration of "SolverTypes.h" to compile under GCC 4.1 (and probably other compilers too) (submitted by Peter Hawkins). | |
| MiniSat_v1.14 for C# | - | Link to Michal Moskal's C# version of MiniSat. | |
| MiniSat_v1.14 wrapper for OCAML | - | Link to Flavio Lerda Home Page . | |
| Pre-compiled binaries... | |||
| MiniSat_v1.14_linux | - | Statically linked Linux binary. | |
| MiniSat_v1.14_cygwin | - | Cygwin/Windows binary. | |