MiniZinc定义0-10中4的倍数约束报unsatisfiable错误原因咨询

问题原因 #

你的第二种写法存在两个明显错误：

• 变量名引用错误：你定义的合法值数组名为div_by_4，但约束里遍历的是未定义的数组not_div_by_4，直接触发了模型不一致警告。
• 量词逻辑错误：forall是全称量词，要求所有遍历到的条件都成立。就算你修正了变量名，约束会要求x同时等于0、4、8三个不同的值，显然不可能满足，自然返回不可满足的结果。

修正方案 #

如果要基于合法值数组写约束，有两种可行写法：

1. 把全称量词替换为存在量词exists，只要x等于数组中任意一个元素即可：

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]);

2. 更简洁的写法是直接用in运算符判断x属于合法值集合，不需要额外定义数组：

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

内容的提问来源于stack exchange，提问作者Balaji Srinivasa