PatrickTrentin88 / fzn2omt

Tools/Scripts to convert MiniZinc/FlatZinc to Optimization Modulo Theories (OMT) for BCLT, OptiMathSAT or Z3 and Satisfiability Modulo Theories (SMT) for CVC4.
8 stars 0 forks source link

Warning for unbounded objective when objective is bounded #10

Open GustavBjordal opened 4 years ago

GustavBjordal commented 4 years ago

For the following MiniZinc model

var 1..10:x;
var 1..10:y;

solve minimize x*y;

which flattens into

var 1..10: x:: output_var;
var 1..10: y:: output_var;
var 1..100: X_INTRODUCED_0_:: is_defined_var;
constraint int_times(x,y,X_INTRODUCED_0_):: defines_var(X_INTRODUCED_0_);
solve  minimize X_INTRODUCED_0_;

fzn2optimathsat.py outputs: % warning: X_INTRODUCED_0_ is unbounded: oo. This seems a bit odd, no?

PatrickTrentin88 commented 4 years ago

Definitively! What version of OptiMathSAT are you using?

This is the result I get with version 1.7.2:

~$ optimathsat-1.7.2-linux-64-bit/bin/optimathsat -optimization=True -opt.verbose=True -input=fzn < test.fzn 
# obj(X_INTRODUCED_0_) := X_INTRODUCED_0_
# obj(X_INTRODUCED_0_) - search start: [ (- oo), oo ]
# obj(X_INTRODUCED_0_) - linear step: 1
# obj(X_INTRODUCED_0_) -  new: 1
# obj(X_INTRODUCED_0_) -  update upper: [ (- oo), 1 ]
# obj(X_INTRODUCED_0_) - binary step: 1
# obj(X_INTRODUCED_0_) - pivot: (not (<= 0 X_INTRODUCED_0_))
# obj(X_INTRODUCED_0_) -  update lower: [ 0, 1 ]
# obj(X_INTRODUCED_0_) - linear step: 2
# obj(X_INTRODUCED_0_) - search end: sat_optimal
# obj(X_INTRODUCED_0_) -  update lower: [ 1, 1 ]
% objective: X_INTRODUCED_0_ (optimal model)
x = 1;
y = 1;
----------
==========

and also:

~$ fzn2optimathsat.py test.fzn 
% objective: X_INTRODUCED_0_ (optimal model)
x = 1;
y = 1;
----------
==========
GustavBjordal commented 4 years ago

Sorry I forgot to add the version: 1.7.2, linux 64-bit. Running on Python 3.6.

It seems like it only happens when fzn2optimathsat.py is called with the -a flag, as it usually is via the IDE:

~$ fzn2optimathsat.py foo.fzn 
% objective: X_INTRODUCED_0_ (optimal model)
x = 1;
y = 1;
----------
==========
~$ fzn2optimathsat.py -a foo.fzn 
% objective: X_INTRODUCED_0_ (model)
% warning: X_INTRODUCED_0_ is unbounded: oo
x = 1;
y = 1;
----------
% objective: X_INTRODUCED_0_ (optimal model)
x = 1;
y = 1;
----------
==========
PatrickTrentin88 commented 4 years ago

Sorry I forgot to add the version: 1.7.2, linux 64-bit. Running on Python 3.6.

It seems like it only happens when fzn2optimathsat.py is called with the -a flag, as it usually is via the IDE:

~$ fzn2optimathsat.py foo.fzn 
% objective: X_INTRODUCED_0_ (optimal model)
x = 1;
y = 1;
----------
==========
~$ fzn2optimathsat.py -a foo.fzn 
% objective: X_INTRODUCED_0_ (model)
% warning: X_INTRODUCED_0_ is unbounded: oo
x = 1;
y = 1;
----------
% objective: X_INTRODUCED_0_ (optimal model)
x = 1;
y = 1;
----------
==========

Thanks! Now I can reproduce the issue.

The model printing routine of OptiMathSAT was initially designed to handle models at the end of the optimization, rather than partial solutions. I guess that I haven't thought of that occurrence when extending its behavior. I'll get it fixed in the next release. For now you can just ignore it for partial models. Thanks!!