From 6fbad27b2fe359387aa4d6462975151e55fe32eb Mon Sep 17 00:00:00 2001 From: IgnaceBleukx Date: Fri, 23 Aug 2024 16:08:59 +0200 Subject: [PATCH] corr subset enumeration in naive version --- cpmpy/tools/explain/mus.py | 25 +++++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py index 54d7fa62b..0d5a9942f 100644 --- a/cpmpy/tools/explain/mus.py +++ b/cpmpy/tools/explain/mus.py @@ -248,7 +248,7 @@ def do_recursion(soft, hard, delta): core = do_recursion(soft, hard, []) return core -def optimal_mus_naive(soft, hard=[], weights=1, solver="ortools", hs_solver="ortools", grow=mss_grow_naive): +def optimal_mus_naive(soft, hard=[], weights=1, solver="ortools", hs_solver="ortools"): """ Naive implementation of `optimal_mus` without assumption variables and incremental solving """ @@ -266,13 +266,22 @@ def optimal_mus_naive(soft, hard=[], weights=1, solver="ortools", hs_solver="ort hitting_set = [c for bv, c in zip(bvs, soft) if bv.value()] if cp.Model(hard + hitting_set).solve(solver=solver) is False: break - # SAT, how to do grow without assumptions? - # for now, using naive grow methods from tools/explain/mcs - mss = grow(soft=[c for bv, c in zip(bvs, soft) if not bv.value()], - hard=hitting_set + hard, - solver=solver) - mcs = [bv for bv,c in zip(bvs, soft) if c not in frozenset(hitting_set + mss)] - hs_solver += cp.sum(mcs) >= 1 + + # else, the hitting set is SAT, now try to extend it without extra solve calls. + # Check which other assumptions/constraints are satisfied using its value() function + # sidenote: some vars may not be know to model and are None! + # complement of grown subset is a correction subset + false_constraints = [s for s in soft if s.value() is False or s.value() is None] + corr_subset = [bv for bv,c in zip(bvs, soft) if c in frozenset(false_constraints)] + hs_solver += cp.sum(corr_subset) >= 1 + + # find more corr subsets, disjoint to this one + sat_subset = hitting_set + false_constraints + while cp.Model(hard + sat_subset).solve(solver=solver) is True: + false_constraints = [s for s in soft if s.value() is False or s.value() is None] + corr_subset = [bv for bv, c in zip(bvs, soft) if c in frozenset(false_constraints)] + hs_solver += cp.sum(corr_subset) >= 1 + sat_subset += false_constraints return hitting_set