This repository archives and restores various versions and derivatives of MiniSat written by various authors over the years. The original MiniSat is written and Copyright © 2003-2006 Niklas Eén, Copyright © 2003-2010 Niklas Sörensson, and distributed under the terms of the MIT license.
You may be wondering, what is MiniSat? What is SAT?
-
build-all— compiles and builds most of the versions here. This requires git and all of this repository's branches to be cloned — an ordinarygit clone https://github.com/notwa/minisat/will suffice. Note that only Linux is currently supported. -
check-all— gathers information about the solvers in thebindirectory created bybuild-all.
You can download any of the versions on GitHub by following the appropriate link and clicking on the green "Clone or download" link on the top right. Select "Download Zip" if you're not familiar with git.
This is just a clone of the upstream master branch.
A version based on Niklas's most recent work is patched and ready to compile with modern compilers.
This is the ubiquitous version of MiniSat that most of its derivatives are based on.
This is the first release of MiniSat 2 that glucose-1.0 is based on.
A few select versions are available on the MiniSat homepage.
Various patch files have been archived. Some of these are used for the build script.
Chanseok Oh's patches have been applied to MiniSat 2.2.0, essentially turning it into glucose-2.3.
Chanseok Oh's other set of patches have been applied to MiniSat 2.2.0, behaving similar to glucose-2.3. This serves as a starting point for MiniSat hack competitions, in which a limited edit distance is imposed.
Ranking first on the main track of the 2016 SAT Competition, this is based on COMiniSatPS.
This is based on MapleCOMSPS.
Ranking first on the main track of the 2017 SAT Competition, this adds a distance heuristic to MapleLCM, which in turn is based on MapleCOMSPS. Note that a patch is available to fix a crash in MapleLCMDist's DRUP-outputting code.
Ranking first on the main track of the 2018 SAT Competition, this is based on MapleLCMDist.
Ranking first in the 2019 SAT Race, this is based on MapleLCMDistChronoBT.
Note that this appears to be typo'd as MapleLCMDisc in the competition.
The original Glucose via the Glucose homepage, based on MiniSat 2.0. Glucose is Copyright © 2009-2017 Gilles Audemard, Laurent Simon.
The next Glucose via the Glucose homepage, based on MiniSat 2.2.0.
This is an update to glucose 2.0. Note that there is a crash specific to this version that has yet to be patched.
This version is currently missing. It was removed from the Glucose homepage.
This update to glucose 2.2 was later cleaned up and released as glucose 3.0. This version was taken from the 2013 SAT Competition.
Note that this commit is currently missing from all subsequent branches of Glucose.
This is a cleaned up version of Glucose 2.3, via the Glucose homepage.
This version was used as a base for the Glucose Hack Track of the 2016 SAT Competition.
This version, also known as Glucose-Syrup, adds a parallel version of Glucose, plus some other improvements.
There is an earlier version of 4.0 that is currently absent.
This is an incremental improvement over Glucose 4.0.
These versions have been omitted from this repository because they are already readily accessible.
CryptoMiniSat is a major rewrite of MiniSat, adding many features, including XOR clauses for improved solving of cryptographic problems. CryptoMiniSat is written and maintained by Mate Soos on the CryptoMiniSat GitHub repository.
Some of these versions may later be archived in git branches, but for the time being, there are:
-
MiniSat derivatives from 2016 submitted to the SAT Competition of 2016.
-
MiniSat derivatives from 2017 submitted to the SAT Competition of 2017.
-
MiniSat derivatives from 2018 submitted to the SAT Competition of 2018.
-
MiniSat derivatives from 2019 submitted to the SAT Race of 2019.
-
and many more from the various competitions and races held in the past and to be held in the future.
MiniSat is a SAT solver that has been applied to complete many tasks over the years. SAT is an abbreviation for satisfiability. SAT solvers solve boolean satisfiability problems, with the possible outcomes of satisfiable, unsatisfiable, or unknown/indeterminate, often alongside a solution or proof. SAT problems are NP-complete.
SAT solvers also serve as a base for most SMT solvers. SAT solvers are restricted to problems given in conjunctive normal form, whereas SMT solvers work with problems described more abstractly. SMT is an acronym for Satisfiability Modulo Theories. An example of an SMT solver is the Simple Theorem Prover (STP), which employs a version of MiniSat.
A very informal overview of using SAT and SMT solvers is given by Dennis Yurichev's SAT/SMT by Example. Further information (and slightly dated resources) is available in SATLIB — The Satisfiability Library.
MiniSat is a popular basis for experimenting with new ideas to solve problems more efficiently, due to the software's code being relatively short and simple. MiniSat's many derivatives have ranked on or won many competitions, under many names such as COMSPS, Glucose, Maple, and more.
There are solvers that are not based on MiniSat. For example, PicoSAT and yices, the latter being an SMT solver. CaDiCaL is another solver from the authors of PicoSAT with highly competitive performance.