Tools (cpmpy.tools)

Set of independent tools that users might appreciate.

List of tools

explain	Collection of tools for explanation techniques.
dimacs	This file implements helper functions for exporting CPMpy models from and to DIMACS format.
maximal_propagate	Maximal propagation of CPMpy constraints using repeated solving.
tune_solver	This file implements parameter tuning for constraint solvers based on SMBO and using adaptive capping.
xcsp3	Set of utilities for working with XCSP3-formatted CP models.

class cpmpy.tools.GridSearchTuner(solvername, model, all_params=None, defaults=None)

Grid search parameter tuner that exhaustively tests all parameter combinations. Inherits from ParameterTuner but uses a simple grid search strategy

tune(time_limit=None, max_tries=None, fix_params={}, verbose=1)

Parameters:

• time_limit – Time budget to run tuner in seconds. Solver will be interrupted when time budget is exceeded

• max_tries – Maximum number of configurations to test

• fix_params – Non-default parameters to run solvers with.

• verbose – how much information to print (0=none)

exception cpmpy.tools.OCUSException

add_note()

Exception.add_note(note) – add a note to the exception

with_traceback()

Exception.with_traceback(tb) – set self.__traceback__ to tb and return self.

class cpmpy.tools.ParameterTuner(solvername, model, all_params=None, defaults=None)

Parameter tuner based on DeCaprio method [ref_to_decaprio]

tune(time_limit=None, max_tries=None, fix_params={}, verbose=1)

Parameters:

• time_limit – Time budget to run tuner in seconds. Solver will be interrupted when time budget is exceeded

• max_tries – Maximum number of configurations to test

• fix_params – Non-default parameters to run solvers with.

• verbose – how much information to print (0=none)

class cpmpy.tools.XCSP3Dataset(root: str = '.', year: int = 2023, track: str = None, transform=None, target_transform=None, download: bool = False)

XCSP3 Dataset in a PyTorch compatible format.

Parameters:

• root (str) – Root directory containing the XCSP3 instances (if ‘download’, instances will be downloaded to this location)

• year (int) – Competition year (2022, 2023 or 2024)

• track (str, optional) – Filter instances by track type (e.g., “COP”, “CSP”, “MiniCOP”)

• transform (callable, optional) – Optional transform to be applied on the instance data (the file path of each problem instance)

• target_transform (callable, optional) – Optional transform to be applied on the metadata (the metadata dictionary of each problem instance)

• download (bool) – If True, downloads the dataset from the internet and puts it in root directory

cpmpy.tools.decompress_lzma(path: PathLike) → StringIO

Decompresses a .lzma file.

Parameters:

path – Location of .lzma file

Returns:

Memory-mapped decompressed file

cpmpy.tools.make_assump_model(soft, hard=[], name=None)

Construct implied version of all soft constraints. Can be used to extract cores (see tools.mus()). Provide name for assumption variables with name param.

cpmpy.tools.marco(soft, hard=[], solver='ortools', map_solver='ortools', return_mus=True, return_mcs=True, do_solution_hint=True)

Enumerating minimal unsatisfiable subsets (MUSes) and minimal correction sets (MCSes) of unsatisfiable constraints.

Iteratively generates a subset of constraints (the seed) and checks whether it is SAT. When the seed is SAT, it is grown to an MSS to derive an MCS. This MCS is then added to the Map solver as a set to hit In case the seed is UNSAT, the seed is shrunk to a real MUS and returned. The Map-solver is instructed to not generated any superset of this MUS as next seeds

Based on:

Liffiton, Mark H., et al. “Fast, flexible MUS enumeration.” Constraints 21 (2016): 223-250.

Param:

solver: name of a solver, must support assumptions (e.g, “ortools”, “exact”, “z3” or “pysat”)

Param:

map_solver: the hitting-set (MAP) solver to use, ideally incremental such as “gurobi”, “pysat” or “exact”

Param:

return_mus: whether the algorithm should return MUSes

Param:

return_mcs: whether the algorithm should return MCSes

Param:

do_solution_hint: when true, will favor large seeds generated by the map-solver, and hence more likely to return MUSes. Especially useful when return_mus=True.

cpmpy.tools.mcs(soft, hard=[], solver='ortools')

Compute Minimal Correction Subset of unsatisfiable model. Removing these contraints will result in a satisfiable model. Computes a subset of constraints which minimizes the total number of constraints to be removed

Param:

soft: list of soft constraints that may be part of the minimal correction subset

Param:

