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 This line is a comment.
Then comes the problem line, which starts with a
p cnf 3 4
Finally the clauses are listed. Each clause is represented as a list of
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:
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.