MSS (cpmpy.tools.explain.mss)
- cpmpy.tools.explain.mss.mss(soft, hard=[], solver='ortools')[source]
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')[source]
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')[source]
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”