DIMACS (cpmpy.tools.dimacs)

This file implements helper functions for exporting CPMpy models from and to DIMACS format. DIMACS is a textual format to represent CNF problems. The header of the file should be formatted as p cnf <n_vars> <n_constraints>. If the number of variables and constraints are not given, it is inferred by the parser.

Each remaining line of the file is formatted as a list of integers. An integer represents a Boolean variable and a negative Boolean variable is represented using a ‘-’ sign.

cpmpy.tools.dimacs.read_dimacs(fname)[source]

Read a CPMpy model from a DIMACS formatted file strictly following the specification: https://web.archive.org/web/20190325181937/https://www.satcompetition.org/2009/format-benchmarks2009.html

Note

The p-line has to denote the correct number of variables and clauses

Parameters:

  • fname – the name of the DIMACS file

  • sep – optional, separator used in the DIMACS file, will try to infer if None

cpmpy.tools.dimacs.write_dimacs(model, fname=None)[source]

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

Todo

TODO: implement pseudoboolean constraints in to_cnf

Parameters:

  • model – a CPMpy model

  • fname – optional, file name to write the DIMACS output to