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

Question

我正在学习使用 Choco-solver。我发现一个很简单的问题都找不到解决办法，也就是说我一定是理解错了什么...

我将代码缩减为：

    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-solver 响应 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 = 1 y = 9 z = -17)，但是如果我使用 mul 且整数大于 1，则约束似乎无法解决。

这是怎么回事？

Answer 1

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

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

关于你的约束，我建议你post一个算术约束如下：model.arithm(x, "+", y.mul(2).intVar(), "=", z).post();。这样，您就可以避免有一个对应于您强制等于 z 的“x+2*y”的中间变量。在这么小的例子中这并不重要，但在依赖 ArExpression（用于算术表达式）时，它可能会导致更大问题的内存问题。

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

Why doesn't Choco-solver find a solution?

choco