School of
Electrical Engineering
and Computer Science
KTH / CSC / Theory Group / Jakob Nordström / Teaching / DD2445 Complexity Theory Autumn 2015 / MiniSat and DIMACS

Some Information About MiniSat and the DIMACS Format


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

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

(xy) ∧ (∼yz)

(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.

Published by: Jakob Nordström <jakobn~at-sign~kth~dot~se>
Updated 2015-09-30