为什么 Choco-solver 找不到解决方案？

Question

我正在学习使用Choco解算器。我发现它无法找到解决一个非常简单的问题的方法，这意味着我一定误解了什么。。。

我把我的代码简化为：

Model model = new Model("Minimum");
IntVar x = model.intVar("x", 1, 9, false);
IntVar y = model.intVar("y", 1, 9, false);
IntVar z = model.intVar("z", -1000, 1000, false);
z.eq(x.add(y.mul(2))).post();
Solver solver = model.getSolver();
solver.showStatistics();
solver.showSolutions();
solver.findSolution();

因此，三个整数变量和一个约束条件表示z = x + 2y。Choco解算器响应Complete search - No solution。

如果我将约束的内部从y.mul(2)更改为y.mul(1)(x=1，y=1，z=2(或y.add(2)(x=1、y=1，z=4(，我发现我得到了正确的解。我甚至可以将其设置为y.mul(-2)(x=1y=9z=-17(，但如果我使用大于1的整数的mul，则约束似乎无法解决。

这是怎么回事？

Answer 1

这确实是Choco Solver 4.10.7中的一个错误。此错误已修复，时间为：https://github.com/chocoteam/choco-solver/issues/841

如果你想使用固定版本，我邀请你从GitHub下载代码，并使用Maven进行编译。

关于你的约束，我建议你发布一个算术约束如下：model.arithm(x, "+", y.mul(2).intVar(), "=", z).post();。这样，就避免了有一个对应于"0"的中间变量；x+2*y"；这在这样一个小例子中并不重要，但在依赖ArExpression(算术表达式(的情况下，它可能会导致更大问题的内存问题。