使用Choco-solver进行约束编程

1. 概述

本文将介绍Choco-solver——一个流行的Java约束编程（CP）框架。我们将简要理解CP的基础概念，然后深入Choco-solver库的核心组件，最后通过实现数独求解器来展示其实际应用。

2. 约束编程概念

CP是一种区别于传统确定性编程或命令式编程的范式，专门用于解决组合优化问题。典型应用场景包括：

✅ 调度规划
✅ 路径优化
✅ 资源分配
✅ 数独谜题求解

CP的核心构成要素：

变量：未知数集合 X₁, X₂, X₃,..., Xₙ
域：变量的可能取值范围 D₁, D₂, D₃,..., Dₖ
约束：变量赋值时需满足的规则 C₁, C₂, C₃,..., Cₘ
问题表示：P = (X, D, C)

3. 环境准备

使用Choco-solver前需添加Maven依赖：

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

4. Choco-solver核心组件

Choco-solver框架的核心组件关系如下：

关键组件说明：

Model类：作为容器管理变量和约束
- 实现IVariableFactory接口，支持高效定义变量及其域
- 支持创建单维/多维数组，便于建模复杂问题
Variable类：表示CP中的变量
Constraint类：表示约束规则
Model类还实现约束工厂接口（如IIntConstraintFactory），提供：
- arithm()：算术关系约束
- sum()：求和约束
- allDifferent()：互异约束
- 其他复杂约束方法

求解流程：

定义变量和约束
通过Model#getSolver()获取Solver实例
调用Solver#solve()或Solver#findSolution()获取解

⚠️ 本文仅展示Choco-solver的基础能力，该库还支持更高级的功能，读者可自行探索。

5. 求解空白数独

数独是9×9矩阵，包含9个3×3子矩阵，每个单元格需填入1-9的唯一值。空白数独存在多解，我们将每个单元格建模为域[1,9]的变量。

5.1 查找多解

核心方法SudokuSolver#findSolutions()：

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

    List<Integer[][]> solvedSudokuBoards = getSolutions(MAX_SOLUTIONS);
    return solvedSudokuBoards;
}

执行步骤：

创建模型和变量
设置约束
获取解

5.2 创建模型和变量

createModelAndVariables()实现：

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

关键点：

创建标识为"Sudoku Solver"的Model实例
通过intVarMatrix()生成9×9的IntVar矩阵
每个变量的域为[1,9]

5.3 设置变量约束

setConstraints()实现：

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();
        }
    }
}

约束设置逻辑：

行约束：每行9个单元格值互异
列约束：每列9个单元格值互异
3×3子矩阵约束：每个子矩阵内值互异

5.4 获取解

getSolutions()实现：

List<Integer[][]> getSolutions(int MAX_SOLUTIONS) {
    List<Integer[][]> solvedSudokuBoards = new ArrayList<>();
    int solutionCount = 0;
    while (solutionCount++ < MAX_SOLUTIONS && sudokuModel.getSolver().solve()) {
        IntVar[] solvedSudokuCells = sudokuModel.retrieveIntVars(true);

        solvedSudokuBoards.add(getNineByNineMatrix(solvedSudokuCells));
        sudokuModel.getSolver().reset();
    }
    return solvedSudokuBoards;
}

关键操作：

getSolver().solve()：填充变量值生成解
retrieveIntVars()：提取所有单元格值
reset()：重置变量状态以查找下一解

5.5 运行结果

测试代码：

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

输出示例（9×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 
---------------------
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 
---------------------
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

6. 求解部分填充数独

实际数独通常部分填充，此时只有唯一解。

6.1 查找单解

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);
}

特殊处理：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();
            }
        }
    }
}

关键点：

先应用基础约束（行/列/子矩阵互异）
对非零单元格添加eq()约束（继承自ArExpression接口）

6.2 运行结果

输入示例（部分填充数独）：