MiniZinc / libminizinc

The MiniZinc compiler
http://www.minizinc.org
Other
510 stars 80 forks source link

2.6.2: Undeterministic behaviour on yumi-dynamic instances #563

Closed informarte closed 2 years ago

informarte commented 2 years ago

I ran

minizinc -c yumi-dynamic.mzn p_4_GG_GG_yumi_grid_setup_3_4_zones.dzn 

10 times on Linux and I obtained three different FlatZinc outputs and these are the diffs to the most common version:

Occurred two times:

1005,1006c1005,1006
< var 0..2613: X_INTRODUCED_1033_ ::var_is_introduced ;
< var 0..2613: X_INTRODUCED_1034_ ::var_is_introduced :: is_defined_var;
---
> var 0..2613: X_INTRODUCED_1033_ ::var_is_introduced :: is_defined_var;
> var 0..2613: X_INTRODUCED_1034_ ::var_is_introduced ;
4066,4067c4066,4067
< constraint array_var_int_element(X_INTRODUCED_1038_,arrival_time,X_INTRODUCED_1033_);
< constraint array_var_int_element(X_INTRODUCED_39_,arrival_time,X_INTRODUCED_1034_):: defines_var(X_INTRODUCED_1034_);
---
> constraint array_var_int_element(X_INTRODUCED_1038_,arrival_time,X_INTRODUCED_1033_):: defines_var(X_INTRODUCED_1033_);
> constraint array_var_int_element(X_INTRODUCED_39_,arrival_time,X_INTRODUCED_1034_);

Both X_INTRODUCED1033 and X_INTRODUCED1034 could be functionally defined and, btw, X_INTRODUCED1032, too.

Occurred two times:

179c179
< var 216..2613: X_INTRODUCED_145_;
---
> var 216..2613: X_INTRODUCED_145_:: is_defined_var;
4261c4261
< constraint int_lin_eq(X_INTRODUCED_1125_,[X_INTRODUCED_1033_,X_INTRODUCED_1274_,X_INTRODUCED_145_],0);
---
> constraint int_lin_eq(X_INTRODUCED_1125_,[X_INTRODUCED_1033_,X_INTRODUCED_1274_,X_INTRODUCED_145_],0):: defines_var(X_INTRODUCED_145_);
Dekker1 commented 2 years ago

To investigate this issue we will need the models and data files. It would be great if you would be able to actually create a minimal example of the issue.

informarte commented 2 years ago

yumi-dynamic is a 2021 MiniZinc challenge problem, so see https://www.minizinc.org/challenge2021/mznc2021_probs.tar.gz for all the files.

informarte commented 2 years ago

I am not the author of yumi-dynamic, so I think I would have a hard time to create a minimal example. As a software engineer, I would rather start by looking for use of uninitialized memory using a tool like Google's MemorySanitizer.

Dekker1 commented 2 years ago

Although uninitialised memory might be the cause. The compiler also makes use of many unordered map structures that uses pointers as keys. It wouldn't be unlikely that these will be the issue when it comes to these types of ordering differences.

Currently in implementation MiniZinc is mostly deterministic, but I'm not sure if we can invest the time to guarantee that this is the case.

informarte commented 2 years ago

@Dekker1, the first diff looks to me like one variable turned is_defined_var while the other lost this status, but maybe it's just an ordering problem. However, the second diff shows clearly that a variable lost the is_defined_var status which, of course, affects solvers which consider this status.