[gecode-users] Issue with a MiniZinc model

[Lucie Kučerová]

Hello,

I've created a simple MiniZinc model describing a planning domain &
problem. The issue is that although MiniZinc itself solves it instantly,
when I use Gecode's fz.exe on the generated FlatZinc model, the program
computes for a while and then crashes.

The MiniZinc model in question is attached below. The only problematic
constraint is the last one from the succesor state constraints, without
it all works OK. Any ideas what is causing the issue?

Thank you in advance
Lucie Kucerova



% Constants
int: t = 2;
int: num_preds = 5;
int: num_actions = 6;
int: num_resc = 1;

% Variables
array[0..t, 0..num_preds - 1] of var bool: predicates;
array[0..t - 1, 0..num_actions - 1] of var bool: actions;
array[0..t, 0..num_resc - 1] of var int: resources;

% Constraints

% Init
constraint predicates[0, 0];
constraint not predicates[0, 1];
constraint not predicates[0, 2];
constraint not predicates[0, 3];
constraint not predicates[0, 4];
constraint resources[0, 0] = 0;

% Goal
constraint predicates[t, 3];
constraint predicates[t, 4];
constraint resources[t, 0] = 100;

% Preconditions
constraint forall (i in 0..t - 1) (actions[i, 0] -> predicates[i, 0]);
constraint forall (i in 0..t - 1) (actions[i, 1] -> predicates[i, 1]);
constraint forall (i in 0..t - 1) (actions[i, 2] -> predicates[i, 0]);
constraint forall (i in 0..t - 1) (actions[i, 3] -> predicates[i, 2]);

% Succesor state
constraint forall (i in 1..t) (predicates[i, 0] <-> predicates[i - 1, 0]
/\ not actions[i - 1, 0] /\ not actions[i - 1, 2]);
constraint forall (i in 1..t) (predicates[i, 1] <-> actions[i - 1, 0] \/
(predicates[i - 1, 1] /\ not actions[i - 1, 1]));
constraint forall (i in 1..t) (predicates[i, 2] <-> actions[i - 1, 1] \/
actions[i - 1, 2] \/ (predicates[i - 1, 2] /\ not actions[i - 1, 3]));
constraint forall (i in 1..t) (predicates[i, 3] <-> actions[i - 1, 3] \/
predicates[i - 1, 3]);
constraint forall (i in 1..t) (predicates[i, 4] <-> actions[i - 1, 4] \/
predicates[i - 1, 4]);
constraint forall (i in 1..t) ((resources[i, 0] = resources[i - 1, 0])
\/ ((resources[i, 0] = resources[i - 1, 0] + 100) /\ actions[i - 1, 5]));

% Incompatible predicates
constraint forall (i in 0..t) (bool2int(predicates[i, 0]) +
bool2int(predicates[i, 1]) + bool2int(predicates[i, 2]) +
bool2int(predicates[i, 3]) < 2);

% Solution
solve satisfy;

% Output
output
  [ show(predicates[i,j]) ++ " " ++ if j == num_preds - 1 then "\n" else
" " endif | i in 0..t, j in 0..num_preds - 1] ++
  ["\n"] ++
  [ show(resources[i,j]) ++ " " ++ if j == num_resc - 1 then "\n" else "
" endif | i in 0..t, j in 0..num_resc - 1] ++
  ["\n"] ++
  [ show(actions[i,j]) ++ if j == num_actions - 1 then "\n" else " "
endif | i in 0..t - 1, j in 0..num_actions - 1];