DIMACS CNF

DIMACS CNF is the plain-text format in which formulas in conjunctive normal form are given to SAT solvers^[1]. Variables are numbered from 1, and a literal is written as a signed integer: 3 for $x_3$ and -3 for $\neg x_3$. A file consists of comment lines beginning with c, one header line p cnf V C stating the number of variables and clauses, and then the clauses, each a sequence of literals terminated by 0. The format was proposed for the Second DIMACS Implementation Challenge on cliques, colouring and satisfiability, held in 1992 and 1993 by the Center for Discrete Mathematics and Theoretical Computer Science^[2], and it has been the common input language of SAT solvers and benchmark collections ever since.

The rules are few^[1]:

Lines beginning with c are comments and may appear before the header. The header p cnf V C comes before any clause; V is the largest variable number and C the number of clauses. Clauses are sequences of whitespace-separated literals, each ending with 0; line breaks carry no meaning, so a clause may span several lines or several clauses may share one, although one clause per line is the norm. The empty clause is written as a lone 0 and makes the formula unsatisfiable.

Some details are left to the reader. The original specification permits variables that do not occur in any clause, and solvers must treat them as unconstrained. Most solvers tolerate a clause count that differs from the header, or a missing header, but strict parsers reject them. Older benchmark files, including the uniform random formulas of SATLIB, end with a line containing % and a stray 0, which parsers commonly skip^[3]. Files are often compressed, and solvers such as MiniSat read gzip-compressed input directly^[8].

(* The DIMACS CNF format: comment lines start with c, the header is
   p cnf <variables> <clauses>, and each clause is a list of literals
   ended by 0. Clauses may span lines. *)
let parse_dimacs (text : string) : cnf =
  let words = ref [] and header = ref None in
  List.iter (fun line ->
      let line = String.trim line in
      if line = "" || line.[0] = 'c' || line.[0] = '%' then ()
      else if line.[0] = 'p' then
        Scanf.sscanf line "p cnf %d %d" (fun v c -> header := Some (v, c))
      else
        String.split_on_char ' ' line |> List.filter (( <> ) "")
        |> List.iter (fun w -> words := int_of_string w :: !words))
    (String.split_on_char '\n' text);
  let nvars, nclauses = match !header with Some h -> h | None -> failwith "no p line" in
  let clauses, current =
    List.fold_left (fun (cs, cur) l -> if l = 0 then (List.rev cur :: cs, []) else (cs, l :: cur))
      ([], []) (List.rev !words) in
  if current <> [] then failwith "last clause not terminated by 0";
  if List.length clauses <> nclauses then failwith "clause count differs from header";
  List.iter (List.iter (fun l -> if abs l > nvars then failwith "variable out of range")) clauses;
  { nvars; clauses = List.rev clauses }
 
let print_dimacs f =
  Printf.sprintf "p cnf %d %d\n" f.nvars (List.length f.clauses)
  ^ String.concat "" (List.map (fun c ->
      String.concat " " (List.map string_of_int (c @ [0])) ^ "\n") f.clauses)

let example = {|c A small instance: three clauses over three variables.
c (x1 or not x2 or x3) and (not x1 or x2) and (not x3)
p cnf 3 3
1 -2 3 0
-1 2 0
-3 0
|}
 
(* The output format of the SAT competitions: a status line, then the
   model on v lines, ended by 0. *)
let report f =
  match fst (Cdcl.solve f) with
  | Cdcl.Sat model ->
    print_endline "s SATISFIABLE";
    print_endline ("v " ^ String.concat " " (List.init f.Cnf.nvars (fun i ->
        string_of_int (if model.(i + 1) then i + 1 else - (i + 1)))) ^ " 0")
  | Cdcl.Unsat -> print_endline "s UNSATISFIABLE"
  | Cdcl.Unknown -> print_endline "s UNKNOWN"

p cnf 3 3
1 -2 3 0
-1 2 0
-3 0
s SATISFIABLE
v -1 -2 -3 0
s UNSATISFIABLE
rejected: last clause not terminated by 0
rejected: clause count differs from header
rejected: variable out of range

The SAT competitions fix the output as well^[4]. A solver prints a status line, s SATISFIABLE, s UNSATISFIABLE or s UNKNOWN; for a satisfiable formula it prints the model on one or more lines beginning with v, as the literals true in the assignment, ended by 0. By convention the process also exits with status 10 for satisfiable and 20 for unsatisfiable formulas, so scripts can test the result without parsing the output. Comment lines beginning with c may carry statistics.

