DIMACS CNF

All formats · Reader spec · Cases and output

dimacs-cnf.iris reads a p cnf header and the declared number of zero-terminated clauses. It skips c comments and stops at % for SATLIB-style tails. Data contains vars, clauses, and the ragged clause array; terminating zeros are consumed without being stored.

The format source is DIMACS, Satisfiability: Suggested Format, §2.1. The reader spec is copied from Gecode’s sat.cpp.

• three-variables has three variables and three clauses of different lengths.
• literal-out-of-range declares three variables but uses literal 4. The reference reports E-EXPECTED-VALUE at input line 2, column 3.

These are hand-made samples under the repository’s MIT license. See the library README for case layout, validation, and Gecode notices.

Reader spec

From Gecode commit 5e7bbd5c26b0702c6fd652356b2289da0710ac3c. Source notices.

dimacs-cnf.irisView full reader spec

format dimacs-cnf

comment "c"
stop "%" # SATLIB files end with "%" and "0"
line "p cnf {vars:0..gecode.int_max} {clauses:0..}"
repeat clauses {
  list clause: -vars..vars until 0 # the terminating 0 is not stored
}

Cases and output

Run the commands from the repository root. Successful reads show dzn, JSON, and a summary. Rejected inputs show the CLI's diagnostic and caret, with the stable error code beside it.

literal-out-of-range

Literal exceeds the declared variable count

InputView full input

p cnf 3 1
1 4 0

E-EXPECTED-VALUE

expected an int in -3..3, found '4'

Read rejectedRun from the repository root.

$ iris read formats/dimacs-cnf/dimacs-cnf.iris formats/dimacs-cnf/cases/literal-out-of-range/input.txt --dzn

formats/dimacs-cnf/cases/literal-out-of-range/input.txt:2:3: expected an int in -3..3, found '4'
     2 | 1 4 0
       |   ^
while reading: repeat [1 of 1] > clause
spec: formats/dimacs-cnf/dimacs-cnf.iris:7

Input rejected

View full diagnosticDownload error JSON

Download full case · Open in playground

three-variables

Three variables and three clauses

InputView full input

c Hand-made three-variable formula
p cnf 3 3
1 -2 0
2 3 -1 0
-3 0

dzn

iris read formats/dimacs-cnf/dimacs-cnf.iris formats/dimacs-cnf/cases/three-variables/input.txt --dzn

dznView full dzn

vars = 3;
clauses = 3;
% clause: array[int] of tuple(array[int] of int)
clause = [([1, -2],), ([2, 3, -1],), ([-3],)];

JSON

iris read formats/dimacs-cnf/dimacs-cnf.iris formats/dimacs-cnf/cases/three-variables/input.txt --json

JSONView full json

{"iris":"0.1","entries":[{"name":"vars","type":"int","depth":0,"value":3},{"name":"clauses","type":"int","depth":0,"value":3},{"name":"clause","type":"int","depth":2,"value":[[1,-2],[2,3,-1],[-3]]}]}

Summary

iris read formats/dimacs-cnf/dimacs-cnf.iris formats/dimacs-cnf/cases/three-variables/input.txt --summary

SummaryView full summary

formats/dimacs-cnf/cases/three-variables/input.txt [dimacs-cnf]
  vars: int 3
  clauses: int 3
  clause: int array 3 x 1..3

Download full case · Open in playground