Skip to content

Instantly share code, notes, and snippets.

@sureshvv
Created April 20, 2020 15:02
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save sureshvv/d737bee93bc2dc49acf09251e6863b66 to your computer and use it in GitHub Desktop.
Save sureshvv/d737bee93bc2dc49acf09251e6863b66 to your computer and use it in GitHub Desktop.
sudoku.py
from copy import deepcopy
from types import SimpleNamespace
from hypothesis import note, settings
from hypothesis.stateful import (invariant, precondition, rule,
RuleBasedStateMachine)
DIM = 3
SIZE = DIM * DIM
class GuessError(Exception):
pass
class Sudoku2(RuleBasedStateMachine):
def __init__(self):
super().__init__()
self.possibilities = []
self.board = []
for i in range(SIZE):
self.board.append([])
self.possibilities.append([])
for i in range(SIZE):
for j in range(SIZE):
self.board[i].append(0)
self.possibilities[i].append([])
self.start()
self.setup()
def printb(self):
for i in range(SIZE):
print(self.possibilities[i])
def start(self):
self.board[0] = [0, 5, 0, 9, 0, 0, 0, 0, 0]
self.board[1] = [0, 0, 9, 0, 0, 0, 0, 3, 0]
self.board[2] = [0, 0, 0, 0, 1, 0, 0, 4, 0]
self.board[3] = [6, 0, 0, 0, 0, 0, 0, 0, 0]
self.board[4] = [8, 0, 0, 4, 0, 0, 0, 6, 0]
self.board[5] = [7, 0, 0, 5, 0, 0, 9, 2, 8]
self.board[6] = [9, 0, 6, 0, 3, 2, 1, 0, 0]
self.board[7] = [0, 2, 0, 0, 0, 5, 0, 0, 0]
self.board[8] = [0, 0, 0, 0, 0, 0, 0, 0, 4]
def setup(self):
self.progress = True
self.guess_error = False
self.context = []
for i in range(SIZE):
for j in range(SIZE):
if not self.board[i][j]:
self.possibilities[i][j] = list(range(1, SIZE + 1))
else:
self.possibilities[i][j] = [self.board[i][j]]
def check4(self, pos):
# print('+++++ check4 ++++++', pos)
# self.print_board()
for i in range(SIZE):
if len(self.possibilities[pos[i][0]][pos[i][1]]) == 1:
target = self.possibilities[pos[i][0]][pos[i][1]][0]
for j in range(SIZE):
if i == j:
continue
if target in self.possibilities[pos[j][0]][pos[j][1]]:
# print('--- removing %d from %d,%d' % (target, pos[j][0], pos[j][1]))
self.possibilities[pos[j][0]][pos[j][1]].remove(target)
if len(self.possibilities[pos[j][0]][pos[j][1]]) <= 0:
raise GuessError
self.progress = True
for j in range(1, SIZE + 1):
count = 0
for i in range(SIZE):
if j in self.possibilities[pos[i][0]][pos[i][1]]:
count += 1
if count <= 0:
raise GuessError
if count == 1:
for i in range(SIZE):
if len(self.possibilities[pos[i][0]][pos[i][1]]) > 1 and \
j in self.possibilities[pos[i][0]][pos[i][1]]:
self.possibilities[pos[i][0]][pos[i][1]] = [j]
# print('--- setting to %d from %d,%d' % (j, pos[i][0], pos[i][1]))
self.progress = True
# self.print_board()
@precondition(lambda self: not self.progress and self.guess_error)
@rule()
def reguess(self):
# go to next guess on stack
print('+++++ RE-GUESS ++++++')
# self.print_board()
last_context = self.context[-1]
while last_context.guess <= 0:
print('+++++ LOOPING IN RE-GUESS ++++++')
self.context.pop()
last_context = self.context[-1]
self.possibilities = deepcopy(last_context.data)
pos = last_context.pos
i = pos // SIZE
j = pos % SIZE
last_context.guess -= 1
# print('--- reguess %d of %s' % (last_context.guess, self.possibilities[i][j]))
self.possibilities[i][j] = [self.possibilities[i][j][last_context.guess]]
self.progress = True
self.guess_error = False
# self.print_board()
def get_next_pos(self, cur_pos):
while True:
cur_pos += 1
i = cur_pos // SIZE
j = cur_pos % SIZE
if i >= SIZE:
assert False
len1 = len(self.possibilities[i][j])
if len1 > 1:
return cur_pos, len1 - 1
@precondition(lambda self: not self.progress and not self.guess_error)
@rule()
def guess(self):
# import pdb; pdb.set_trace()
print('+++++ GUESS ++++++')
# self.print_board()
# push new guess on stack
# check if last guess
# if so, pop from stack and move on to next guess
last_pos = self.context[-1].pos if self.context else 0
pos, guess = self.get_next_pos(last_pos)
i = pos // SIZE
j = pos % SIZE
data = deepcopy(self.possibilities)
# print('--- guess %d of %s' % (guess, self.possibilities[i][j]))
self.possibilities[i][j] = [self.possibilities[i][j][guess]]
new_context = SimpleNamespace()
new_context.pos = pos
new_context.guess = guess
new_context.data = data
self.context.append(new_context)
self.progress = True
# self.print_board()
@precondition(lambda self: self.progress)
@rule()
def reduce(self):
self.print_board()
while self.progress:
self.progress = False
try:
for y in range(SIZE):
self.check4([(y, x) for x in range(SIZE)])
self.check4([(x, y) for x in range(SIZE)])
for z1 in range(DIM):
for z2 in range(DIM):
sq1 = [(x + z1 * DIM, y + z2 * DIM) for x in range(
DIM) for y in range(DIM)]
self.check4(sq1)
# self.print_board()
except GuessError:
self.progress = False
self.guess_error = True
items = [y for x in self.possibilities for y in x if len(y) > 1]
if not items:
break
self.print_board()
@invariant()
def all_done(self):
items = [y for x in self.possibilities for y in x if len(y) > 1]
if len(items) == 0:
self.write_notes()
assert False
def print_board(self):
for x in self.possibilities:
for y in range(SIZE):
print(' ' if len(x[y]) > 1 else x[y][0], end=' ')
print(' ')
print('----------------')
def write_notes(self):
for x in self.possibilities:
note([x[y][0] for y in range(SIZE)])
# The default of 200 is sometimes not enough for Hypothesis to find
# a falsifying example.
Sudoku2.TestCase.settings = settings(stateful_step_count=9999999)
DieHardTest = Sudoku2.TestCase
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment