Panic due to overflow when using unbounded integers

[JulGvoz]

Link to .fzn file: https://gist.github.com/JulGvoz/2e2602562d56495775b12ec8bad689ca

When running as MZN_SOLVER_PATH=path/to/Pumpkin minizinc --time-limit 10000 -s --solver pumpkin input.fzn

The solving process crashes with:

% Generated FlatZinc statistics:
%%%mzn-stat: paths=0
%%%mzn-stat: flatBoolVars=901
%%%mzn-stat: flatIntVars=603
%%%mzn-stat: flatBoolConstraints=1451
%%%mzn-stat: flatIntConstraints=1103
%%%mzn-stat: evaluatedHalfReifiedConstraints=480
%%%mzn-stat: method="minimize"
%%%mzn-stat: flatTime=0.0454977
%%%mzn-stat-end

thread 'main' panicked at pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs:139:18:
all predicates in the conflict nogood should be assigned to true
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
=====ERROR=====
%%%mzn-stat: nSolutions=0
%%%mzn-stat-end

[ImkoMarijnissen]

Thank you for providing this instance!

At a cursory glance, when running in debug mode on the current main (301551a), it indicates that an overflow occurs. In this case, we expect the behaviour of the solver to be undetermined.

I will have another look tomorrow, but I think that this is an inherent limitation of using i32s (though it is not guaranteed that using an i64 would solve the issue).

[JulGvoz]

Other solvers that I ran it with (Gecode, CP-SAT, Chuffed) seemed to work fine on it - I wonder if there is a deeper reason why Pumpkin specifically fails? (Or perhaps other solvers return a wrong result?)

[ImkoMarijnissen]

Looking a bit further into it, I think this has to do with the unbounded integers, which are contained in the model you provided (which we only recently started supporting in #285).

The behaviour of Gecode is interesting in this regard. If I give it the following model:

var int: x;
solve minimize x;

Then it will output an objective (and value of x) of -2_147_483_646.

However, if you give it this model:

var int: x;
solve minimize 1500 * x;

Then it will output a value of x of -1_431_655 with an objective value of -2_147_482_500, a significantly lower value of x than it output when the objective was not weighted. To me, this indicates that they might perform dynamic scaling of bounds depending on weights.

Chuffed and OR-Tools CP-SAT appear to do something similar, so it could be interesting to look into!

[JulGvoz]

I assume that if there's a term such as 1500 * x, then a new variable is created, say y, and a constraint y = 1500*x. Since y initially is "unbounded", i.e. it's bounds are set to i32 bounds, then the propagator for the constraint would correspondingly update x.