Go to Qiita Advent Calendar 2024 Top
LoginSignup
18
15

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 5 years have passed since last update.

@tkinagaki

[Python]Z3で数独パズルを解く

Last updated at Posted at 2017-09-28

はじめに

初投稿かつn番煎じです

数独について

数独とは

↑こういうやつ - 3×3のブロックに区切られた 9×9の正方形の枠内に1〜9までの数字を入れるペンシルパズルの一つ - ナンプレともいう > https://ja.wikipedia.org/wiki/数独

数独のルール

  • 空いているマスに1〜9のいずれかの数字を入れる
  • 縦・横の各列及び、太線で囲まれた3×3のブロック内に同じ数字が複数入ってはいけない

Z3について

Z3とは

  • Microsoft Research が開発したSMTソルバ
  • MITライセンス

https://github.com/Z3Prover/z3

SMTソルバとは

  • 一階述語論理式の充足可能性を判定してくれる
  • 充足可能(SAT)の場合は充足割り当て解の一つを出力してくれる
  • 充足不可(UNSAT)の場合は出してくれない（そりゃそうだ）

解いてみる

準備

  • githubからz3を拾ってくる

https://github.com/Z3Prover/z3

今回解く問題

[数独問題集上級001](http://www.sudokugame.org/archive/printsudoku.php?nd=2&xh=1)を解いてみます

実装

  • Python3で実装しました
# -*- coding: utf-8 -*-

# z3をインポート
from z3 import *

#全ての変数valは1<=val<=9であることの制約を追加するメソッド
def betweenOneToNine(val,s):
    for i in range(n):
        for j in range(n):
            s.add(1 <= val[i][j], val[i][j] <= n)    

#rowがそれぞれ他と値が異なっていることの制約を追加するメソッド
def distinctRow(val,s):
    for i in range(n):
        tmpList = []
        for j in range(n):
            tmpList.append(val[i][j])
        s.add(Distinct(tmpList))

#columnがそれぞれ他と値が異なっていることの制約を追加するメソッド
def distinctColumn(val,s):
    for i in range(n):
        tmpList = []
        for j in range(n):
            tmpList.append(val[j][i])
        s.add(Distinct(tmpList))

#ブロックの中身がそれぞれ他と値がことなっていることの制約を追加するメソッド
def distinctBlock(val,s):
    for k in range(3):
        for l in range(3):
            tmpList = []
            for i in range(3):
                for j in range(3):
                    tmpList.append(val[3*k+i][3*l+j])
            s.add(Distinct(tmpList))

#あるマス目に任意の数値をセットすることの制約を追加するメソッド
def setNum(val,s,x,y,num):
    s.add(val[x-1][y-1]==num)

#数独問題集上級001の問題設定の制約を追加するメソッド
#http://www.sudokugame.org/archive/printsudoku.php?nd=2&xh=1
def setProb001(val,s):
    setNum(val,s,2,6,1)
    setNum(val,s,2,8,8)
    setNum(val,s,3,1,6)
    setNum(val,s,3,2,4)
    setNum(val,s,3,7,7)
    setNum(val,s,4,6,3)
    setNum(val,s,5,3,1)
    setNum(val,s,5,4,8)
    setNum(val,s,5,6,5)
    setNum(val,s,6,1,9)
    setNum(val,s,6,7,4)
    setNum(val,s,6,9,2)
    setNum(val,s,7,6,9)
    setNum(val,s,7,7,3)
    setNum(val,s,7,8,5)
    setNum(val,s,8,1,7)
    setNum(val,s,8,5,6)
    setNum(val,s,9,5,2)            

#n*n個の変数を用意
n = 9
val = [[Int("val[%d,%d]" % (i,j)) for j in range(n)] for i in range(n)]
s = Solver()

#制約を追加
betweenOneToNine(val,s)
distinctRow(val,s)
distinctColumn(val,s)
distinctBlock(val,s)
setProb001(val,s)

#充足可能性を判定、unsatならexit
r = s.check()
if r == sat:
    m = s.model()
    #印字
    for i in range(n):
        for j in range(n):
            print("%d " % m[ val[i][j] ].as_long(), end="")
        print()
else:
    print(r)

解説

だいたいこんな戦略でやりました

  1. 9*9個の整数型の変数valを用意
  2. 全ての変数valにおいて、1≤val≤9
  3. 縦列の９個の変数は全て異なる
  4. 横列の９個の変数は全て異なる
  5. 3*3のブロック内の９個の変数は全て異なる
  6. 初期配置されている変数を入力

1. 9*9個の整数型の変数valを用意

  • 整数型変数を一つ作るのは以下の通り
x = Int("x")
  • 今回の問題を解くには、整数型変数9*9個必要
  • これから制約をつっこんでいくソルバーもここで用意
#n*n個の変数を用意
n = 9
val = [[Int("val[%d,%d]" % (i,j)) for j in range(n)] for i in range(n)]
s = Solver()

2. 全ての変数valにおいて、1≤val≤9

  • ソルバに制約を追加するのは以下の通り
  • この例だと、命題Pと命題Qの積を制約として追加している
s.add(P,Q)
  • 今回の問題を解くには9*9個のval全てが1以上9以下であってほしいので以下の通り
#全ての変数valは1<=val<=9であることの制約を追加するメソッド
def betweenOneToNine(val,s):
    for i in range(n):
        for j in range(n):
            s.add(1 <= val[i][j], val[i][j] <= n)

3. 縦列の９個の変数は全て異なる

  • 複数の式が異なる値を持つことの制約は以下の通り
  • この場合、xとyとzはいずれも異なる値となる
Distinct(x, y, z)
  • 今回の問題を解くには9つの縦列の数字はそれぞれ全て異なっていてほしいので以下の通り
#rowがそれぞれ他と値が異なっていることの制約を追加するメソッド
def distinctRow(val,s):
    for i in range(n):
        tmpList = []
        for j in range(n):
            tmpList.append(val[i][j])
        s.add(Distinct(tmpList))

4. 横列の９個の変数は全て異なる

  • 縦列の時とほぼ一緒
  • 今回の問題を解くには9つの横列の数字はそれぞれ全て異なっていてほしいので以下の通り
#columnがそれぞれ他と値が異なっていることの制約を追加するメソッド
def distinctColumn(val,s):
    for i in range(n):
        tmpList = []
        for j in range(n):
            tmpList.append(val[j][i])
        s.add(Distinct(tmpList))

5. 3*3のブロック内の９個の変数は全て異なる

  • 縦横列の時からちょっと工夫する
  • 今回の問題を解くに9つある3*3ブロック内の数字はそれぞれ全て異なっていてほしいので以下の通り
#ブロックの中身がそれぞれ他と値がことなっていることの制約を追加するメソッド
def distinctBlock(val,s):
    for k in range(3):
        for l in range(3):
            tmpList = []
            for i in range(3):
                for j in range(3):
                    tmpList.append(val[3*k+i][3*l+j])
            s.add(Distinct(tmpList))

6. 初期配置されている変数を入力

  • セッターのようなメソッドを用意しておく
  • 第3,4引数で座標を指定
  • 第5引数で配置する数値を指定
#あるマス目に任意の数値をセットすることの制約を追加するメソッド
def setNum(val,s,x,y,num):
    s.add(val[x-1][y-1]==num)
  • 今回の問題に初期配置されている数値をガツガツ入れていく
  • しんどい
  • もっと賢いやり方をすべき
#数独問題集上級001の問題設定の制約を追加するメソッド
def setProb001(val,s):
    setNum(val,s,2,6,1)
    setNum(val,s,2,8,8)
    setNum(val,s,3,1,6)
    setNum(val,s,3,2,4)
    setNum(val,s,3,7,7)
    setNum(val,s,4,6,3)
    setNum(val,s,5,3,1)
    setNum(val,s,5,4,8)
    setNum(val,s,5,6,5)
    setNum(val,s,6,1,9)
    setNum(val,s,6,7,4)
    setNum(val,s,6,9,2)
    setNum(val,s,7,6,9)
    setNum(val,s,7,7,3)
    setNum(val,s,7,8,5)
    setNum(val,s,8,1,7)
    setNum(val,s,8,5,6)
    setNum(val,s,9,5,2)

結果

  • 解が出力されました
1 8 7 6 3 2 5 4 9
5 9 2 4 7 1 6 8 3
6 4 3 9 5 8 7 2 1
4 7 6 2 9 3 8 1 5
3 2 1 8 4 5 9 7 6
9 5 8 7 1 6 4 3 2
2 6 4 1 8 9 3 5 7
7 1 5 3 6 4 2 9 8
8 3 9 5 2 7 1 6 4

まとめ

  • Z3を使って簡単な論理問題を解きたかったので
  • Pythonで実装しました
  • これで数独パズルの懸賞に応募し放題！
18
15
5

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
18
15

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?