Created
December 11, 2019 06:55
-
-
Save bisco/22249b20dbce0d8315603eecf9061076 to your computer and use it in GitHub Desktop.
z3を使って数独を解くソースコード
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/usr/bin/env python3 | |
from z3 import * | |
#---------------------------# | |
# const | |
#---------------------------# | |
sudoku = [] | |
solver = Solver() | |
#---------------------------# | |
def add_rules(n): | |
for r in range(n): | |
for c in range(n): | |
# 各マスには1~nのいずれかの数値が入る | |
solver.add(1 <= sudoku[r][c], sudoku[r][c] <= n) | |
# 同じ行のマスにはそれぞれ異なる数値が入る | |
solver.add(Distinct(sudoku[r])) | |
# 同じ列のマスにはそれぞれ異なる数値が入る | |
for c in range(n): | |
solver.add(Distinct([sudoku[r][c] for r in range(n)])) | |
# sqrt(n) x sqrt(n)の同一ブロック内のマスには、それぞれ異なる数値が入る | |
block_len = int(pow(n, 0.5)) | |
for row in range(block_len): | |
for col in range(block_len): | |
d = [] | |
for r in range(block_len): | |
for c in range(block_len): | |
d.append(sudoku[row*block_len + r][col*block_len + c]) | |
solver.add(Distinct(d)) | |
def gen_sudoku_map(n): | |
""" | |
the rule of naming each grid | |
0 1 2 3 ... n-1 | |
a a0 a1 a2 a3 ... an-1 | |
b b0 b1 | |
c c0 | |
d | |
e | |
: | |
""" | |
for row in range(n): | |
sudoku.append([]) | |
r = chr(ord("a") + row) | |
for col in range(n): | |
key = "{}{}".format(r, col) | |
sudoku[row].append(BitVec(key, 8)) | |
def read_sudoku_question(filename): | |
""" | |
file format: | |
delimiter: space | |
unknown_grid: fill 0 | |
""" | |
q = [] | |
with open(filename) as f: | |
row = 0 | |
for line in f: | |
line = line.strip().split() | |
q.append([]) | |
for col, v in enumerate(line): | |
v = int(v.strip()) | |
q[row].append(v) | |
row += 1 | |
return row, q | |
def subst_var_to_const(q): | |
for r, row in enumerate(q): | |
for c, v in enumerate(row): | |
if v != 0: | |
key = "{}{}".format(chr(ord("a") + r), c) | |
sudoku[r][c] = substitute(sudoku[r][c], (sudoku[r][c], BitVecVal(v, 8))) | |
def main(): | |
if len(sys.argv) != 2: | |
print("usage: {} sudoku_question_file".format(sys.argv[0])) | |
sys.exit(1) | |
n, q = read_sudoku_question(sys.argv[1]) | |
gen_sudoku_map(n) | |
subst_var_to_const(q) | |
add_rules(n) | |
if solver.check() == sat: | |
m = solver.model() | |
for r, row in enumerate(q): | |
tmp = [] | |
for c, v in enumerate(row): | |
if v == 0: | |
tmp.append(str(m[sudoku[r][c]])) # modelは辞書みたいに使う | |
else: | |
tmp.append(str(v)) | |
print(" ".join(tmp)) | |
else: | |
print("This sudoku question isn't solvable") | |
if __name__ == "__main__": | |
main() |
Hi, PKHG. Usage and sample input are here.
$ cat input.txt
0 5 0 0 0 1 0 7 0
1 0 0 0 0 2 0 0 0
2 0 7 0 0 4 1 0 0
0 2 0 0 0 0 9 1 6
0 0 5 0 0 0 2 0 0
9 1 6 0 0 0 0 3 0
0 0 1 7 0 0 5 0 3
0 0 0 5 0 0 0 0 1
0 4 0 9 0 0 0 2 0
$ ./sudoku_z3.py input.txt
3 5 4 6 9 1 8 7 2
1 6 9 8 7 2 3 5 4
2 8 7 3 5 4 1 6 9
7 2 8 4 3 5 9 1 6
4 3 5 1 6 9 2 8 7
9 1 6 2 8 7 4 3 5
6 9 1 7 2 8 5 4 3
8 7 2 5 4 3 6 9 1
5 4 3 9 1 6 7 2 8
I used this website to get sudoku questions. You can use sudoku questions generated by it for free.
https://kachikachi.net/numberplace/
This website can't output a sudoku question as a text file, so I copied by hand...
ありがとうございます わたしわ Peter ともします but English or German is much essier to me. The
kachijachi is too difficult for me, just a beginner in 日本語。I an a 祖父78
years young. I did some time ago lots of different types of sudoku using z3
in a jupyter notebook (Python) and just lately fond it back. That search
braught me to your GIST and had to study first your aproach I had some
contact with people from
microsoft to tell me for example how to find all solutions of the 8 queens
chrss problem using z3. Because I doughted a sodoku of my local newspaper .
so building it into my sudokusolver to find ALL solutions (good ons have
only one)
A nice z3 using solver for scyscraper sudoku was done by me and adding
extra conditions like diagonals too digits 1-9 is finally very easy (found
it back) if you are interested I exported it into HTML and uploaded it to
my site
thanks for your hsndwork 😉 have to try reading kachikachi page
greets Peter
Op do 4 jun. 2020 om 15:57 schreef bisco(or nbisco) <
notifications@github.com>
… ***@***.**** commented on this gist.
------------------------------
Hi, PKHG. Usage and sample input are here.
$ cat input.txt
0 5 0 0 0 1 0 7 0
1 0 0 0 0 2 0 0 0
2 0 7 0 0 4 1 0 0
0 2 0 0 0 0 9 1 6
0 0 5 0 0 0 2 0 0
9 1 6 0 0 0 0 3 0
0 0 1 7 0 0 5 0 3
0 0 0 5 0 0 0 0 1
0 4 0 9 0 0 0 2 0
$ ./sudoku_z3.py input.txt
3 5 4 6 9 1 8 7 2
1 6 9 8 7 2 3 5 4
2 8 7 3 5 4 1 6 9
7 2 8 4 3 5 9 1 6
4 3 5 1 6 9 2 8 7
9 1 6 2 8 7 4 3 5
6 9 1 7 2 8 5 4 3
8 7 2 5 4 3 6 9 1
5 4 3 9 1 6 7 2 8
I used this website to get sudoku questions. You can use sudoku questions
generated by it for free.
https://kachikachi.net/numberplace/
This website can't output a sudoku question as a text file, so I copied by
hand...
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<https://gist.github.com/22249b20dbce0d8315603eecf9061076#gistcomment-3329600>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AAH6355C74DFM4EMMFXX5WTRU6R6HANCNFSM4NRKSPRQ>
.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Looks interesting, need an example input file or how to get
Please let me know (arigatou gozaimasu)