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.