使用 Choco 进行约束编程

banq
在本教程中，我们将学习Choco-solver，一种流行的 Java 约束编程 (CP) 框架。

在本文中，我们探索了 Choco-solver，一个用于解决组合问题的多功能且富有表现力的开源库。该库通过定义变量、其域值和约束，几乎以声明的方式帮助建模问题。因此，它允许我们获得多种解决方案，而无需编写任何特定于领域的逻辑。

总的来说，我们将简要了解 CP 的基础知识，然后了解 Choco-solver 库的关键概念。最后，我们将创建一个使用该库来解决数独难题的小程序。

约束规划(Constraint Programming)概念
CP是一种不同于传统确定性或命令式编程的范式，有助于解决组合问题。与约束编程相关的一些用例包括调度、规划、路由、打包、资源分配和解决数独难题。

首先，让我们回顾一下CP 的主要构造：

  • 变量：一组未知数 X 1， X 2， X 3，…， X n
  • 域：未知数的可能值，表示为 D 1、D 2、D 3、…、D k
  • 约束：将域值分配给变量时应满足的规则或标准，表示为 C 1， C 2， C 3，…， Cm
通常表示为 P = (X, D, C)，其中 P 代表问题

先决条件
在我们开始使用 Choco-solver 之前，让我们导入必要的Maven 依赖项：

<dependency>
   <groupId>org.choco-solver</groupId>
   <artifactId>choco-solver</artifactId>
   <version>4.10.14</version>
</dependency>

Choco-solver 的关键组件
让我们来看看 Choco-solver 框架的关键组件。在库中，Model类是保存变量和约束的容器或上下文：

Choco-solver 组件
Variable和Constraint类表示 CP 编程范式中的变量和约束。Model类实现了IVariableFactory接口，包括有效定义变量及其域值的方法。此外，它能够创建域值的单维和多维数组，为复杂问题建模提供了出色的灵活性和便利性。

此外，Model类实现了约束工厂接口，如IIntConstraintFactory。因此，其方法（如arithm()、sum()、allDifferent()等）有助于定义变量之间的算术关系。该库提供了许多其他方法来设置更复杂的约束。

定义变量和约束后，我们可以调用 Model#getSolver() 方法来获取 Solver类。此外，它的方法如Solver#solve()和 Solver#findSolution() 有助于获取解决方案。

此外，本文只是对 Choco-solver 库更广泛功能的预览。它为探索该库更复杂的功能提供了动力。

在下一节中，我们将在为数独板实施解决方案时了解更多信息。

解答空白数独板Sudoku Board
数独板Sudoku Board是一个 9 x 9 矩阵，包含九个 3 x 3 矩阵，每个矩阵都有 1 到 9 之间的唯一值。

空白数独板可以有多个解决方案。我们将每个单元格表示为一个变量，其域值从 1 到 9，并使用 Choco-solver 库实现SudokuSolver类。

1. 寻找多个解决方案
让我们看看SudokuSolver#findSolutions()方法：

List<Integer[][]> findSolutions(final int MAX_SOLUTIONS) {
    IntVar[][] sudokuCells = createModelAndVariables();
    setConstraints(sudokuCells);
    List<Integer[][]> solvedSudokuBoards = getSolutions(MAX_SOLUTIONS);
    return solvedSudokuBoards;
}

它在 s udokuCells中创建一个模型及其变量。然后，它对变量设置约束并最终获得解决方案。

2. 创建模型和变量
createModelAndVariables ()方法实例化模型并返回一个 9 x 9 矩阵：

IntVar[][] createModelAndVariables() {
    sudokuModel = new Model("Sudoku Solver");
    IntVar[][] sudokuCells = sudokuModel.intVarMatrix("board", 9, 9, 1, 9);
    return sudokuCells;
}

首先，我们创建带有标识符Sudoku Solver 的Model对象。接下来，我们通过在新创建的Model对象上调用Model#intVarMatrix()来创建一个二维 9 x 9 矩阵。它包含域值范围从 1 到 9 的IntVar变量。

3. 设置变量约束
下一步，我们对Model对象的域变量设置约束：

void setConstraints(IntVar[][] sudokuCells) {
    for (int i = 0; i < 9; i++) {
        IntVar[] rowCells = getRowCells(sudokuCells, i);
        sudokuModel.allDifferent(rowCells).post();
        IntVar[] columnCells = getColumnCells(sudokuCells, i);
        sudokuModel.allDifferent(columnCells).post();
    }
    for (int i = 0; i < 9; i += 3) {
        for (int j = 0; j < 9; j += 3) {
            IntVar[] cellsInRange = getCellsInRange(j, j + 2, i, i + 2, sudokuCells);
            sudokuModel.allDifferent(cellsInRange).post();
        }
    }
}

getRowCells ()和getColumnCells()方法分别返回第 i行和第 i 列中的所有单元格。然后，Model#allDifferent()对数独板的九行和九列中检索到的单元格变量设置约束。它确保域值 1-9 不会在任何行或列中重复。

此外，我们检索所有 3 x 3 网格的单元格并应用约束以确保其单元格中的值唯一。

4. 获取解决方案
最后，设置约束后，我们调用getSolutions()方法：

