Pysat wsum

[sourdough-bread]

Weighted sum

• Added case where a boolean variable-based expression is of the form a * x - b * y where a and b: sum should transform to weighted sum.
  • Moved implementation into the flattening to stay true to the user's model.
• Added support with PySAT:
  • weighted sum interpreted as pseudo boolean constraint
  • sum encoded as a cardinality constraint

[tias]

feedback

[sourdough-bread]

New version can be reviewed.

[tias]

I wanted to include it in the release I am about to make, so I made some quick cleanups (space changes, solver_vars instead of list of solver_var, a few one-line docs).

But then I noticed:

1. there are two test failing, including in test_flatten, which need to be fixed
2. current master is not merge into it yet, so there might be more (or less) tests failing after that.

If you could fix that, then it can be merged for the next release, it looks ready otherwise (but so there might be some subtle cases still in the new flatten code)

[tias]

see open comments

also, we merged the transform() refactor so pysat interface changed a bit, which needs conflict/merging.

but importantly, I want the changes to 'flatten_model.py' as a separate pull request. These are optimisations that improve the flattening, but imho can be treated independently of pysat. I think it also means that the pysat_wsum tests should become generic flatten tests?

If yes, we can merge this branch before checking the optimisations in more detail. (the preferred option)

If no, we should first get the optimisations on that separate branch right, and then merge this

[tias]

@IgnaceBleukx you probably best do the resolve of test_constraints yourself

[tias]

@IgnaceBleukx the tests indeed test bvar*bvar, which pysat does not support (and throwns an exception on now); so I had to remove 'mul' from the tests to not trigger this test.

However, it also tests that for z3, which does not support it either.
So can you instead remove the bv*bv test from the automatic constraint generation and not test that? I don't understand where it is generated or how to stop it being generated...

Note that this code is rebased on the unmerged #316, you can wait with a further code review till that one is merged.

[tias]

OK, so first, we need to check for 'out of bounds' bounds in both card/pb, as the encoding libraries simply refuse to encode a trivially true/false constraint.

I might also accidentally have removed the bv < 1 support case (or it used to be in simplify_bool and now it aint no more?)...

Then, all pb/cardinality expressions are expected to be of the following normalized form:
wsum <= const (potentially reified)

From a CPMpy design that is fine: a solver interface only implements the constraint formulations it 'natively' supports.

So then the question is, do we have a transformation that rewrites e.g. wsum <= var or wsum >= wsum into such 'normalized' linear constraints?
I would expect 'linearize'? @IgnaceBleukx ?

But this interface is more sensitive to the creation of auxliary integer variables (e.g. for bv[0] > bv[1]+bv[2]). So how far do we want to go with this?

[IgnaceBleukx]

Yes, we absolutely have such normalization!
The standalone one is canonical_comparison which also gets called from linearize.
I proposed to run canonical_comparison before flatten in #432 as it will result in many "free" optimizations in terms of nb of aux vars when flattening. Pretty sure we need to fix that part of the transformation before getting serious with this pull request. Atm, flattening a sum can result in creating an aux intvar, causing PySAT interface to crash. E.g., a > b + c becomes [a > IV0, b + c == IV0]...

I think it would be best if we indeed put PySAT after linearize, but we have to adapt the transformation so it leaves simple clauses and ands as we currently do not check for that.
Putting it after linearize will significantly reduce the cases we have to check for in the encodings, as we only have <=, >= and == remaining. The not-equals gets transformed to an implication/Big-M formulation.
(The latter one if we have smt like a -> x + y + z != 2)

I would simply add the case of bv * bv to linearize too as it can be encoded as an and

The only potential downside of putting PySAT after linearize is the potential overhead of the transformation... Linearize is quite a beast to get through for each expression...

Regarding the bounds checking for encoding, I am ok for doing it ourselves now, but I think we can also just open an issue with PySAT themselves to fix this.