Some Information About MiniSAT and the DIMACS Format
MiniSAT
A version of MiniSAT should now be available on (essentially) all
Ubuntu Linux machines at KTH CSC using the command
minisat2.
Please send an e-mail to the CSC systems group 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
minisat2 <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
minisat2 -h
will give a list of some MiniSAT options.
The DIMACS Format
For our purposes, all we need to know about the DIMACS format is
the following (simplified) description.
The example 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.
