Home
Download
Compilation
Usage
DIMACS format
ISCAS/RTL format

DIMACS CNF format

This format is widely accepted as the standard format for boolean formulas in CNF. Benchmarks listed on satlib.org, for instance, are in the DIMACS CNF format.

An input file starts with comments (each line starts with c). The number of variables and the number of clauses is defined by the line p cnf variables clauses

Each of the next lines specifies a clause: a positive literal is denoted by the corresponding number, and a negative literal is denoted by the corresponding negative number. The last number in a line should be zero. For example,

c A sample .cnf file.
p cnf 3 2
1 -3 0
2 3 -1 0