Linearized model leads to UNSAT or unfeasible solutions given the bound

[raphaelboudreault]

OS: Linux Ubuntu 22.04 MZN version: 2.8.5

Hello! I am currently working on a MiniZinc model involving float and integer variables, using a linear solver (in my case, SCIP 8.0.4). In the model, I have an array of float variable declared under the form array[X, Y] of var 0.0..<float bound>: x, involved in numerous constraints. However, depending on the value used for <float bound>, I am getting different results. Using a value of 1000.0, the returned solution is optimal and as expected. Using instead a value of 100000000.0, the solver returns UNSAT. See attached the generated FZN in both cases, which differ only by a factor in the domains and paremeters. Clearly, this is not an expected behavior, and I wonder if it is related to MiniZinc or the solver. CPLEX allows instead an unfeasible solution using the biggest value.

On another note, using

array[X, Y] of var float: x
constraint forall(i in X, j in Y)(x[i, j] >= 0 /\ x[i, j] <= <float bound>)

leads to

MiniZinc: flattening error: unbounded coefficient in linear expression. Make sure variables involved in non-linear/logical expressions have finite bounds in their definition or via constraints

where I felt like the two formulations should be equivalent from the point of view of MiniZinc. Thanks!

linear_NO.txt linear_OK.txt

[ImadAziez]

Hello, I am facing a similar issue when working with float and integer variables in MiniZinc. I’ve noticed that when I change the upper bound for my float variables, I also get different results from the solver. I haven’t found a solution yet, and I’m wondering if anyone has come across this issue or if there's a workaround. Thank you!