DIMACS (cpmpy.tools.io.dimacs)

Helper functions for loading CPMpy models from and writing to DIMACS format.

DIMACS is a textual format to represent CNF problems. More can be read about it here:

• https://satisfiability.org/competition/2009/format-benchmarks2009.html

• https://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html

Format:

The header of the file can optionally include a p-line; p cnf <n_vars> <n_constraints> [<top_weight>]. If the number of variables and constraints are not given, it is inferred by the parser.

Note

It is preferred by the SAT competition to no longer include the p-line.

Each remaining line of the file is formatted as a list of integers with a trailing 0; literals belonging to the same clause. Each integer references a Boolean variable by its index (1-based) and a negative Boolean variable is represented using a ‘-’ sign.

E.g. the clause (a or b or c) is represented as 1 2 3 0.

In the case of weighted instances, soft clauses are represented as <weight> <literal> 0.

E.g. the soft clause (a or b or c) with weight 3 is represented as 3 1 2 3 0.

Comments are lines starting with a c character.

Full example:

c This is a comment
p cnf 3 3
1 2 3 0
c This is another comment
-2 -3 0
-1 0

List of functions

load_dimacs	Load a CPMpy model from a DIMACS formatted file strictly following the specification.
write_dimacs	Writes a CPMpy model to DIMACS format.

cpmpy.tools.io.dimacs.load_dimacs(dimacs: str | PathLike | TextIO, open: Callable = <built-in function open>, type: str | None = None)

Load a CPMpy model from a DIMACS formatted file strictly following the specification.

Note

The (optional) p-line has to denote the correct number of variables and clauses.

Parameters:

• dimacs (str or os.PathLike or TextIO) –

  • A file path to a DIMACS/WCNF file, or

  • A string containing DIMACS/WCNF content directly, or

  • A TextIO object already open for reading

• open (Callable) – callable to open the file for reading (default: builtin open). Use for decompression, e.g. lambda p: lzma.open(p, 'rt') for .cnf.xz.

• type (str, optional) – type of the file to load. If None, it is inferred from the file content. Supported types: “cnf”, “wcnf”.

Returns:

The CPMpy model of the DIMACS instance.

Return type:

cp.Model

Raises:

ValueError – If the optional type argument is not supported.

cpmpy.tools.io.dimacs.write_dimacs(model: Model, path: str | PathLike | None = None, encoding: str = 'auto', p_header: bool = False, header: str | None = None, open: Callable = functools.partial(<built-in function open>, mode='w'), annotate_bool: BooleanEncodingAnnotator | None = None) → str

Writes a CPMpy model to DIMACS format. Uses the “to_cnf” transformation from CPMpy.

Warning

If the model has an objective, WCNF is emitted. DIMACS/WCNF has no field for constant objective offsets; when objective transformation introduces one, it is ignored and a warning is raised. The written model still preserves the optimisation, but its objective value may differ by that constant.

Parameters:

• model (cp.Model) – a CPMpy model

• path (str or os.PathLike, optional) – file path to write the DIMACS output to. If None, the DIMACS string is returned.

• encoding (str) – the encoding used for int2bool, choose from (“auto”, “direct”, “order”, or “binary”) (default: “auto”)

• p_header (bool) – whether to include the p ... problem header line. Replaces the h prefix for WCNF with a top weight. (default: False)

• header (str, optional) – Optional header text to prepend as DIMACS comments. If None, a default CPMpy header is created only when writing to path. Pass an empty string to skip adding a header.

• open (Callable) – callable to open the file for writing (default: builtin open). Called as open(path). This mirrors the open= argument in loaders and allows custom compression or I/O (e.g. lambda p: lzma.open(p, 'wt')).

• annotate_bool (BooleanEncodingAnnotator, optional) – encoding annotator, annotates boolean variables with names describing how they contribute to an encoded integer variable. When provided, each DIMACS literal ID is mapped back to that name via a c <id> <name> comment line. When None, no comments are written.