An unsatisfiability claim is backed by a proof written to a separate file. The DRAT format uses the same conventions as DIMACS: each line is a clause that the solver has learned, ended by 0, or the same prefixed by d for a clause it has deleted, and an independent checker verifies that each added clause follows from the ones before it^[6].

QDIMACS extends the format to quantified Boolean formulas by inserting quantifier lines after the header: e 1 2 0 declares variables 1 and 2 existential and a 3 0 declares variable 3 universal, in order from the outermost quantifier^[5]. WCNF, used by the MaxSAT evaluations, gives each clause a weight as its first number, with hard clauses that must be satisfied marked by a designated top weight or, in the newer format, by h^[7]. The same challenge also standardized a format for graphs, p edge V E followed by lines e u v, which is still used for colouring and clique benchmarks^[2].

The Center for Discrete Mathematics and Theoretical Computer Science (DIMACS) at Rutgers University ran its Second Implementation Challenge in 1992–1993 on three NP-hard problems: finding cliques, colouring graphs and deciding satisfiability. To allow solvers to be compared on shared benchmarks, the organizers proposed simple input formats, including the CNF format described here^[1][2]. The benchmark library SATLIB, begun in the late 1990s, distributed thousands of instances in the format^[3], and the SAT competitions, held since 2002, use it for all their tracks^[4]. The format has remained unchanged apart from the conventions for output and proofs that the competitions added.

• SATThe Boolean satisfiability problem, SAT, asks whether some assignment of true and false to the variables of a propositional formula makes the formula true. It was the first problem shown to be NP-complete, so every problem in NP reduces to it, and no polynomial-time algorithm is known. In practice SAT solvers based on conflict-driven clause learning decide industrial instances with millions of variables, which has made SAT a general-purpose engine for hardware and software verification, planning, scheduling and combinatorics.
• CNFA propositional formula is in conjunctive normal form (CNF) when it is a conjunction of clauses, each clause a disjunction of literals, and each literal a variable or its negation. Every formula is equivalent to one in CNF, but the equivalent CNF can be exponentially larger; the Tseitin transformation instead produces an equisatisfiable CNF of linear size by adding variables. CNF is the input format of SAT solvers and resolution provers, and restricted forms such as Horn clauses and 2-CNF can be solved in linear time.
• Pigeonhole formulaThe pigeonhole formulas PHPⁿ⁺¹ₙ are CNF formulas stating that n + 1 pigeons can be placed in n holes with no two in the same hole. They are unsatisfiable, as the pigeonhole principle says, but Haken proved in 1985 that every resolution refutation of them has exponential size. Since SAT solvers based on DPLL and CDCL produce resolution proofs, they need exponential time on these small formulas, which makes the family the standard example of what resolution cannot do. Proof systems that can count, such as cutting planes and extended resolution, refute them in polynomial size.
• Tseitin transformationThe Tseitin transformation converts an arbitrary propositional formula or Boolean circuit into conjunctive normal form in linear time by introducing a new variable for each subformula and adding a few clauses that define it as the result of its operator: g ↔ a ∧ b becomes (¬g ∨ a), (¬g ∨ b) and (g ∨ ¬a ∨ ¬b). The result is not equivalent to the original formula but equisatisfiable, and every model of one extends or restricts to a model of the other. It is how SAT solvers receive circuits and structured formulas; the Plaisted–Greenbaum variant emits only the implications required by each subformula's polarity, roughly halving the clauses.

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

1. [1]DIMACS, “Satisfiability suggested format” (1993), from the Second DIMACS Implementation Challenge.
2. [2]D. S. Johnson, M. A. Trick (eds.), Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, DIMACS Series in Discrete Mathematics and Theoretical Computer Science 26, American Mathematical Society (1996).
3. [3]H. H. Hoos, T. Stützle, “SATLIB: an online resource for research on SAT”, in SAT 2000, IOS Press (2000).
4. [4]SAT Competition, “Input and output format requirements”.
5. [5]QBFLIB, “QDIMACS standard, version 1.1” (2005).
6. [6]N. Wetzler, M. J. H. Heule, W. A. Hunt, “DRAT-trim: efficient checking and trimming using expressive clausal proofs”, SAT (2014).
7. [7]MaxSAT Evaluation, “Input format”.
8. [8]N. Eén, N. Sörensson, “An extensible SAT-solver”, SAT, Lecture Notes in Computer Science 2919 (2004).

last updated 28 September 2026