hard: list of hard constraints, will be added to the model before solving

Param:

solver: the SAT-solver to use, must support optimization

cpmpy.tools.mcs_grow(soft, hard, solver='ortools')

Computes correction subset without requirement of optimization support Relies on assumptions so incremental solvers are adviced. Can be faster in some cases compared to optimal correction subset

Param:

soft: list of soft constraints that may be part of the minimal correction subset

Param:

hard: list of hard constraints, will be added to the model before solving

Param:

solver: the SAT-solver to use, must support assumptions

cpmpy.tools.mcs_grow_naive(soft, hard, solver='ortools')

Compute Minimal Correction Subset of unsatsifiable model. Computes a subset-minimal set of constraints by greedily removing contraints. Can be used when solver does not support assumptions No guarantees on optimality, but can be faster in some cases

Param:

soft: list of soft constraints that may be part of the minimal correction subset

Param:

hard: list of hard constraints, will be added to the model before solving

Param:

solver: the SAT-solver to use, ideally incremental such as “gurobi”, “exact”

cpmpy.tools.mcs_opt(soft, hard, weights=1, solver='ortools')

Compute Minimal Correction Subset of unsatisfiable model. Constraints can be weighted using the weights parameter. Computes a subset of constraints which minimizes the sum of all weights of constraints.

Param:

soft: list of soft constraints that may be part of the minimal correction subset

Param:

hard: list of hard constraints, will be added to the model before solving

Param:

weights: weight of each constraint, default is 1

Param:

solver: the SAT-solver to use, must support optimization

cpmpy.tools.mss(soft, hard=[], solver='ortools')

Compute Maximal Satisfiable Subset of unsatisfiable model. Computes a subset of constraints which maximises the total number of constraints

cpmpy.tools.mss_grow(soft, hard=[], solver='ortools')

Compute Maximal Satisfiable Subset of unsatsifiable model. Computes a subset-maximal set of constraints by greedily adding contraints. Relies on solving under assumptions, so using an incremental solver is adviced No guarantees on optimality, but can be faster in some cases

Param:

soft: list of soft constraints to find a maximal satisfiable subset of

Param:

hard: list of hard constraints, will be added to the model before solving

Param:

solver: name of a solver, must support assumptions (e.g, “ortools”, “exact”, “z3” or “pysat”)

Exploits the solution found to add more constraints at once, cfr: Mencía, Carlos, and Joao Marques-Silva. “Efficient relaxations of over-constrained CSPs.” 2014 IEEE 26th International Conference on Tools with Artificial Intelligence. IEEE, 2014.

cpmpy.tools.mss_grow_naive(soft, hard=[], solver='ortools')

Compute Maximal Satisfiable Subset of unsatsifiable model. Computes a subset-maximal set of constraints by greedily adding contraints. Can be used when solver does not support assumptions No guarantees on optimality, but can be faster in some cases

Param:

soft: list of soft constraints to find a maximal satisfiable subset of

Param:

hard: list of hard constraints, will be added to the model before solving

Param:

solver: the SAT-solver to use, ideally incremental such as “gurobi”, “exact”

cpmpy.tools.mss_opt(soft, hard=[], weights=1, solver='ortools')

Compute Maximal Satisfiable Subset of unsatisfiable model. Constraints can be weighted using the weights parameter. Computes a subset of constraints which maximizes the sum of all weights on constraints

cpmpy.tools.mus(soft, hard=[], solver='ortools')

A CP deletion-based MUS algorithm using assumption variables and unsat core extraction

For solvers that support s.solve(assumptions=…) and s.get_core()

Each constraint is an arbitrary CPMpy expression, so it can also be sublists of constraints (e.g. constraint groups), contain aribtrary nested expressions, global constraints, etc.

Will extract an unsat core and then shrink the core further by repeatedly ommitting one assumption variable.

Param:

soft: soft constraints, list of expressions

Param:

hard: hard constraints, optional, list of expressions

Param:

solver: name of a solver, must support assumptions (e.g, “ortools”, “exact”, “z3” or “pysat”)

cpmpy.tools.mus_naive(soft, hard=[], solver='ortools')

A naive pure CP deletion-based MUS algorithm

Will repeatedly solve the problem from scratch with one less constraint For anything but tiny sets of constraints, this will be terribly slow.

Best to only use for testing on solvers that do not support assumptions. For others, use mus()

Parameters:

• soft – soft constraints, list of expressions

• hard – hard constraints, optional, list of expressions

• solver – name of a solver, see SolverLookup.solvernames()

