  School of
Electrical Engineering
and Computer Science
 KTH / CSC / Theory Group / Jakob Nordström / Teaching / DD3501 Current Research in Proof Complexity 2011/12 / MiniSAT and DIMACS

# 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

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