choco ソルバー ライブラリを使用して一連のパズルを生成しています。ソルバーを実行し、解がいくつあるかを確認し、複数ある場合は制約を追加する必要があります。これを繰り返すと、独自の解決策を持つ一連の制約 (手がかり) が得られます。
ただし、 model.getSolver(findAllSolutions()) を実行すると、追加のチェックはゼロのソリューションを返します。
どうにかしてモデル ソルバーをリセットする必要があると思いますが、これを達成する方法が見つかりません。必要に応じて、新しいモデルを生成したり、既存の制約を再作成したりしたくありません。
元のコードには 110 の IntVar と膨大な数の制約がありますが、私ははるかに小さな例を作成しました。
注: 実際のアプリケーションでは、高速化のために model.getSolver().findAllSolutions(new SolutionCounter(model,2)) を使用していますが、ここではその手順を省略しています。
Model model = new Model();
// setup two doors A and B, one has the value 0 the other 1
IntVar doorA = model.intVar("Door A", 0, 1);
IntVar doorB = model.intVar("Door B", 0, 1);
model.allDifferent(new IntVar[]{doorA, doorB}).post();
// setup two windows A and B, one has the value 0 the other 1
IntVar windowA = model.intVar("Window A", 0, 1);
IntVar windowB = model.intVar("Window B", 0, 1);
model.allDifferent(new IntVar[]{windowA, windowB}).post();
// assign the first constraint and count the solutions
model.arithm(doorA,"=",0).post();
// this should force door B to be 1 - there are two remaining solutions
List<Solution> solutions = model.getSolver().findAllSolutions();
System.out.println("results after first clue");
for (Solution s : solutions) {
System.out.println(">"+s.toString());
}
assertEquals("First clue leaves two solutions",2,solutions.size());
// add second clue
model.arithm(windowA,"=",1).post();
// this should force window B to by 0 - only one valid solution
List<Solution> solutions2 = model.getSolver().findAllSolutions();
System.out.println("results after second clue");
for (Solution s : solutions2) {
System.out.println(">"+s.toString());
}
assertEquals("Second clue leaves one solution",1,solutions2.size());