# Dimacs

DIMACS format is a standard interface to SAT solvers.

Many SAT solvers accept a common format for input and output that
is used in SAT solving competititons;
this page gives the competitions' official description.

The basic input format is as follows. At the top you can have *comment
lines* that start with a c, like this:

c This line is a comment.

Then comes the *problem line*, which starts with a p and then says
how many variables and clauses there are. For instance, here is a problem line
that says this is a CNF problem with 3 variables and 4 clauses:

p cnf 3 4

Finally the clauses are listed. Each clause is represented as a list of
numbers like 3 and -42. A positive number like 3 represents a
positive occurrence of variable 3. A negative number like -42 represents
a negated occurrence of variable 42.

The number 0 is treated in a special way: it is not a variable, but
instead marks the end of each clause. This allows a single clause to be split
up over multiple lines.

### Input Format Questions and *Clean* Formulas

If we could be sure the above document was the standard, we could very
easily convert from our cnf representation into it. The only twist is
that 0 isn't a valid identifier in DIMACS format, but it is a valid identifier
in our representation. To get around this, we can just add one to every
variable number throughout the problem.

However, the SAT competitions generally use a simplified version of the
DIMACS format. For instance, the 2012 SAT competititon used the same rules as the 2011
competititon and for previous years, and restrict the format so that the
solver may assume:

- Each variable, from 1 to the number of variables specified on the problem
line, is used at least once in some clause.
- The clauses are distinct and may not simultaneously contain opposite
literals.
- There are exactly the right number of clauses given in the problem
line.
- Clauses are kept on the same line.

It appears that the rules do not rule out empty clauses.

**BOZO** Eventually, we would like to make sure we produce DIMACS files
that conform to these more stringent requirements, since otherwise a SAT solver
that believes it can make these assumptions may make a mistake. We may
eventually add a cleaning phase to our SAT integration, to ensure that we only
call the SAT solver on "clean" formulas.

### Subtopics

- Dimacs-export
- Writer to translate cnf formulas into DIMACS files.
- Dimacs-interp
- How we interpret the DIMACS formatted output from the SAT solver.