对于不同定义的相同约束，问题是不可满足的

Question

我是 minizinc 的初学者，我试图在不使用 mod 函数的情况下为 0 到 10 范围内的 4 的倍数定义一个约束。

这行得通：

var 0..10: x;
array[1..8] of int: not_div_by_4 = [ 1, 2, 3, 5, 6, 7, 9, 10 ]; 
constraint forall (i in 1..length(not_div_by_4))(x != not_div_by_4[i]);

虽然这不起作用，并声称它不能满足模型不一致警告（我想这是一个线索）：

var 0..10: x;
array[1..3] of int: div_by_4 = [ 0, 4, 8 ]; 
constraint forall (i in 1..length(not_div_by_4))(x == not_div_by_4[i]);

知道定义约束的第二种方式有什么问题吗？

Answer 1

您的第二个代码要求一个变量同时等于几个不同的值。这是不可满足的，并且在编译时会被检测到。

以下作品：

var 0..10: x;
array[1..3] of int: div_by_4 = [ 0, 4, 8 ]; 
constraint exists (i in 1..length(div_by_4))(x == div_by_4[i]);

更短的方法：

var 0..10: x;
constraint x in {0, 4, 8};