Explanation tools (cpmpy.tools.explain)

Collection of tools for explanation techniques.

List of tools

mus	A CP deletion-based MUS algorithm using assumption variables and unsat core extraction
mss	Compute Maximal Satisfiable Subset of unsatisfiable model.
mcs	Compute Minimal Correction Subset of unsatisfiable model.
utils	Utilities for explanation techniques

MUS (cpmpy.tools.explain.mus)

Re-impementation of MUS-computation techniques in CPMPy

• Deletion-based MUS

• QuickXplain

• Optimal MUS

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

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, see SolverLookup.solvernames() “z3” and “gurobi” are incremental, “ortools” restarts the solver

Param:

time_limit: optional time limit in seconds

Returns:

list of constraints forming MUS, or empty list if time limit reached

cpmpy.tools.explain.mus.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()

Param:

soft: soft constraints, list of expressions

Param:

hard: hard constraints, optional, list of expressions

Param:

solver: name of a solver, see SolverLookup.solvernames()

cpmpy.tools.explain.mus.optimal_mus(soft, hard=[], weights=None, solver='ortools', hs_solver='ortools', time_limit=None)

Find an optimal 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.

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.

Param:

soft: soft constraints, list of expressions

Param:

hard: hard constraints, optional, list of expressions

Param:

weights: optional weights for optimization

Param:

solver: name of a solver

Param:

hs_solver: solver for hitting set problem

Param:

time_limit: optional time limit in seconds

Returns:

list of constraints forming optimal MUS, or empty list if time limit reached

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

Naive implementation of optimal_mus without assumption variables and incremental solving

cpmpy.tools.explain.mus.quickxplain(soft, hard=[], solver='ortools', time_limit=None)

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.

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

Param:

soft: soft constraints, list of expressions

Param:

hard: hard constraints, optional, list of expressions

Param:

solver: name of a solver

Param:

time_limit: optional time limit in seconds

Returns:

list of constraints, or empty list if time limit reached

cpmpy.tools.explain.mus.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.explain.mus.smus(soft, hard=[], solver='ortools', hs_solver='ortools')

MSS (cpmpy.tools.explain.mss)

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

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

Parameters:

time_limit – time limit in seconds (default: None)

Returns:

list of constraints, or empty list if time limit is reached

cpmpy.tools.explain.mss.mss_grow(soft, hard=[], solver='ortools', time_limit=None)

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

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.

Parameters:

time_limit – time limit in seconds (default: None)

Returns:

list of constraints, or empty list if time limit is reached

cpmpy.tools.explain.mss.mss_grow_naive(soft, hard=[], solver='ortools', time_limit=None)

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

Parameters:

time_limit – time limit in seconds (default: None)

Returns:

list of constraints, or empty list if time limit is reached

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

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

Parameters:

time_limit – time limit in seconds (default: None)

Returns:

list of constraints, or empty list if time limit is reached

MCS (cpmpy.tools.explain.mcs)

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

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

Parameters:

time_limit – time limit in seconds (default: None)

Returns:

list of constraints, or empty list if time limit is reached

cpmpy.tools.explain.mcs.mcs_grow(soft, hard, solver='ortools', time_limit=None)

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

Parameters:

time_limit – time limit in seconds (default: None)

Returns:

list of constraints, or empty list if time limit is reached

cpmpy.tools.explain.mcs.mcs_grow_naive(soft, hard, solver='ortools', time_limit=None)

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

Parameters:

time_limit – time limit in seconds (default: None)

Returns:

list of constraints, or empty list if time limit is reached

cpmpy.tools.explain.mcs.mcs_opt(soft, hard, weights=1, solver='ortools', time_limit=None)

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.

Parameters:

time_limit – time limit in seconds (default: None)

Returns:

list of constraints, or empty list if time limit is reached

Utils (cpmpy.tools.explain.utils)

Utilities for explanation techniques

List of functions

make_assump_model

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.explain.utils.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