原文: SQL Sudoku Constraint Programming
#1
SQL 数独：约束编程
CM Lubinski
考虑数独游戏，最常在九乘九的单元格网格上进行，其中每个单元格可以包含1到9的整数之一。游戏规定每一行必须只包含互不相同的元素，每一列以及九个三乘三的子棋盘也必须如此。具体的游戏开局时，棋盘上已有一些单元格被预先填入数字，玩家需要推导出剩余的值。
实际上，我们可以比"推导"更具体；我们玩游戏时，很可能是在减少每个单元格可能的选择数量。我们认识到每条规则——例如行包含互不相同的值等——限制了它所影响的单元格的取值。赢得游戏等同于找到一组不违反任何规则的单元格取值。我们难道不能简单地定义规则，然后让计算机来搜索吗？它肯定会实现比我们使用的任何策略都更高效的方法。
这正是约束编程（一种声明式编程）所承诺的。为了进一步介绍它，让我们看看其中一个更常见的实现：SQL。
SQL 数独
通过在 SQL 中实现数独，我们将看到一些在整个约束编程中反复出现的高级概念。我们还会遇到 SQL 实现中的几个痛点，这些问题可以通过使用更通用的语言（如稍后介绍的 Minizinc）来缓解。
让我们首先为每个单元格创建一个值域；这是任意单元格可能包含的所有可能值的集合（1-9）。
CREATETABLEcell_domain(vint);INSERTINTOcell_domainVALUES(1);INSERTINTOcell_domainVALUES(2);INSERTINTOcell_domainVALUES(3);INSERTINTOcell_domainVALUES(4);INSERTINTOcell_domainVALUES(5);INSERTINTOcell_domainVALUES(6);INSERTINTOcell_domainVALUES(7);INSERTINTOcell_domainVALUES(8);INSERTINTOcell_domainVALUES(9);一行由九个这样的值组成，要求每个单元格的值互不相同。我实在想不出比逐个比较每对值（我们很快会再次遇到这种冗长问题）更优雅的方式来编码这种必要的差异性。和单元格类似，我们正在定义数独一行的值域。每个 SQL 条目代表一个可能的数独行。
CREATETABLEsudokurow(c1int,c2int,c3int,c4int,c5int,c6int,c7int,c8int,c9int);INSERTINTOsudokurowSELECTd1.vasc1,d2.vasc2,...d9.vasc9-- 每个单元格FROMcell_domainasd1,cell_domainasd2,...WHEREc1<>c2andc1<>c3and...-- c1 是唯一的andc2<>c3andc2<>c4and...-- c2 是唯一的...andc8<>c9-- c8 和 c9 是唯一的;现在我们有了行，就可以实现一个数独棋盘的表示。由于可能的数独棋盘数量太多（即值域太大），无法具体化，我们将使用一个 SQL 视图来表示数独棋盘的值域。同样，我们将使用成对的差异性约束，这意味着大量的不等式。
CREATEVIEWboardASSELECTr1.c1asc11,r1.c2asc12,......r9.c8asc98,r9.c9asc99FROMsudokurowasr1,sudokurowasr2,...WHERE-- 列值互异c11<>c21andc11<>c31...andc21<>c31andc21<>c41......c19<>c29andc19<>c39...andc29<>c39andc29<>c49...-- 子方块值互异（全部九个）andc11<>c22andc11<>c23......;求解一个特定的数独棋盘就变得和在 “where” 子句中包含初始配置的 select 查询一样简单：
SELECT*FROMboardWHEREc11=1andc22=2and...;在食谱中加入 Zinc
我进行约束编程的首选工具是 Zinc 套件。Minizinc 是一种用于描述约束问题的高级开源语言；其源文件被编译成一种中立但较低级的语言，称为 Flatzinc。然后，Flatzinc 文件可以被众多约束求解器之一读取和求解，因为存在许多潜在的搜索实现方式。打个比方，Minizinc 是源代码，Flatzinc 是虚拟机字节码，而求解器是特定于操作系统的运行时环境。
让我们看看数独如何适应 Minizinc。我们从数独棋盘开始，它由 9x9 个单元格组成，每个单元格的取值范围在整数 1 到 9 之间。
array[1..9, 1..9] of var 1..9: board;接下来，我们添加约束来表示对行和列的限制。注意这比 SQL 实现简洁多少。
constraint forall (row in 1..9) (alldifferent (col in 1..9) (board[row, col])); constraint forall (col in 1..9) (alldifferent (row in 1..9) (board[row, col]));我们还为每个包含互异值的子网格添加约束。下面的描述为了清晰而过于显式——我们可以很容易地使用 for 循环来达到同样的效果。
constraint ( alldifferent (row in 1..3, col in 1..3) (board[row, col]) /\ alldifferent (row in 1..3, col in 4..6) (board[row, col]) /\ alldifferent (row in 1..3, col in 7..9) (board[row, col]) /\ alldifferent (row in 4..6, col in 1..3) (board[row, col]) /\ alldifferent (row in 4..6, col in 4..6) (board[row, col]) /\ alldifferent (row in 4..6, col in 7..9) (board[row, col]) /\ alldifferent (row in 7..9, col in 1..3) (board[row, col]) /\ alldifferent (row in 7..9, col in 4..6) (board[row, col]) /\ alldifferent (row in 7..9, col in 7..9) (board[row, col]) );最后，我们需要为棋盘的初始配置（即我们给定的值）添加一个约束：
constraint ( board[1, 1] = 1 /\ board[2, 2] = 2 /\ ... );去芜存菁
如果你在计算机科学理论上花过任何时间，很可能遇到过 NP 难问题，即其复杂度随输入规模呈指数级（或更糟）增长的任务。不幸的是，这些问题在"现实世界"中非常普遍。你可能需要为共享资源制定最佳时间表，找到两个文档之间的最小必要更改，或者甚至只是解决像上面数独游戏这样的问题。这些问题的变体都是 NP 难的，因此对于大型输入，仅仅检查每个可能的答案并挑选最优的是不可行的。
幸运的是，我们并不总是需要检查所有可能的解来找到最优解。例如，在数独中，许多棋盘选择会产生无效配置——即每个方块、列或行中的数字不唯一。使用约束进行编程意味着将搜索空间限制在那些有效的解决方案上，从而显著减少运行时间。
然而，约束编程环境和库提供的不仅仅是对限制搜索空间的良好隐喻。它们通常还提供非常高效的引擎来搜索可能性空间。考虑我们的数独游戏；每个单元格可以取值的范围取决于同一行、同一列和同一方块中已经已知的单元格。了解一个单元格的潜在取值范围反过来又对其他单元格提供了额外的约束。例如，如果一行中除一个单元格外的所有单元格的取值范围都排除了数字 8，那么我们可以肯定那个例外单元格包含数字 8，无论其取值范围中还有其他什么值。在调整取值范围时的这种来回过程被称为"传播"。
经过足够的传播后，系统会意识到它无法再进一步缩小搜索空间，程序将需要进行猜测。然后，这个猜测会触发新一轮的传播。它会跟踪每个"决策"，以便能够撤销它所做的一系列猜测并尝试不同的选择，始终寻求最优解。决策最终可能导致无效或"失败"的配置，这指示何时需要撤销决策堆栈，并且某些搜索策略（例如二分搜索）可能以更高效的顺序进行"猜测"。
请注意，解决方案既是正确的也是最优的。我们只是通过丢弃无效配置来节省工作量（从而节省时间），而不是通过丢弃有效解。如果我们没有提供足够的约束，搜索空间将仍然巨大得无法计算。我们描述的约束越多，需要执行的工作就越少，我们找到解决方案的速度也就越快。你也可以想象，如果我们将搜索空间限制得比问题的要求更严格，我们可以快速地找到次优解。
实现说明
要在你的应用程序中使用 Minizinc，很可能需要你的应用程序编写一个 Minizinc 源文件。然后它可以调用一个一次性的编译器/执行器并读取结果，这些结果通常以 JSON 形式读取。这种方法在开发期间特别有吸引力，因为直接访问 minizinc 输入文件和编译器将使调试更简单。对于生产应用程序，你可能希望切换到较低级别的库（例如 Gecode）以获得性能提升，但 Minizinc 对于开发和学习约束编程基础知识非常棒。实际上有一个 Flatzinc 的 Gecode 实现，这意味着你只会受到编译开销的影响。
资源
- SQL 数独初始化脚本
- 完整的 Minizinc 数独脚本
- Minizinc: 官网, 教程
- Coursera 的离散优化课程 (来自 Pascal Van Hentenryck)
- Gecode 的 flatzinc 插件