Conversation
hbierlee
left a comment
hbierlee
left a comment
There was a problem hiding this comment.
I feel it can be simplified?
cpmpy/solvers/exact.py
Outdated
| assump_vals = [1 for v in assumptions] | ||
| assump_vars = [self.solver_var(v) for v in assumptions] | ||
| self.assumption_dict = {xct_var: (xct_val,cpm_assump) for (xct_var, xct_val, cpm_assump) in zip(assump_vars,assump_vals,assumptions)} | ||
| self.xct_solver.setAssumptions(list(zip(assump_vars,assump_vals))) |
There was a problem hiding this comment.
the number of dicts/zips/lists all feels overly complicated to me
Why is it not just 671 create a dict of solver_var(v): v, then setAssumptions with a comprehension of .keys on that dict to get solver_var(v), 1 tuples?
There was a problem hiding this comment.
Perhaps this could also avoid creating the boolvar just to use as key in 680.
There was a problem hiding this comment.
The boolvar is necessary because exact actually returns a list of strings with the names of the assump vars, so to get back the actual assump var I need to recreate it with the same name. Could perhaps do the opposite and make the dict already have the strings, but I don't think this is a bottleneck and this makes a little more sense personally.
There was a problem hiding this comment.
I would do it the same as in get_core, it seems getLastCore also returns the strings of the variables, and we use those to map from exact variables to cpmpy variables. I don't think it's a performance bottleneck, but it doesn't feel like it's the most direct way either.
|
I would also think there are no specific tests needed, if this implementation is run in the regular MUS tests (although they are not very thorough imo) |
|
On the question as to how to make sure the solver has no constraints (which would be hard constraints) in it when calling |
|
|
||
| s = SolverLookup.get("exact", m) | ||
|
|
||
| assert not s.solve(assumptions=assumptions), "MUS: model must be UNSAT" |
There was a problem hiding this comment.
did you check whether exact can detect this itself? maybe put a comment if exact cannot detect it
| raise NotSupportedError("Solver does not support unsat core extraction") | ||
|
|
||
| @staticmethod | ||
| def _native_mus(self, soft, hard=[]): |
| from cpmpy.tools.explain.utils import make_assump_model # avoid circular import | ||
| m, soft, assumptions = make_assump_model(soft, hard) | ||
|
|
||
| s = SolverLookup.get("exact", m) |
There was a problem hiding this comment.
perhaps it could be a classmethod, in which case the first argument becomes cls and you could replace this with cls(m). This shows the intention of the native_mus being executed with the current class.
|
|
||
| :param soft: soft constraints, list of expressions | ||
| :param hard: hard constraints, optional, list of expressions | ||
| :param solver: which solver to use (only `gurobi` and `exact` supported) |
There was a problem hiding this comment.
make this an assert, no idea what error we will get if I call it with the wrong name
There was a problem hiding this comment.
related, there's a SolverLookup method out there that will get you the class (it may also return a nice error which would avoid the assert).
2 participants
Add native mus computation for Exact, this also serves as a template to add mus computation for gurobi and adapt #880
Do still need to write some tests