Module dimacs 

DIMACS CNF parsing and printing — the SAT-competition interchange format, and the front door for running arbitrary instances through the solver.

The format is a header p cnf <num_vars> <num_clauses>, optional c … comment lines, then a stream of signed integers: each clause is terminated by 0, a clause may span several lines, and several clauses may share a line. We parse fail-closed — a missing or garbled header, a literal naming a variable beyond num_vars, a non-integer token, or a final clause with no terminating 0 is a typed error, never a quietly mangled formula.

The header clause COUNT is deliberately advisory: real instances miscount and competition solvers tolerate it, so we keep the clauses we actually read rather than rejecting on a count mismatch. The variable COUNT, by contrast, bounds the literals and is enforced.

Structs

DimacsCnf

A parsed CNF formula: num_vars variables and clauses over packed Lits.

Enums

DimacsError

Why a DIMACS input was rejected. Better a typed error than a silently wrong formula.

Functions

parse

Parse a DIMACS CNF string. See the module docs for the fail-closed contract.

print

Render a DimacsCnf back to DIMACS text. parse(print(x)) == x.