Some Information About MiniSat and the DIMACS Format
MiniSat
A version of MiniSat should be available on (essentially) all
Ubuntu Linux machines at KTH CSC using the command
minisat.
Please send an e-mail to KTH IT support if this does not work for you.
If you want to play around with MiniSat on your own computer, you can
download and install the solver from the webpage
www.minisat.se.
The suggested way of running MiniSat is to do
minisat <CNF formula file> <output file>.
MiniSat will then read the CNF formula in DIMACS format from
the input file and report the result on the output file.
If the solver determines that the formula is unsatisfiable, it writes
UNSAT.
If it finds the formula to be satisfiable, it writes
SAT
followed by the signs of the variables
(positive=true, negative=false)
in a satisfying assignment.
Doing
minisat --help
will give a list of some MiniSat options.
The DIMACS Format
For our purposes, all we need to know about the DIMACS format, which
is the de facto standard format for SAT solving, is the following
(simplified) description. The example CNF formula
(x
∨
y)
∧
(∼y
∨
z)
(where we write ∼ for negation)
can be coded in DIMACS format as the following file:
c All of this line is a comment
c This an encoding of the CNF formula mentioned above
p cnf 3 2
1 2 0
-2 3 0
Or in words:
-
The file can start with comments, which are lines beginning with the character
c.
-
Then follows a line
p cnf <nvars> <nclauses>
specifying the exact number of variables and clauses in the formula.
-
After this the clauses follow, one per line,
where each line is a list of integers of
absolute value at most
<nvars>
terminated by 0 (zero).
The variables are assumed to be indexed from 1 to <nvars>
and a minus sign means negation. Zero just means end of clause.
