Linear decomposition for Regular using MDD#981
Conversation
…rting MDD natively)
tias
left a comment
There was a problem hiding this comment.
some changes on the decompose part required.
Also, best weight till the decompose itself is in master (Ignace is working on it) and then that we iterated on it here, before putting it in the xcsp3 branch
| break | ||
| newlist: List[Expression] = [] | ||
| todolist: List[Expression] = [] # these still need to be decomposed | ||
| positive_decomps = get_positive_decompositions() |
There was a problem hiding this comment.
this is unexpected (to call an outside function) and different from 'decompose_custom'.
Should we instead not have an extra argument 'decompose_positive' which is a dict like decompose custom?
There was a problem hiding this comment.
It's possible, but the reason I did it like this is because the existence of a positive decomposition is solver independent, so it will be the same for any call to decompose_in_tree(), unlike decompose custom
There was a problem hiding this comment.
I understand. but its positive decompositions are the same 'for now'. if we are extensible on custom for plain decompositions, might as well be extensible for positive decomps too.
With ignace we finalized the signature for decomposition for cpmpy at large, including nested and half-reif; Ideally we can do that straight
(not we have to do this not in the PR, but the parent PRs)
| for expr in lst_of_expr: | ||
| if isinstance(expr, GlobalConstraint) and expr.name not in supported: | ||
| # toplevel/positive global constraint, decompose | ||
| positive_decomp = positive_decomps.get(expr.name) |
There was a problem hiding this comment.
there are 2 different patterns in this code: for positive_decomp it is fetched upfront, for decompose_custom it checks in the if whether it is 'in' and only then calls/applies it...
these two are so similar that they should be treated similar imho
|
|
||
| newlist.extend(expr.args[0].implies(e) for e in exprs) | ||
| newlist.extend(toplevel_exprs) | ||
| already_decomposed = True |
There was a problem hiding this comment.
the already_decomposed is a bit weird...
I'm also not sure the flow is correct; as in, 2 ifs above after decompose you add them to todolist because their args can have globals too; the code below does it recursive.
So, don't you have to follow the pattern of above? and add them to todolist?
note that you can just 'continue' if you have fully handled the case; this avoids the need for an already decomposed flag, and makes sure nothing extra will be posted accidentally either
|
seems I reviewed it against the wrong branch... is it still OK like this? |
Building on #924, #949 and #980, I implemented a linear decomposition of the Regular global constraint using the MDD global. To convert the DFA to an MDD, I used Algorithm 1 in:
"A Regular Language Membership Constraint for Finite Sequences of Variables", Gilles Pesant, 2004
to convert a DFA to a layered graph (equivalent to an MDD). The advantage here is that transitions that cannot lead to an accepting state will not be part of the resulting layered graph.
By doing this, we can also take advantage of the positive decomposition for MDDs when the Regular global is top-level or positively reified. (Same goes for Table in #945)