gurobi improved MUS

[OrestisLomis]

This implement the suggested improvement of #979

[IgnaceBleukx]

I'm still getting to grips with the code, so also some comments on the original implementation.

If I understand correctly, the tool works as follows:
You want to find an MUS for a set of soft CPMpy constraints; there can be hard CPMpy constraints as well.
A single CPMpy constraint may require multiple Gurobi-constraints. So, we introduce a Boolean variable a to represent the group, and add the hard constraints

a -> a_1 /\ a_2 /\ ... a_n
a_1 -> grb_transformed_constraint_1
a_2 -> grb_transformed_constraint_2
...

the soft constraint is then a = 1 ?

There seems to be too much bookkeeping going on. What is the difference between grb_force_cons and grb_hard_cons?

[IgnaceBleukx]

This very much feels like you're doing things backwards.
Wouldn't it make more sense to first do all of this soft-constraints stuff, and just add the mapping you get here to the original hard constraint list?

[hbierlee]

I think that would also work

[OrestisLomis]

I'm not sure I get what you mean. The hard constraint machinery comes after this. Only the transformation of the hard constraint to gurobi comes before which is fine to be moved but not sure if that's what you really meant.

[hbierlee]

Mostly correct, in my mind it is simpler: for MIP solvers (or at least for gurobi) the main interface difference with the assumption-based solvers is that instead of only Boolean literals we can directly make a MUS out of supported "soft" constraints. It's a little more general in that sense. The transformation process is identical though, we just make an assumption model (reifya -> C for each model constraint C, which is then transformes in whatever way. We don't have to intro a_1, ... This is just like make_assump_model right?).

There are two optimizations we then added, 1) since we can post a supported soft constraint directly, we don't introduce a if C is already supported (e.g. a linear), and 2) as per Riley's comment a can be a constant because gurobi allows the bound of a to be part of the MUS.

Maybe some things can be reshuffled, however, note that we should only do model.update once as it's expensive. I believe this is what causes some of the extra bookkeeping.

I think the grb_hard_cons was just renamed, but the original instantiation was left in.

[hbierlee]

The new optimization looks good to me. Ignace's comments can further simplify the implementation which would be good

[hbierlee]

I think that would also work

[OrestisLomis]

Just to add to what @hbierlee already said. We indeed do not "need" the assumption variables for a MIP model. A MIP solver can just compute an IIS for the constraints as they are. The need for the assumption variables (and here it makes more sense to call them indicator variables) is to group gurobi constraints as CPMpy level constraints. So in practice a soft constraint such as p >= 1 & p <= 2 gets transformed into a list of gurobi constraints and each of them gets reified. So we get a_1 -> p >= 1 and a_2 -> p <= 2. Crucially these constraints should be hard constraints because they always hold (will clarify with an example below, this breaks for other MIP solvers which don't expose hard constraints). Then you can add a soft constraint a_1 >= 1. As @hbierlee said there are two improvements. The first one is that we don't actually need to reify constraints when the group is just a singleton, this was already implemented in the original PR #880. The second one is that actually we do not need a_1 >= 1 as a soft constraint either. The model should be simpler if we just set the lowerbound of a_1 to 1 and then that lowerbound can be found as part of the MUS/IIS, which is something MIP solvers can do.

There is indeed quite a bit of bookkeeping going on with different type of gurobi constraints which all have different API calls. The grb_hard_cons and grb_force_cons were essentially the same thing. Indeed no reason to have had them split in two so I simplified the code.

Now why do the reified constraints need to be hard constraints? Essentially just using the same indicator variable does not force the grouping by itself. Consider the problem where we have p >= 1 & p < 1 and p < 1 as the constraints in our model, which for gurobi becomes a_1 -> p >= 1, a_1 -> p < 1 and p < 0. Clearly the actual MUS should just be the constraint p >= 1 & p < 1 . But if all the constraints a_1 -> p >= 1, a_1 -> p < 1 and p < 1 are soft what can happen is that Gurobi's IIS can return a_1 -> p >= 1, p < 1 and the lowerbound of a_1 as part of the IIS, bypassing the grouping.

[OrestisLomis]

Also I've gone over the requested changes and also fixed a small bug that was left behind. Feel free to have another look.

[hbierlee]

So in practice a soft constraint such as p >= 1 & p <= 2 gets transformed into a list of gurobi constraints and each of them gets reified. So we get a_1 -> p >= 1 and a_2 -> p <= 2

Assuming this example is really a single soft constraint (a little ambiguous due to the &), the soft constraint p >= 1 & p <= 2 is added as hard constraint a-> (p >= 1 & p <= 2) which is then hopefully transformed to (a-> (p >= 1)) & (a-> (p <= 2)). If you mean these are two soft constraints you'd get two a's. However my main point is that this is all no different from assumption-based solvers when you do make_assump_model (and the reified constraints therein also become 'hard constraints ' ; it's just the assumptions which need not all hold)

[OrestisLomis]

Yes, you are correct. Though it doesn't really break the example as the transformed constraints will typically still be considered as separate soft constraints internally. So unless a solver supports a conjunctive constraints they should still be hard constraints. But this discussion is more relevant for other solvers/PRs anyway so no need to go to deep into the details.

Processed docchange