Infeasable assumptions are not reported

[magneticflux-]

What version of OR-Tools and what language are you using?
Version: main, 9.9.3956
Language: Java

Which solver are you using (e.g. CP-SAT, Routing Solver, GLOP, BOP, Gurobi)
CP-SAT

What operating system (Linux, Windows, ...) and version?
Linux, x86_64

What did you do?
I use "enforcement" variables to track down invalid constraints during development. When solving normally, they are simply model.trueLiteral(), but if that is proved infeasible, the model is recreated with real variables that are added as assumptions and stopAfterFirstSolution set. Checking sufficientAssumptionsForInfeasibility after the second solve shows me which constraint groups caused the problem.

What did you expect to see
A model that is infeasible to start with will never be feasible if the enforcement literals are replaced with assumed variables.

What did you see instead?

The second model reports OPTIMAL, but the solution is invalid. These are the (zipped, binary) protobufs of the two models:

Infeasible: hard-assumptions.bin.gz
Optimal: soft-assumptions.bin.gz

[lperron]

So,

maybe this is a bug, not sure. The conditions to use assumptions are tricky. For instance, parallelism is not supported, objective are not supported.

I do not understand.

A model that is infeasible to start with will never be feasible if the enforcement literals are replaced with assumed variables.

what happens if:

• you solve normally (enforcement literals are true literals) ?
• you solve with variable enforcement literals (new_bool_var) ?
• you solve with variable enforcement literals and an objective to maximize the number of true enforcement literals ?
• you solve with variable enforcement literals and use them as assumptions ?

[lperron]

We do check all solutions returned, so I do not believe the not feasible part.