I'm learning to use Choco-solver. I found that it fails to find a solution to a very simple problem, which means that I must have misunderstood something...
I reduced my code to this:
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();
So, three integer variables and one constraint saying that z = x + 2y. Choco-solver responds Complete search - No solution.
I find that I get correct solutions if I change the inner part of the constraint from y.mul(2) to y.mul(1) (x = 1, y = 1, z = 2) or to y.add(2) (x = 1, y = 1, z = 4). I can even set it to y.mul(-2) (x = 1 y = 9 z = -17), but if I use mul with an integer larger than 1 the constraint seems to be unsolveable.
What is going on here?
This was indeed a bug in Choco Solver 4.10.7. This bug has been fixed since: https://github.com/chocoteam/choco-solver/issues/841
If you want to use the fixed version, I invite you to download the code from GitHub and compile it using Maven.
Concerning your constraint, I advise you to post an arithm constraint as following: model.arithm(x, "+", y.mul(2).intVar(), "=", z).post();. This way, you avoid having an intermediate variable corresponding to "x+2*y" that you force to be equal to z. It does not really matter in such a small example, but it could lead to memory issues on bigger problems while relying on ArExpression (for Arithmetical Expression).