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.
marco	Enumerating minimal unsatisfiable subsets (MUSes) and minimal correction sets (MCSes) of unsatisfiable constraints.
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')

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.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()

Parameters:

• soft – soft constraints, list of expressions

• hard – hard constraints, optional, list of expressions

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

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

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

MSS (cpmpy.tools.explain.mss)

cpmpy.tools.explain.mss.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.explain.mss.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.explain.mss.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.explain.mss.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

MCS (cpmpy.tools.explain.mcs)

cpmpy.tools.explain.mcs.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.explain.mcs.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.explain.mcs.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.explain.mcs.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

MARCO (cpmpy.tools.explain.marco)

Re-implementation of MUS-enumeration using MARCO.

cpmpy.tools.explain.marco.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.

Utils (cpmpy.tools.explain.utils)

Utilities for explanation techniques

List of functions

make_assump_model

Construct implied version of all soft constraints.

exception cpmpy.tools.explain.utils.OCUSException

add_note()

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

args

with_traceback()

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

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.

cpmpy.tools.explain.utils.replace_cons_with_assump(cpm_cons, assump_map)

Replace soft constraints with assumption variables in a Boolean CPMpy expression.