SMTソルバーを用いた数独の解

sudoku.py

import numpy as np
from z3 import *

# 例題
board_spec = '''
       39
     1  5
  3 5 8  
  8 9   6
 7   2   
1  4     
  9 8  5 
 2    6  
4  7     '''

board_spec = np.array([list(row) for row in board_spec.split('\n')[1:]])
board = np.array([Int(f'v{i}') for i in range(9*9)]).reshape((9, 9))

def distinct(M):
    solver.add(Distinct(M.flatten().tolist()))               # 「相異なる」制約

solver = Solver()                                            # SMTソルバーの設定
for ch, v in zip(board_spec.flatten(), board.flatten()):
    solver.add(And(1 <= v, v <= 9) if ch == ' ' else v == int(ch))
for i in range(9):
    distinct(board[i,:])                                     # 各行の値は相異なる
    distinct(board[:,i])                                     # 各列の値は相異なる
    distinct(board[3*(i//3):3*(i//3+1), 3*(i%3):3*(i%3+1)])  # 各3x3ブロックの値は相異なる

if solver.check() == sat:
    model = solver.model()
    print(np.frompyfunc(lambda v: model[v], 1, 1)(board))

@fuloru169さんのQiitaの記事を参考にさせていただきました。

実行結果は以下です。実行時間のほとんどはライブラリの読み込み時間のような気がします。

[[7 5 1 8 4 6 2 3 9]
 [8 9 2 3 7 1 4 6 5]
 [6 4 3 2 5 9 8 7 1]
 [2 3 8 1 9 7 5 4 6]
 [9 7 4 5 6 2 3 1 8]
 [1 6 5 4 3 8 9 2 7]
 [3 1 9 6 8 4 7 5 2]
 [5 2 7 9 1 3 6 8 4]
 [4 8 6 7 2 5 1 9 3]]