cpmpy.tools.mus_native(soft, hard=[], solver='exact')

Compute a MUS using a solver’s native MUS extractor.

Parameters:

• soft – soft constraints, list of expressions

• hard – hard constraints, optional, list of expressions

• solver – which solver to use (exact or gurobi)

cpmpy.tools.ocus(soft, hard=[], weights=None, meta_constraint=True, solver='ortools', hs_solver='ortools', do_solution_hint=True)

Find an optimal and constrained MUS according to a linear objective function. By not providing a weightvector, this function will return the smallest mus. Works by iteratively generating correction subsets and computing optimal hitting sets to those enumerated sets. For better performance of the algorithm, use an incemental solver to compute the hitting sets such as Gurobi.

Assumption-based implementation for solvers that support s.solve(assumptions=…) More naive version available as optimal_mus_naive to use with other solvers.

Param:

soft: list of soft constraints to find an optimal MUS of

Param:

hard: list of hard constraints, will be added to the model before solving

Param:

weights: list of weights for the soft constraints, will be used to compute the objective function

Param:

meta_constraint: a Boolean CPMpy expression that contains constraints in soft as sub-expressions. By not providing a meta_constraint, this function will return an optimal mus.

Param:

solver: name of a solver, must support assumptions (e.g, “ortools”, “exact”, “z3” or “pysat”)

Param:

hs_solver: the hitting-set solver to use, ideally incremental such as “gurobi”

Param:

do_solution_hint: when true, will favor large satisfiable subsets generated by the SAT-solver

CPMpy implementation loosely based on the “OCUS” algorithm from:

Gamba, Emilio, Bart Bogaerts, and Tias Guns. “Efficiently explaining CSPs with unsatisfiable subset optimization.” Journal of Artificial Intelligence Research 78 (2023): 709-746.

cpmpy.tools.ocus_naive(soft, hard=[], weights=None, meta_constraint=True, solver='ortools', hs_solver='ortools', do_solution_hint=True)

Naive implementation of ocus without assumption variables and incremental solving

cpmpy.tools.optimal_mus(soft, hard=[], weights=None, solver='ortools', hs_solver='ortools', do_solution_hint=True)

Find an optimal MUS according to a linear objective function.

cpmpy.tools.optimal_mus_naive(soft, hard=[], weights=None, solver='ortools', hs_solver='ortools')

Naive implementation of optimal_mus without assumption variables and incremental solving

cpmpy.tools.quickxplain(soft, hard=[], solver='ortools')

Find a preferred minimal unsatisfiable subset of constraints, based on the ordering of constraints.

A total order is imposed on the constraints using the ordering of soft. Constraints with lower index are preferred over ones with higher index

Assumption-based implementation for solvers that support s.solve(assumptions=…) and s.get_core() More naive version available as quickxplain_naive to use with other solvers.

Param:

soft: list of soft constraints to find a preferred minimal unsatisfiable subset of

Param:

hard: list of hard constraints, will be added to the model before solving

Param:

solver: name of a solver, must support assumptions (e.g, “ortools”, “exact”, “z3” or “pysat”)

CPMpy implementation of the QuickXplain algorithm by Junker:

Junker, Ulrich. “Preferred explanations and relaxations for over-constrained problems.” AAAI-2004. 2004. https://cdn.aaai.org/AAAI/2004/AAAI04-027.pdf

cpmpy.tools.quickxplain_naive(soft, hard=[], solver='ortools')

Find a preferred minimal unsatisfiable subset of constraints, based on the ordering of constraints.

A total order is imposed on the constraints using the ordering of soft. Constraints with lower index are preferred over ones with higher index

Naive implementation, re-solving the model from scratch. Can be slower depending on the number of global constraints used and solver support for reified constraints.

CPMpy implementation of the QuickXplain algorithm by Junker:

Junker, Ulrich. “Preferred explanations and relaxations for over-constrained problems.” AAAI-2004. 2004. https://cdn.aaai.org/AAAI/2004/AAAI04-027.pdf

cpmpy.tools.read_xcsp3(path: PathLike) → Model

Reads in an XCSP3 instance (.xml or .xml.lzma) and returns its matching CPMpy model.

Parameters:

path – location of the XCSP3 instance to read (expects a .xml or .xml.lzma file).

Returns:

The XCSP3 instance loaded as a CPMpy model.

cpmpy.tools.smus(soft, hard=[], solver='ortools', hs_solver='ortools')

Find a smallest MUS according, equivalent to optimal_mus with weights=None