2
$\begingroup$

I have the following model.

array[int] of float: weight;
set of int: nodes = index_set(weight);
int: n = max(nodes);

array[nodes] of var 1..n: segment_start;
array[nodes] of var 0..0: segment_length;

function var float: segment_weight(int: s) = 
  sum 
    (i in segment_start[s]..(segment_start[s] + segment_length[s] - 1) where i <= n)
    (weight[i]);

var float: mass = sum (s in nodes) (segment_weight(s));

solve satisfy;

The model is unsatisfiable according to MiniZinc, however, when I get rid of the variable mass, a solution is found. How can an existence of a variable (i.e. not a constraint) influence whether a model is solvable? Does it have sometime to do with optional types? And how do I fix this?

Improve this question
$\endgroup$
3
  • $\begingroup$ The issue may be with your data (which is not shown here). $\endgroup$
    – prubin ♦
    Dec 2, 2021 at 17:06
  • $\begingroup$ I can try to modify the data on my side and see how it affects the outcome. The question still stands, though; how can adding a variable change the satisfiability? $\endgroup$
    – Eugleo
    Dec 2, 2021 at 18:56
  • $\begingroup$ One possibility would be that something in the data makes segment_weight(s) undefined for a specific value of s. $\endgroup$
    – prubin ♦
    Dec 2, 2021 at 20:20

1 Answer 1

Reset to default
3
$\begingroup$

It seems you ran into an issue in the MiniZinc compiler. Running with weight = [1,2,3]; under the current release (2.5.5) does indeed give UNSAT (even though it shouldn't):

$ minizinc --solver cbc ./should_work.mzn
=====UNSATISFIABLE=====

However, if you run using the current develop branch of MiniZinc then it does give an asnwer:

$ ./github.com/MiniZinc/libminizinc/build/Debug/minizinc --solver cbc ./should_work.mzn
segment_start = [1, 1, 1];
segment_length = [0, 0, 0];
----------

I do not know exactly where this issue was solved, but I can say that a new release of MiniZinc will soon be available that should include this fix. In the meantime you could already use the develop branch of MiniZinc.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.