jump-dev / MiniZinc.jl

A Julia interface to the MiniZinc constraint modeling language
https://www.minizinc.org/
MIT License
18 stars 4 forks source link

Handling numerical Issues in model #54

Closed zengjian-hu-rai closed 11 months ago

zengjian-hu-rai commented 11 months ago

When model contains numbers >= typemax(Int32), I noticed some strange behaviors. Check the following simple model:

large_n = typemax(Int32)

Issue 1: if we set rhs = large_n, I got an error msg:

ERROR: LoadError: MathOptInterface.UnsupportedConstraint{MathOptInterface.ScalarNonlinearFunction, MathOptInterface.GreaterThan{Int32}}: MathOptInterface.ScalarNonlinearFunction-in-MathOptInterface.GreaterThan{Int32} constraint is not supported by the model.

However, the error'd disappear if we set rhs to something even bigger e.g., 2*large_n?

Issue 2: When we set rhs = 2*large_n, it returns MOI.OPTIMAL

var 1 .. 10: x1; var 1 .. 10: x2; constraint ((x1 * 2147483647) + x2) >= 4294967294; solve satisfy;

But, if we set large_n = typemax(Int32) + 2, it returns MOI.INFEASIBLE

var 1 .. 10: x1; var 1 .. 10: x2; constraint ((x1 * 2147483649) + x2) >= 4294967298; solve satisfy;

Looks like the solver (chuffed) can't handle these large numbers. Should we always warn user when there is numerical issue in the model? What error message'd be appropriate?

Repro:

function test_moi_numerical_issue()
    model = MOI.Utilities.Model{Int}()
    x, _= MOI.add_constrained_variable(model, MOI.Integer())
    y, _= MOI.add_constrained_variable(model, MOI.Integer())
    MOI.add_constraint(model, x, MOI.Interval(1, 10))
    MOI.add_constraint(model, y, MOI.Interval(1, 10))
    large_n = typemax(Int32) 
    snf1 = MOI.ScalarNonlinearFunction(:*, Any[x, large_n])
    rhs = large_n
    c1 = MOI.add_constraint(model, MOI.ScalarNonlinearFunction(:+, Any[snf1, y]), MOI.GreaterThan(rhs))
    optimizer = MiniZinc.Optimizer{Int}("chuffed")
    index_map,_ = MOI.optimize!(optimizer, model)
    @test MOI.get(optimizer, MOI.TerminationStatus()) === MOI.INFEASIBLE
    @test MOI.get(optimizer, MOI.ResultCount()) == 0
    @test MOI.get(optimizer, MOI.RawStatusString()) == "UNSATISFIABLE"
end
odow commented 11 months ago

For 1:

You have defined MOI.Utilities.Model{Int}() which has value type Int64. But the MOI.GreaterThan(rhs) is MOI.GreaterThan{Int32}. The value type of your sets must match the value type of the model. Using 2 * rhs promotes to Int64 and so things work.

For 2:

This should come from an error or warning in libminizinc or chuffed itself.

MiniZinc.jl can not decide whether the solver experienced numerical issues based on the values. Our job is just to tell the user what libminizinc reports. (For example, if you used "highs" it should probably work.)

chriscoey commented 11 months ago

@odow thanks - looking at just case 2, we'd like it if MiniZinc could throw an error that an int64 in an MOI model couldn't be converted to an int32, or something like that.

odow commented 11 months ago

I don't fully understand. Is libminizinc limited to int32? If so, why doesn't it throw an error? We just write the .mzn file format. If libminizinc can't deal with it, that should be their problem, not ours.

chriscoey commented 11 months ago

internally on a different (larger) example we saw errors like:

│ failed process: Process(`/Users/jhu/.julia/artifacts/f5a7ecea4a8a9ee26d48f4fcce9af54d211adcb4/bin/minizinc --solver /Users/jhu/.julia/artifacts/3d101099493ef72978acae4a0a14eb1cbdb2a731/chuffed.msc --output-objective -o /tmp/jl_DnU1Uo/model.ozn /tmp/jl_DnU1Uo/model.mzn --time-limit 300000`, ProcessExited(1)) [1] 

and

Error: The literal '3531929349' of the type int is out of range (-2147483646..2147483646) in line no. 601
Error: syntax error, unexpected ':', expecting FZ_INT_LIT in line no. 601

we'll try to get you something to reproduce these

odow commented 11 months ago

I think this is a bug in Chuffed. And some solvers do not support int64.

The (infeasible) model is:

var 1 .. 10: x;
var 1 .. 10: y;
constraint 2147483647 * x - y >= 21474836470;
solve satisfy;

Chuffed 0.10.4

x = 10;
y = 10;

COIN-BC 2.10.7

=====UNSATISFIABLE=====

Gecode 6.3.0

Error: The literal '-2147483647' of the type int is out of range (-2147483646..2147483646) in line no. 1
Error: syntax error, unexpected ',', expecting ']' in line no. 1
=====ERROR=====
chriscoey commented 11 months ago

Ah thanks Oscar. Ideally when we call a MiniZinc via MOI and something like that isn't supported, we would get an informative error back. Is that possible to do here?

odow commented 11 months ago

I've confirmed that it's still an issue with the latest minizinc release. opened an issue: https://github.com/chuffed/chuffed/issues/157

Is that possible to do here?

Not really. Hopefully we can handle the =====ERROR===== case without crashing, but we can't tell if a solution is incorrect because of numerical issues, or if it is really feasible when the solver reports unsatisfiable.

chriscoey commented 11 months ago

Thank you Oscar! Very helpful

odow commented 11 months ago

Okay, we should be able to catch the error case without crashing your process.

odow commented 11 months ago

So I've marked this as closed and I'll release a new version. That should fix your error, although now MOI will return OTHER_ERROR (but you should handle this in the application?).

If that's not sufficient, please comment and I'll re-open.

chriscoey commented 11 months ago

Thanks - I think that's all we can expect from minizinc.jl probably. Hopefully Chuffed devs will fix their overflow bug!