		Search-engine friendly clone of the ACL2 documentation.

Satlink

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.