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)

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.