DIMACS CNF

also: dimacs

The plain-text interchange format for CNF instances: a header giving the variable and clause counts, then one clause per line as space-separated nonzero integers terminated by a zero, with a negative integer meaning a negated variable. Every SAT solver reads it, which is what makes solvers comparable at all.

The interchange format every SAT solver reads. A header line gives the counts, then each clause is a line of space-separated nonzero integers terminated by 0, with $- k$ meaning the negation of variable $k$ .

(x1 or x2) and (not x1 or x2) and (not x2): three clauses over two variables.

c a comment line
p cnf 2 3
1 2 0
-1 2 0
-2 0

The format is deliberately minimal, which is what makes it universal: variables are numbered rather than named, there is no syntax for anything but a clause, and the header lets a reader size its arrays in one pass. Every competition instance and benchmark suite is distributed in it, so it is also the reason independent solvers are comparable at all.

Implementing SAT in OCaml Part 1CNF, unit propagation, a full recursive DPLL solver, pure literal elimination, a DIMACS parser, and a command-line driver.