Commit 293b29cc authored by Cool Fire (HN)'s avatar Cool Fire (HN)

Initial commit

parents
000260701
680070090
190004500
820100040
004602900
050003028
009300074
040050036
703018000
530070000
600195000
098000060
800060003
400803001
700020006
060000280
000419005
000080079
#!/usr/bin/env python3
from z3 import *
print("Using Z3 version: %s" % z3.get_version_string())
# Read and normalize input
inp = open('input.txt').readlines()
for i in range(len(inp)):
inp[i] = list(inp[i].rstrip("\n"))
for j in range(len(inp[i])):
inp[i][j] = int(inp[i][j])
print('Input state:')
print_matrix(inp)
print('')
s = Solver()
# Create playing field
field = []
for x in range(9):
field.append([])
for y in range(9):
field[x].append(Int("field_%s_%s" % (x, y)))
# Add constraints to make each field be some number between 1 and 9
for x in range(9):
for y in range(9):
s.add(And(field[x][y] > 0, field[x][y] < 10))
# Add constraint for rows
for x in range(9):
s.add(Distinct(field[x]))
# Add constraint for cols
for y in range(9):
col = []
for x in range(9):
col.append(field[x][y])
s.add(Distinct(col))
#Add constraints for each 3x3
for xoff in range(3):
for yoff in range(3):
block = []
for x in range(3):
for y in range(3):
block.append(field[xoff * 3 + x][yoff * 3 + y])
s.add(Distinct(block))
# Add constraints provided by input state
for x in range(9):
for y in range(9):
if(inp[x][y] != 0):
s.add(field[x][y] == inp[x][y])
# Solve it and print result
if s.check() == sat:
print('Output state:')
solution = s.model()
r = [ [ solution.evaluate(field[x][y]) for y in range(9) ] for x in range(9) ]
print_matrix(r)
else:
print('Appears to be unsolvable. Check your input.')
#!/usr/bin/env python3
from z3 import *
print("Using Z3 version: %s" % z3.get_version_string())
s = Solver()
print(s.check())
print(s.model())
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment