Decompose linear

[IgnaceBleukx]

Starting from #835, allow for decompose_custom which is populated with a new transformation "decompose_linear" containing a few specialized decompositions.

Only draft for now, and some open questions:

• For non-Boolean solvers, do we also add the constraint encoding == intvar or do we eliminate the intvar all together?
• Where should we put the decompose code? We should be able to access ivarmap, so for me it made the most sense to put them into the linearize file. Alternatively, we can detect bv == (iv == val) style constraints after flattening, and we don't do the encoding explicitely during decompose.

[tias]

decomp custom should be an optional argument.

The decomp_linear function is nice; the fact that you add a decomp_custom argument, do you prefer that over https://cpmpy.readthedocs.io/en/latest/api/expressions/globalconstraints.html#alternative-decompositions that overwrites the decomp function?

I actually think the proposed approach is nice and it being explicit is a plus.

Should we have separate overrides for reified? E.g. circuit toplevel is simpler... or would we achieve the equivalent when we do context aware flattening on the full formulation?

[IgnaceBleukx]

I think the main advantage of using the decomp_custom argument is that we do not have to loop over the entire tree in decompose_linear as well : ) Otherwise, we would need to find the globals in the expression tree and overwrite their decompose function there...

I would have to think about the reif vs non-reif ones. As long as our decompositions also model the negation of the global, there is no real point in making the distinction; not sure if it would get that much easier if we don't model the negation in the Circuit decomp? Indeed, we should get a lot of things for free when we add context aware flattening

[tias]

Thought some more about it; your proposal is the better way forward.

And we don't need answers to the half-reif question to move forward with this improvement to our current linearisation.

[IgnaceBleukx]

Merged the current master in this branch and added some tests.

One open question and one issue remains:

• For the non-Boolean solvers, we need to make a constraint encoding.encode_term() == iv. But where should we make this? In the decomposition would make sense, as we know if and when we make a new encoding, but there we don't know if the solver in question is Boolean or not. Alternative is in the solver interface, but it might get messy trying to figure out which encoding variables are new?
• There is something weird going on with the element decomposition. It only triggers as part of the decomposition of Inverse; I still need to have a closer look at that. It probably has to do with partial functions; ideally we would merge safening into the decompose transformation...

[IgnaceBleukx]

Ok managed to fix the element issue, small oversight in the decomposition on my side ; )

What other globals would we want to make a linear friendly decomposition for?
Table/NegTable, InDomain, Count and GCC come to mind. (Maybe Among?)

Also the the ExceptN variants probably?

[IgnaceBleukx]

Finally got the tests to work and added some extra globals.
I realized that for GCC and Among, we basically get the linear decomp for free as we decompose them to Count constraints anyway.

Should be ready for review now.

[tias]

Great to see this happening.

Why do you use encode/intvarmap instead of the more straightforward (var == val) expressions, which CSE has to pick up later then?
The decompose_linear is called before flatten right, so the decompositions could look like any other decomposition?

(this would push the responsability of handling the proper encoding of the var and the 'keep_integer' to later in the stack)

[tias]

chatted with an agent about my rough ideas; decided a new transformation instead of doing two-stage could work well.

Small test example:

import cpmpy as cp
x = cp.intvar(1, 3, shape=3, name=("a", "b", "c"))
cons = cp.AllDifferent(x)
cp.SolverLookup.get("exact").transform(cons)

gives
[sum([BV0, BV1, BV2]) <= 1, sum([BV3, BV4, BV5]) <= 1, sum([BV6, BV7, BV8]) <= 1, sum([BV0, BV3, BV6]) == 1, sum([1, 2, 3, -1] * [BV0, BV3, BV6, a]) == 0, sum([BV1, BV4, BV7]) == 1, sum([1, 2, 3, -1] * [BV1, BV4, BV7, b]) == 0, sum([BV2, BV5, BV8]) == 1, sum([1, 2, 3, -1] * [BV2, BV5, BV8, c]) == 0]

We could give the new transformation your original keep_integer argument so a solver can indicate the last two are not needed?

[tias]

I think the keep_integer is dangerous... it relies on removing the integer later.

Perhaps, we could give the new transformation an optional ivarmap argument, then it can put the ivar in the ivarmap if it did its thing (and not post the = intvar); then perhaps that is a safer approach where the solvers can later check the ivarmap?