Format DIMACS

DIMACS (Input)

Short Description

The DIMACS format is the official formal used by the SAT Competition (more-or-less since the very beginning).

Syntax

There is an old description from the 90s that diverges from the current format as defined by the SAT Competition.

The file contains comments (starting by a 'c'). Then it contains a header.

p cnf <number-of-literals> <number-of-clauses>

Every clause is given by a list of literals (using a / -a where a is an integer smaller than the number given in the header). The separator '0' is used to separate clauses, but usually '0' followed by a line break is used.

Remark that many solvers support compressed files as input and decompress the files as needed. Various tools support only a subset of the input proof format (like comments in the middle of the clauses).

Example

Here is the beginning of a file:

c STATUS SATISFIABLE
p cnf 2718 45039
-1 -2 0
-1 12 0
-2 12 0
-3 -4 0