You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 

53 lines
1.6 KiB

# coding: utf-8
import os, sys
from z3 import *
# get the playground information
if len(sys.argv) != 2:
print("Usage: python3 square.py <test-file>")
sys.exit(0)
with open(sys.argv[1]) as f:
playground = f.read()
rows = playground.strip().split("\n")
playground = [[None if x == "_" else int(x) for x in r.split()] for r in rows]
# get the playground size
size_y = len(playground)
assert(size_y != 0)
size_x = len(playground[0])
assert(size_x != 0)
assert(size_x == size_y)
#################################### Square ####################################
# create the solver
solver = Solver()
numbers = [[None for _j in range(size_x)] for _j in range(size_y)]
# TODO: create an integer variable for each playground cell
# hint: use something like the coordinates as part of the variable name
# TODO: assign each known number the corresponding value from playground
# TODO: declare a variable for the sum of all columns, rows and diagonals
# TODO: enforce that each column sums up to the declared variable
# TODO: enforce that each row sums up to the declared variable
# TODO enforce that both diagonals sum up to the declared variable
# call the solver and check satisfiability
res = solver.check()
if res != sat:
print("unsat")
sys.exit(1)
# print the model
m = solver.model()
for i in range(size_y):
results = []
for j in range(size_x):
num = numbers[i][j]
results.append("_" if num is None else m[num].as_long())
print(("%4s" * len(results)) % tuple(results))
################################################################################