List<Integer[][]> getSolutions(int MAX_SOLUTIONS) {
    List<Integer[][]> solvedSudokuBoards = new ArrayList<>();
    int solutionCount = 0;
    while (sudokuModel.getSolver().solve()) {
        if (solutionCount++ > MAX_SOLUTIONS - 1) {
            break;
        }
        IntVar[] solvedSudokuCells = sudokuModel.retrieveIntVars(true);
        solvedSudokuBoards.add(getNineByNineMatrix(solvedSudokuCells));
        sudokuModel.getSolver().reset();
    }
    return solvedSudokuBoards;
}

该方法返回包含List中的解决方案的多个二维数组。Model#getSolver()获取Solver对象，我们在该对象上调用Solver#solve()用解决方案填充Model中的IntVar变量。

稍后，我们通过调用Model#retrieveIntVars()检索数组中的所有单元格值。在循环结束时，我们调用Solver#reset()来重置变量值。随后，该库在下一次迭代中将新解决方案填充到变量中。

5. 结果
现在，让我们运行SudokuSolver#findSolutions()方法来检查结果：

void whenSudokuBoardIsEmpty_thenFindTwoSolutions() {
    SudokuSolver sudokuSolver = new SudokuSolver();
    List<Integer[][]> sudokuSolutionMatrices = sudokuSolver.findSolutions(2);
    sudokuSolutionMatrices.forEach(e -> checkValidity(e));
    sudokuSolutionMatrices.forEach(sudokuSolver::printSolution);
}

该程序可帮助找到空白数独板的两个可能解决方案。找到解决方案后，它会调用checkValidity()来验证结果。最后，SudokuSolver#printSolution()方法打印 9 x 9 数独板：

3 7 2 | 1 5 6 | 4 9 8 
8 4 5 | 2 3 9 | 6 7 1 
1 9 6 | 8 7 4 | 3 2 5 
<hr>
5 3 1 | 6 2 7 | 8 4 9 
4 2 9 | 3 8 5 | 7 1 6 
7 6 8 | 4 9 1 | 2 5 3 
<hr>
9 1 4 | 7 6 3 | 5 8 2 
6 8 7 | 5 1 2 | 9 3 4 
2 5 3 | 9 4 8 | 1 6 7 

类似地，可以检索和打印多个解决方案。

解答部分解答的数独题
通常，在数独谜题中，棋盘是部分填满的。这次我们将以与上一节类似的方式处理这个问题。但是，只有一个解决方案。

1. 寻找单一解决方案
对于这样的场景，让我们在SudokuSolver类中实现findSolution()方法：

Integer[][] findSolution(int[][] preSolvedSudokuMatrix) {
    IntVar[][] sudokuCells = createModelAndVariables();
    setConstraints(sudokuCells, preSolvedSudokuMatrix);
    Solution solution = sudokuModel.getSolver().findSolution();
    IntVar[] solvedSudokuCells = solution.retrieveIntVars(true).toArray(new IntVar[0]);
    return getNineByNineMatrix(solvedSudokuCells);
}

该程序像以前一样声明变量并设置约束。但是，与上一个示例不同，它调用重载的setConstraints()方法，并附加一个二维数组参数。未解析的单元格在二维preSolvedSudokuMatrix数组中用0值表示。

现在让我们看一下方法setConstraints()：

void setConstraints(IntVar[][] sudokuCells, int[][] preSolvedSudokuMatrix) {
    setConstraints(sudokuCells);
    for (int i = 0; i < 9; i++) {
        for (int j = 0; j < 9; j++) {
            if (preSolvedSudokuMatrix<i>[j] != 0) {
                sudokuCells<i>[j].eq(preSolvedSudokuMatrix<i>[j])
                  .post();
            }
        }
    }
}

首先，调用setConstraints()帮助像以前一样设置默认约束。然后，从ArExpression接口继承的eq ()方法应用约束来分配preSolvedSudokuMatrix中预填充的单元格值。

最后，在SudokuSolver#findSolution()方法中，我们调用Solver#findSolution()来获取Solution对象。最终，Solution#retrieveIntVars()帮助检索已填充的单元格。

2. 结果
让我们考虑一个预先填充的数独板：

数独谜题
让我们运行SudokuSolver#findSolution()方法来填充其余字段：

void whenSudokuPartiallySolved_thenFindSolution() {
    SudokuSolver sudokuSolver = new SudokuSolver();
    Integer[][] solvedSudokuBoard = sudokuSolver.findSolution(initialValues);
    checkValidity(solvedSudokuBoard);
    sudokuSolver.printSolution(solvedSudokuBoard);
}

我们使用checkValidity()方法验证SudokuSolver#findSolution()的结果。然后，我们打印解决方案：

9 8 4 | 7 5 1 | 2 6 3 
5 7 3 | 4 6 2 | 8 9 1 
1 6 2 | 9 3 8 | 5 4 7 
<hr>
2 4 5 | 8 1 3 | 9 7 6 
7 9 8 | 6 2 4 | 3 1 5 
6 3 1 | 5 9 7 | 4 2 8 
<hr>
8 1 6 | 3 4 9 | 7 5 2 
3 5 9 | 2 7 6 | 1 8 4 
4 2 7 | 1 8 5 | 6 3 9