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_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.
	MiniSat_v1.13_src.zip	-	The SAT 2005 competition version. It's hacked up and a bit ugly, but it is fast and it works.
	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.src.zip	-	If you despise C++, here is an experimental C version by Niklas Sörensson
	MiniSat-STL_v1.14.src.zip	-	A version based on STL instead of our home-brewed dynamic vector "vec" and quick-sort implementation. Well, actually not. We are waiting for someone with a thorough knowledge of STL to do this for us (you?). One of the Niklases refuses to use STL because he doesn't understand it properly.
Pre-compiled binaries...
	MiniSat_v1.13_linux	-	Statically linked Linux binary.
	MiniSat_v1.13_cygwin	-	Cygwin/Windows binary.