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.

class cpmpy.tools.dimacs.DimacsReader(var_name=None)[source]
initialize(n_vars, n_clauses)[source]
n_clauses()[source]
n_vars()[source]
read(fname)[source]
read_clause(tokens)[source]
read_tokens(tokens)[source]
to_model()[source]
class cpmpy.tools.dimacs.GDimacsReader(var_name=None, assumption_name=None)[source]
initialize(n_vars, n_clauses)
n_clauses()
n_groups()[source]
n_vars()
read(fname)
read_clause(tokens)
read_tokens(tokens)[source]
to_model()[source]
cpmpy.tools.dimacs.read_dimacs(fname, var_name=None)[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

  • name – prefix for variable names, optional

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

cpmpy.tools.dimacs.read_gdimacs(fname, var_name=None, assumption_name=None)[source]

Read a CPMpy model from a GDIMACS (Grouped DIMACS) formatted file (strictly following https://satisfiability.org/competition/2011/rules.pdf, except that groups are allowed to have disjoint sets of clauses)

Parameters:

fname – path to the GDIMACS file

Returns:

tuple (model, soft, hard, assumptions) where: - model: CPMpy Model with all constraints - soft: list of soft constraint groups - hard: list of hard constraints (from group 0) - assumptions: assumption variables for each soft constraint group

cpmpy.tools.dimacs.write_dimacs(model, fname=None, encoding='auto', canonical=False)[source]

Writes CPMpy model to DIMACS format. :param model: a CPMpy model :param fname: optional, file name to write the DIMACS output to :param name: prefix for variable names, optional :param encoding: the encoding used for int2bool, choose from (“auto”, “direct”, “order”, or “binary”)

cpmpy.tools.dimacs.write_dimacs_(constraints, groups=None, fname=None, canonical=False)[source]

Helper function: constraints are assumped to be CNF (i.e. a list of conjunctions of hard clauses), groups are a list of tuples of (assumption variable, soft clauses)

cpmpy.tools.dimacs.write_gdimacs(soft, hard=None, fname=None, encoding='auto', disjoint=True, canonical=False)[source]

Writes CPMpy constraints to GDIMACS (Grouped DIMACS) format for MUS extraction.

Uses the “to_gcnf” transformation to convert soft and hard constraints into grouped CNF. The GDIMACS format follows the specification at: https://satisfiability.org/competition/2011/rules.pdf

Each soft constraint is assigned to a separate group. Hard constraints are placed in group {0}. This format is used by MUS (Minimal Unsatisfiable Subset) solvers to find minimal explanations for infeasibility in SAT instances.

Parameters:

  • soft – list of CPMpy constraints that can be violated (soft constraints)

  • hard – list of CPMpy constraints that must be satisfied (hard constraints), optional

  • fname – file path to write the GDIMACS output

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

  • disjoint – if True, ensures groups are disjoint by introducing auxiliary variables. Required by some MUS solvers (e.g., MUSSER2) for correctness. We have seen an overhead of ~25% when enabled.

  • canonical – if True, outputs variables in sorted order and literals within clauses sorted by variable (positive before negative for same variable)

Returns:

GDIMACS formatted string