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')[source]
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')[source]
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.optimal_mus(soft, hard=[], weights=None, solver='ortools', hs_solver='ortools', do_solution_hint=True)[source]
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.
- 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:
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.optimal_mus_naive(soft, hard=[], weights=None, solver='ortools', hs_solver='ortools')[source]
Naive implementation of optimal_mus without assumption variables and incremental solving
- cpmpy.tools.explain.mus.quickxplain(soft, hard=[], solver='ortools')[source]
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')[source]
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