用10分钟写个程序解数独游戏

瞎扯的前言：

作为一个数独爱好者，在某某文摘还流行的中学时代，我课上没事就喜欢翻到最后几页做起里面的数独游戏。今天偶然发现一个在线数独游戏网站，重温当年玩了几局后，突发奇想决定写一个小程序来求解数独问题。在ta的帮助下，我这个经常智商下线的玩家也得以在骨灰级难度的游戏中排到top 4%.

开始之前的准备：

本文用到的建模语言是MiniZinc（需要到官网下载它的IDE），一种约束建模语言（Constraint Modeling Language）.  致力于解决优化问题（optimization problem）和满足问题（satisfaction problem）。而且， 有了它，只需要把问题准确的表述出来，我们自己不必知道问题怎么解，minizinc自然会给出答案。是不是很神奇！话不多说，直接上手吧。

源码摸这里。

Action：

数独游戏，其实就是一个satisfaction problem. 我们要做的，就是：

1. 把游戏规则描述清楚
2. 设计输入数据的格式
3. 愉快的开始“作弊”

1. 游戏规则的描述

典型的数独游戏会给出类似上边这样一个方阵，我们需要从1~9中选出合适的数字填满空白的格子，使整个9×9方阵和9个3×3小方阵同时满足：

每行每列的数字都不重复。

我们接下来用几个约束条件（constraint）来描述这个规则。

先用二维数组grid表示这个方阵：

set of int: size = 1..9;

array[size, size] of var 1..9: grid;

size是包含1~9的正数的集合，grid是要求解的二维数组，每个值的范围也是在1~9之间。

开始写第一个constraint：

include "alldifferent.mzn";

constraint forall (i in size) (alldifferent([grid[i, j] | j in size]));

forall相当于数学符号∀。”alldifferent.mzn”是MiniZinc众多global constraint中的一个，可以理解为编程语言中的库。第二行的constraint其实就是把数学表达式翻译成minizinc能看懂的话，说人话就是：

对所有的i，都有grid[i, 1], grid[i, 2], … , grid[i, 9]两两不相等。也就是方阵每一行的9个数字互不相等。

类似的可以对每一列的数字不相等写出另一个constraint。

表达完大方阵的约束条件，再来看小方阵。现在需要翻译的数学表达式有点不一样了：

对3×3矩阵中的所有i, j, grid[i, j]都不相等。

以左上角的3×3矩阵为例：

constraint alldifferent([grid[i, j] | i in 1..3, j in 1..3]);

对其他8个3×3矩阵，按照相同格式书写即可，只需要把i，j对应的范围做修改。

PS: 尽管上述constraint过于冗长，但我们为了快速实现，暂不考虑这方面的优化。

2. 设计输入数据的格式

完成了对规则的描述之后，接下来看如何把一个题目中的数据读进来。

我们可以在模型里再增加一个二维数组input_grid来存储题目中的已知数据。题目中的空白处在input_grid中用1~9以外的数表示，这里用0为例。

array[size, size] of 0..9: input_grid;

input_grid的值在数据文件（.dzn）中书写。有了这个数据，把其中有效部分（即非零部分的数据）赋给grid矩阵就实现了数据的读入。

tips: <->符号是“等价于”的意思。

constraint forall(i in size, j in size)(input_grid[i, j] > 0  <->  input_grid[i, j] = grid[i, j]);

3. 愉快的开始“作弊”

最后再加上

solve satisfy;

表明这是一个求解satisfaction的问题。并对输出矩阵的格式做一些处理，就大功告成了！

怎么用呢？

很简单，把数据存在一个新建的.dzn文件中。

然后run model文件“sudoku.mzn”, 选择加载的dzn数据文件。就可以看到minizinc为你解出的答案了。

点这里可以查看完整代码。

严肃的总结：

写出程序之后我兴奋的回到在线sudoku puzzles网站，试玩了高难度级别，直接排到了top 4%。要不是手残打字老出错，兴许可以到3%以内。然而玩了两把我就不想玩了，我现在感觉把一个喜欢的游戏给毁了。可能我再也不会认认真真玩数独了。。。

传送门：

对MiniZinc有兴趣的朋友可以读下官方的教程：A MiniZinc Tutorial， 探索更多的玩法。