Document linearize and have complete and separated mul decomposition#808
Document linearize and have complete and separated mul decomposition#808
Conversation
…only the int*int part is added, rest untouched
IgnaceBleukx
left a comment
IgnaceBleukx
left a comment
There was a problem hiding this comment.
For the doc, mostly minor stuff.
Code-wise: I think we are missing a CSE opportunity in the helper function; looks good otherwise.
| for translating to Pseudo-Boolean or CNF formats. | ||
|
|
||
| There are a number of components to getting a good linearisation: | ||
| - **Decomposing global constraints/functions** in a 'linear friendly' way. |
There was a problem hiding this comment.
Yes, but we currently don't do this yet in this PR? (Only for AllDiff)
cpmpy/transformations/linearize.py
Outdated
| There are a number of components to getting a good linearisation: | ||
| - **Decomposing global constraints/functions** in a 'linear friendly' way. | ||
| A common pattern is that constraints that enforce domain consistency on integer variables, | ||
| that they should be decomposed over a Boolean representation of the domain. This is the |
| - **Decomposing global constraints/functions** in a 'linear friendly' way. | ||
| A common pattern is that constraints that enforce domain consistency on integer variables, | ||
| that they should be decomposed over a Boolean representation of the domain. This is the | ||
| case for :class:`~cpmpy.expressions.globalconstraints.AllDifferent`, :class:`~cpmpy.expressions.globalfunctions.Element` |
There was a problem hiding this comment.
certainly also for Count
|
|
||
| - **Implications** e.g. `B -> sum(X) <= 4` should be linearised with the Big-M method. | ||
|
|
||
| - **Domain encodings** e.g. of `A=cp.intvar(0,4)` would create binary variables and constraints |
There was a problem hiding this comment.
This is a bit surprising to see in the docs here for me.
The other points are "constraint xxx is not linear, and should be linearized as follows...."; but here there is no "input" constraint?
cpmpy/transformations/linearize.py
Outdated
| - **Implications** e.g. `B -> sum(X) <= 4` should be linearised with the Big-M method. | ||
|
|
||
| - **Domain encodings** e.g. of `A=cp.intvar(0,4)` would create binary variables and constraints | ||
| like `B0 -> A=0`, `B1 -> A=1`, `B2 -> A=2`, etc and `sum(B0..4) = 1`. |
cpmpy/transformations/linearize.py
Outdated
| and is decomposed as such if not in `supported`. | ||
| Any other unsupported global constraint should be decomposed using | ||
| :func:`cpmpy.transformations.decompose_global.decompose_in_tree()`. | ||
| reified: Whether the constraint is fully reified. When True, nested implications |
There was a problem hiding this comment.
Not fully reified? We only support half-reified in linearize
cpmpy/transformations/linearize.py
Outdated
| - `const`: The difference between the original expression and the new expression, | ||
| i.e. a constant term that must be added to pos_expr to be an equivalent linear expression. | ||
| Replaces a var/sum/wsum expression containing :class:`~cpmpy.expressions.variables.NegBoolView` | ||
| with an equivalent expression using only :class:`~cpmpy.expressions.variables.BoolVar`, |
|
|
||
| It might add a constant term to the expression. If you want the constant separately, | ||
| use :func:`only_positive_bv_wsum_const`. | ||
|
|
There was a problem hiding this comment.
I'm wondering if this doc needs an example.
"E.g., the weighed sum 3*~x + 4*y is transformed to 3 + -3*x + 4*y. If you want the constant 3 to be separate, use only_positive_bv_wsum_const instead."
| lin_cnt = cp.Model(lin_cons).solveAll(display=assert_cons_is_true(cons)) | ||
| cons_cnt = cp.Model(cons).solveAll(display=assert_cons_is_true(cons)) | ||
| self.assertEqual(lin_cnt, cons_cnt) | ||
|
|
There was a problem hiding this comment.
Also test != and reified mult?
|
I enabled multiplication and related globals in test_constraints (which was quite satisfying to do); but it seems that reified multiplications are going wrong. |
|
Indeed, we should probably do both. Neither is to be taken lightly. I have some ideas for a refactor of linearize_constraint, but it might be a bumpy ride. |
|
First extracting mul as a global (and fixing it) would have been the easier route retrospectively... This rewrite should be a good basis for further improvements that will simplify it (e.g. doing globals before linearize, incl mul). Some things that surfaced:
The implimentation style of having a function with a 'condition' argument is quite clean... its what Henk used for pindakaas. We could consider it when rewriting flatten too. (perhaps we should rename it from 'implication_literal' to 'condition' indeed, or actually in pindakaas its 'conditions' as multiple are accepted, which makes sense...) I don't think we should add more to this PR though |
|
ah, also, 83000+ tests that took 7 hours+ on my machine, and I don't even have cplex/gurobi installed at the moment... (and 17 failed, pindakaas bug #810 ) |
|
That seems like a really really long time to run all tests... |
* solution_callback for Hexaly * Gracefully exit when not properly initialised * Populate objective on callback
some long lines should not be split, makes them unreadable
|
Time to transform the first case is <0.01 for both pindakaas and pysat. Time to solve is 2.5s for pysat and 122s for pindakaas |
|
merged #811 in, now only the 4 panics from #810 remain. The slowness of pindakaas also remains; pysat is notably faster, but still takes quite some time on some tests too. However, another thing I notice is memory use: when running test/test_constraints with only pysat, memory climbs up linearly, at 30% it was around 15Gb or so... so something is not cleaning up properly. Is it that the python garbage collector is not being run, so it is not cleaning up all our Booleans? or is it because maybe we are not closing the solver objects properly, so they keep their memory alive? or they keep our python objects alive? I have 0 experience with memory and Python, if somebody knows how to look into this, by all means... (running the tests with ortools stays at less then a Gb...) |
|
I've done some digging into the memory issues, and there are several parts to it:
with cp.SolverLookup(solver, model) as solver:
assert solver.solve()For this, we need to implement the context manager protocol for our solvers... https://book.pythontips.com/en/latest/context_managers.html
|
5 participants
So I wanted to better characterize linearize and add documentation.
Then I felt like 'mul' should be treated separately
Then I added multiplication of int*int as well.
But it is not finished... tests are choking on bool*bool especially, which I kept at bool level (half undone already) but then there are bools popping up at places where there is a (trivial) comparison.
Some other notes:
I wonder if we should make mul between two vars a global constraint after all... then we can take this out of linearize? e.g. there might be a CP solver that does not implement mul...
We switched away from doing 'decompose_comparison' on GlobalFunctions, in the hope of avoiding unnecessary auxliaries in nested expressions, but I now realize that this way we may include unneeded auxiliary variables for toplevel comparisons, e.g. now
b*v >= 5will be decomposed asdecomp-of(b*v = aux), aux >= 5...Maybe the previous point is not too bad, because aux>=5 is just a bound update, not a live constraint. But for
b*v = rwe would dob*v = aux, aux=r, which happens when flatten flattens some sum that containsb*v, which is another argument for making mul of two vars a global constraint: then we can decompose it before flatten?