1. Read DIMACS CNF

A DIMACS CNF file starts with a p cnf header. It declares the number of Boolean variables and clauses. Each clause is a sequence of signed variable numbers followed by 0. A negative number denotes a negated variable.

Start with the header, then add the clause body. All commands below run from the repository root; see the tutorial setup.

Capture the header

A line pattern matches a whole remaining line. Literal text checks p cnf; the two captures read integers and store them as vars and clauses. The ranges reject negative counts. gecode.int_max is a host constant, fixed at 2147483646, which the library reader uses as the upper bound.

line "p cnf {vars:0..gecode.int_max} {clauses:0..}"

For now the input contains only a header. The reader spec must consume the whole input, so save the clauses for the next stage.

p cnf 3 3

iris read site/examples/tutorial/dimacs-header.iris site/examples/tutorial/dimacs-header.txt --dzn

vars = 3;
clauses = 3;

--dzn prints named MiniZinc data assignments. The two captures produce two scalar integer entries. See the Specification’s line patterns and ranges.

Add comments and clauses

Declare comment "c" at the top level to skip input comments. # introduces a comment in the reader spec itself. These are separate conventions.

repeat clauses runs its body exactly that many times. A list reads until its sentinel, consuming the terminating 0 without storing it. The range -vars..vars checks each stored literal against the declared variable count.

comment "c"
line "p cnf {vars:0..gecode.int_max} {clauses:0..}"
repeat clauses {
  list clause: -vars..vars until 0
}

c Three clauses of different lengths
p cnf 3 3
1 -2 0
2 3 -1 0
-3 0

iris read site/examples/tutorial/dimacs-clauses.iris site/examples/tutorial/dimacs-clauses.txt --dzn

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

Each list is one row of clause. Repetition adds another array level, so clause has depth 2 and its rows can have different lengths. A clause can span physical lines: zero ends it. Too few clauses or a missing zero fails while reading; extra data after the declared clauses also fails.

The Specification defines comment and stop prefixes, repeats, and lists.

Check an application policy

Suppose your application accepts only nonempty clauses. Add a check after the repeat. In count(clause), clause denotes one record’s list, so the condition runs once per clause. size(clause) would instead count the clauses, because a direct name in size always refers to the whole column.

comment "c"
line "p cnf {vars:0..gecode.int_max} {clauses:0..}"
repeat clauses {
  list clause: -vars..vars until 0
}
check count(clause) > 0 "this application requires nonempty clauses"

c Three clauses of different lengths
p cnf 3 3
1 -2 0
2 3 -1 0
-3 0

iris read site/examples/tutorial/dimacs-nonempty.iris site/examples/tutorial/dimacs-clauses.txt --dzn

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

An empty clause violates that policy:

p cnf 3 1
0

iris read site/examples/tutorial/dimacs-nonempty.iris site/examples/tutorial/dimacs-empty.txt --dzn

site/examples/tutorial/dimacs-empty.txt:2:1: check failed for record 1 of 'clause': this application requires nonempty clauses
     2 | 0
       | ^
spec: site/examples/tutorial/dimacs-nonempty.iris:6

This is E-CHECK-FAILED. The caret points at the failing record’s start. A failed read prints no partial data. See records and checks for the rules that make a check range over records.

Finish with the library reader

DIMACS itself permits an empty clause, which makes the formula unsatisfiable, so the library reader leaves out that policy. It adds a format name and stop "%" for the SATLIB trailer. The stop prefix makes the rest of the input unavailable to reading, including the trailer’s final zero.

This is the complete DIMACS CNF library reader:

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
}

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

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

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

The library page includes a failing literal-range example and source downloads. Continue with TSPLIB sections.