为什么 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)，但如果我使用大于 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();。这样，您就避免了一个与“x+2*y”相对应的中间变量，您强制它等于 z。在这样一个小例子中并不重要，但在依赖 ArExpression（用于算术表达式）时，可能会导致更大问题的内存问题。