Choice of output can make Gecode 6.3.0 nonterminate #220

Activity

1. zayenz commented on Sep 9, 2025

   

   zayenz

   on Sep 9, 2025

   Last edited by zayenz

   More actions

   This is, unfortunately, a known and hard to explain behavior. There are two things that change when changing the output variables in MiniZinc and using Gecode

   • The problem changes in that the projected set of solutions change.
   • The default search strategy changes. Gecode by default, when no search strategy is given, uses the output variables as a heuristic on what variables might be important to search on.

   The first problem can be seen in a problem like this

   var 0..10: x;
   var 0..10: y;
   var 0..10: z;
   
   constraint x < y;
   constraint y < z;
   
   solve satisfy;
   
   output ["x: \(x), z: \(z)"];
   

   This problem has a total of 45 solutions, one for each pair of values for x and z that are separated by one step (as witnessed by the y variable). Since the y variable is not in the output, Gecode doesn't care what value it has, just that it has some value. However, changing the output-line to output ["x: \(x), y: \(y), z: \(z)"]; gives a total of 165 solutions, for each original solution we now also print out the witness that x and z have a value between them.

   The second problem is also problematic, since it can give wildly different search trees. The heuristic is good in general, but very problematic when trying to solve a problem and adding "debug" output. If there is a usable search heuristic to specify, that goes a long way to ameliorate this problem.

   Now, in this case I think both these issues are to blame, but mostly that the search heuristic changed. But, there is also also a third issue. Minimization search means that after each solution is found with value v for the objective, a constraint objective < v is added. For float variables, this is implemented as objective < v - step for some fixed step value. The default setting for step is 0 though, which means that this added constraint is a very weak constraint as the next better solution might be infinitesimally better.

   There are two way around this, both around increasing the step value.

   1. Adding the --step parameter to the Gecode backend. In the MiniZinc IDE this can be added as a custom parameter --step of flag type solver backend, with a string argument of say 0.001. This solves the problem with a bit more search than the original output definition, but not significantly.
   2. Setting a default search like float_search([c], 0.0, input_order, indomain_min), which specifies that the main variable to search on is the c variable. This solves the problem in a similar amount of search as with the original output statement and no search annotation.