by David A. Wheeler, version 1.00 (2008-06-28)
MiniSat is a minimalistic, open-source Boolean satisfiability problem (SAT) solver, developed for both researchers and developers; it is released under the "MIT license".
A SAT solver can determine if it is possible to find assignments to boolean variables that would make a given expression true, if the expression is written with only AND, OR, NOT, parentheses, and boolean variables. If it's satisfiable, most SAT solvers (including MiniSAT) can also show a set of assignments that make the expression true. Many problems can be broken down into a large SAT problem (perhaps with thousands of variables), so SAT solvers have a variety of uses.
This article is a brief user guide (documentation) for the MiniSAT (MiniSAT2) program. It describes how to use MiniSAT, including its input format, options, and output format.
Like many SAT solvers, MiniSAT requires that its input be in conjunctive normal form (CNF or cnf). CNF is built from these building blocks:
An example of CNF is:
(x1 | -x5 | x4) & (-x1 | x5 | x3 | x4) & (-x3 | x4).
Any boolean expression can be converted into CNF; algorithms and code for doing so are available elsewhere (e.g., see "Artificial Intelligence: A modern Approach" by Russel and Norvig, 1995).
MiniSAT, like most SAT solvers, accepts its input in a simplified "DIMACS CNF" format, which is a simple text format. Every line beginning "c" is a comment. The first non-comment line must be of the form:
p cnf NUMBER_OF_VARIABLES NUMBER_OF_CLAUSES
Each of the non-comment lines afterwards defines a clause. Each of these lines is a space-separated list of variables; a positive value means that corresponding variable (so 4 means x4), and a negative value means the negation of that variable (so -5 means -x5). Each line must end in a space and the number 0.
So the CNF expression above would be written as:
c Here is a comment. p cnf 5 3 1 -5 4 0 -1 5 3 4 0 -3 -4 0
The "p cnf" line means that this is SAT problem in CNF format with 5 variables and 3 clauses. The first line after it is the first clause, meaning x1 | -x5 | x4.
You can view this as a single expression. Alternatively, you can view this as a set of clauses, and the solver's job is to find the set of boolean variable assignments that make all the clauses true.
The SAT 2004 competition has more information.
MiniSAT's usage is:
minisat [options] [INPUT-FILE [RESULT-OUTPUT-FILE]]
The INPUT-FILE is in DIMACS CNF format as described above, either plain text or gzipped. You can invoke it with the options "-h" or "--help" to see the other options.
The program's options include:
-pre = {none,once} [Turn on preprocessor]
-asymm
-rcheck
-grow = NUM [ must be greater than 0 ]
-polarity-mode = {true,false,rnd}
-decay = NUM [ 0 - 1 ]
-rnd-freq = NUM [ 0 - 1 ]
-dimacs = OUTPUT-FILE
-verbosity = {0,1,2}
Options with a value must be immediately followed by "=" and its value, e.g.:
minisat -pre=once
For many problems, using the preprocessor is a good idea (-pre=once).
When run, miniSAT sends to standard error a number of different statistics about its execution. It will output to standard output either "SATISFIABLE" or "UNSATISFIABLE" (without the quote marks), depending on whether or not the expression is satisfiable or not.
If you give it a RESULT-OUTPUT-FILE, miniSAT will write text to the file. The first line will be "SAT" (if it is satisfiable) or "UNSAT" (if it is not). If it is SAT, the second line will be set of assignments to the boolean variables that satisfies the expression. (There may be many others; it simply has to produce one assignment).
So for the example above, it will produce in the output file:
SAT 1 2 -3 4 5 0
This means that it is satisfiable, with x1=t, x2=t, x3=f, x4=t, and x5=t (where t is true and f is false). Going back to our original example, we should see that this is a solution:
(x1 | -x5 | x4) = t | -t | t = t (-x1 | x5 | x3 | x4) = -t | t | f | t = t (-x3 | x4) = -f | t = t
If you want to get another solution, the "obvious" way is to add, as a new clause, the negated form of the previous solution. E.G., for our example, we could take:
1 2 -3 4 5 0and create this new input (note that the count of clauses has increased):
p cnf 5 4 1 -5 4 0 -1 5 3 4 0 -3 -4 0 -1 -2 3 -4 -5 0
If we put this in file "second.in", and run:
minisat second.in second.outWe will get a new solution; here's second.out:
SAT 1 -2 -3 4 5 0IE., x1=t, x2=f, x3=f, x4=t, and x5=t. This is a different solution from the previous one, because x2=f instead of x2=t. We can confirm this (it's the same as last time, because x2 isn't even in any of the clauses):
(x1 | -x5 | x4) = t | -t | t = t (-x1 | x5 | x3 | x4) = -t | t | f | t = t (-x3 | x4) = -f | t = t
You can get more information from:
This article was written by David A. Wheeler, and is released to the public domain. If you use it or reference it, please credit David A. Wheeler (though this is not a requirement for its use). You can get this version at http://www.dwheeler.com/essays/minisat-user-guide-1.0.html, or the latest version at http://www.dwheeler.com/essays/minisat-user-guide.html.