利用google or-tools 求解数独难题

数独是一种常见的智力游戏,它的规则是:在一个9×9的网格内填入81个1至9的数字，要求每一行的数字不能出现重复，每一列的数字不能出现重新,同时在9×9的大网格内又划分为9个3×3的小网格要求每个小网格内的数字也不能出现重复。游戏开始时在大网格内已填入若干个数字,要求游戏的参与者填充剩余的数字如下图所示：

今天我们用google or-tools的建模语言cp_model来破解 手机app上的数独游戏enjoy sudoku上难度级别最高的maelstorm级的数独难题：

在建模之前，我们首先要明确数独游戏的规则，我们只需把游戏规则告诉cp_model，至于如何破解则不需要我们操心,cp_model会帮你搞定一切.再次确认游戏规则：  

1.在9×9的大网格内：每行、每列元素都不能重复。  
2.在3×3的小网格内：所有元素都不能重复。

 

初始化变量

明确了游戏规则后,我们首先要在代码中定义大网格和小网格的尺寸，以及一个待破解的数独网格，其中未填数字的元素我们会用0来代替：

from ortools.sat.python import cp_model
model = cp_model.CpModel()

#小网格尺寸
cell_size = 3
#大网格每行,每列尺寸
line_size = cell_size**2

line = list(range(0, line_size))
cell = list(range(0, cell_size))

#待破解的数独网格
initial_grid = [[2, 8, 1, 0, 0, 0, 0, 0, 0],
                [7, 9, 6, 1, 0, 4, 0, 3, 5],
                [5, 3, 4, 6, 0, 0, 0, 0, 0], 
                [3, 4, 0, 8, 0, 0, 6, 9, 7],
                [8, 1, 0, 7, 0, 6, 0, 5, 0], 
                [6, 7, 0, 0, 0, 0, 0, 8, 1],
                [0, 0, 7, 0, 0, 8, 0, 2, 0], 
                [1, 2, 8, 3, 0, 7, 5, 4, 0],
                [0, 0, 3, 2, 0, 0, 7, 0, 8]]

定义网格变量

接下来我们要定义一个9×9的大网格变量,它用来存储破解完成以后网格内的所有数字,然后对网格变量赋初始值：

#定义存储破解结果的网格变量
grid = {}
for i in line:
    for j in line:
        grid[(i, j)] = model.NewIntVar(1, line_size, 'grid %i %i' % (i, j))  
        
#初始化网格变量
for i in line:
    for j in line:
        if initial_grid[i][j]:
            model.Add(grid[(i, j)] == initial_grid[i][j])  

添加游戏规则

接下来我们要将游戏规则告诉cp_model,并往网格变量中添加游戏规则的约束：

1.行约束： 每行的元素都不一样。
2.列约束: 每列的元素都不一样。
3.cell(小网格)约束: 每个cell内的元素都不一样。

#行约束： 每行的元素都不一样
for i in line:
    model.AddAllDifferent([grid[(i, j)] for j in line])  
    
#列约束: 每列的元素都不一样
for j in line:
    model.AddAllDifferent([grid[(i, j)] for i in line])  
    

#cell约束: 每个cell内的元素都不一样
for i in cell:
    for j in cell:
        one_cell = []
        for di in cell:
            for dj in cell:
                one_cell.append(grid[(i * cell_size + di,
                                      j * cell_size + dj)])

        model.AddAllDifferent(one_cell) 

求解

设定好游戏规则以后,我们就可以舒舒服服的让or-tools来替我们完成剩下的求解过程，就这么简单！最后我们的程序仅耗时3毫秒就破解了这个数独游戏。

%%time
# 求解
solver = cp_model.CpSolver()
status = solver.Solve(model)
if status == cp_model.OPTIMAL:
    for i in line:
        print([int(solver.Value(grid[(i, j)])) for j in line])

参考资料：

以上代码来自于：https://github.com/google/or-tools/blob/master/examples/python/sudoku_sat.py