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