Skip to content

Instantly share code, notes, and snippets.

@jbum
Created May 27, 2016 16:57
Show Gist options
  • Save jbum/4b39259edd3dc903e0243d76cd125502 to your computer and use it in GitHub Desktop.
Save jbum/4b39259edd3dc903e0243d76cd125502 to your computer and use it in GitHub Desktop.
# KenKen (aka Calcudoku, Mathdoku, Kendoku, Inkies) - contributed by Jim Bumgardner
# https://en.wikipedia.org/wiki/KenKen
#
# Puzzles sourced from the Inkies collection at Krazydad.com
from Numberjack import *
#
# Ensure that the sum of the segments
# in cc == res
#
bStats = {'cnt':0,'failures':0,'backtracks':0,'walltime':0,'propags':0,'checks':0}
def parsePuzzle(sz,puzz):
(layout,clues) = puzz.split(';')
clues = clues.split(',')
ldict = {}
grid = []
nbrClues = 0
for i in range(sz*sz):
ch = layout[i]
if ch not in ldict:
clue = clues[nbrClues]
op = clue[-1]
val = int(clue[:-1])
cage = [val,op,[]]
nbrClues += 1
ldict[ch] = cage
grid.append(cage)
y = (i/sz)+1
x = (i%sz)+1
ldict[ch][2].append([y,x])
return grid
# problem = [
# [11, '+', [[1, 1], [2, 1]]],
# [2, '/', [[1, 2], [1, 3]]],
# [20, '*', [[1, 4], [2, 4]]],
# [6, '-', [[1, 5], [1, 6], [2, 6], [3, 6]]],
# etc...
def solveKenKen(sz,puzz, param):
problem = parsePuzzle(sz,puzz)
num_p = len(problem)
grid = Matrix(sz, sz, 1, sz)
model = Model()
model += [AllDiff(row) for row in grid.row]
model += [AllDiff(col) for col in grid.col]
# calculate the segments
for (res, op, segment) in problem:
cage = [grid[y-1,x-1] for (y,x) in segment]
if op == '+':
model += Sum(cage) == res
elif op == '-':
model += ((cage[0] - cage[1]) == res) | ((cage[1] - cage[0]) == res)
elif op == '*':
# Note: Ideally, I'd prefer to do this:
model += Product(cage) == res
elif op == '/':
model += ((cage[0] * res) == cage[1]) | ((cage[1] * res) == cage[0])
# pass
else:
print "Invalid op",op
solver = model.load(param['solver'])
solver.reset(full=True) # needed to clear from previous solves
solver.setVerbosity(param['verbose'])
solver.startNewSearch()
res = solver.getNextSolution()
outS = ''
# if solver.is_sat():
if res == SAT:
outS = ''.join(map(str, grid.flat))
if param['verbose']:
print "Hit1",outS
res2 = solver.getNextSolution()
if res2 == SAT:
outS = ''.join(map(str, grid.flat))
if param['verbose']:
print "Hit2",outS
return "mult"
else:
return "unsat"
bStats['cnt'] += 1
bStats['failures'] += solver.getFailures()
bStats['backtracks'] += solver.getBacktracks()
bStats['propags'] += solver.getPropags()
bStats['checks'] += solver.getChecks()
bStats['walltime'] += solver.getTime()
return outS
# Test puzzles from the Inkies collection at Krazydad.com
test_puzzles = [
(3,"AABCDBCDD;1-,3*,3*,7+","213321132"), # easy
(3,"AABCDBCDD;3*,1-,6*,6+","132321213"), # hard
(6, 'ABBBBCADEEFCADGHFIJDGHKIJLLMKNOOLMKN;8+,12+,8+,13+,2-,1-,2-,4-,6+,1-,14+,6+,1-,1-,1-', '352146465312134625546231621453213564'),
(6, 'AABBCDEFGGCDEFHICDJFHIKKJFLLLMJNNOOM;7+,3-,13+,14+,1-,11+,3-,3-,2-,11+,1-,12+,2-,5+,8+', '162543524136413265356421235614641352'),
(6, 'ABCDDEABCFFEGGCHIIJKCHLLJKMMNOPPQQNO;2-,2-,17+,3-,8+,1-,7+,2-,7+,3-,2-,2-,6+,1-,8+,4-,5+', '236415412653524361365124641532153246'),
(6, 'AABBCDEAFGCDEFFGHHIJJGKLIMMNKLOOMNKK;13+,1-,2-,2-,6+,11+,13+,1-,4-,2-,17+,4-,9+,7+,6+', '362154146532514623653241231465425316'),
(6, 'ABCDDEABCCFEGGHIFJKKHILJMNOOLPMNQQLP;5+,2-,16*,1-,2/,2/,4*,7+,8+,2-,3/,8*,6+,24*,6*,2-,1-', '234651351462412536625314546123163245'), # easy boom
(6,"ABBCDEAFGCDEHFGIJKHLMIJKNLMOOPNQQRRP;6*,2/,1-,3/,9+,15*,2/,10*,2/,24*,9+,3-,9+,1-,4-,2/,1-,5+","124635632514251463513246346152465321"), # med boom
(6,"ABBCDEAFFCDEGHIJJKGHILMKNHILMONPPPMO;3-,3-,1-,3/,24*,5+,4*,13+,10+,8+,2/,2/,48*,2/,2-,20*","214536532614426351153462361245645123"), # hard boom
(6,"ABCCDDABEEFFGGHHIJKLMIIJKLMNOOPPPNQQ;5+,3-,2/,2/,7+,2-,30*,5+,90*,2/,5+,3/,1-,1-,2-,48*,5*","153624426153561432234561315246642315"), # easy
(6,"AABCDDEEBCFFEGGHHFIJJKKLIMNNOLIMPPOL;2/,2-,4*,3-,36*,80*,2/,1-,15+,7+,3/,6+,20*,2/,4-,9+","125436263145312564534621641253456312"), # easy
(6,"ABCCDEABFGDEHHFGIIJJKLLMNNKOMMNNNOPP;2/,3-,6*,6+,2/,1-,18*,6+,3/,3/,7+,2-,7+,540*,4*,1-","413256245613154362621534536421362145"), # easy
(6,"AABBCDEAFGCDEHFGIIJHKLMMJNKLOPNNQQOP;8+,20*,2/,7+,1-,3/,2/,2-,7+,1-,12*,3/,5+,6*,4*,1-,1-","124536453261361452546123612345235614"), # med
(6,"ABCCDEABCFDEGHCFIJGHKIIJLMKKNNLMKOON;1-,4-,300*,3/,2-,2/,3-,3/,14+,3/,72*,7+,12*,9+,15*","412536356214265143523461134625641352"), # med
(6,"AAABCDEFBBCDEFGBBDHIGJKKHILJMNOOLMMN;72*,144*,2/,9+,3-,2-,1-,3/,7+,1-,5+,3/,40*,2-,6*","436125562413245361154632321546613254"), # hard
(6,"AABBCDEEBFCDGHIFJJGHIKLLMMIKNNOOOOPP;7+,8*,3-,2/,1-,1-,10*,1-,12+,3-,5+,2/,3/,24*,48*,8+","612453341526253641564312135264426135"), # hard
]
if __name__ == "__main__":
import time
default = {'solver': 'Mistral', 'verbose': 0}
param = input(default)
st = time.time()
nbrCorrect = 0
nbrPuzzles = 0
nbrMults = 0
for (sz,puzz,stored_answer) in test_puzzles:
# print sz,puzz,ans
nbrPuzzles += 1
last_answer = solveKenKen(sz,puzz,param)
if param['verbose']:
print last_answer
if last_answer == stored_answer:
nbrCorrect += 1
elif last_answer == 'mult':
nbrMults += 1
print "%s %d/%d (%d mults) %.2f secs" % (param['solver'], nbrCorrect, nbrPuzzles, nbrMults, time.time()-st),bStats
# Mistral 0/9 (0 mults) 0.04 secs {'propags': 0, 'cnt': 0, 'backtracks': 0, 'failures': 0, 'checks': 0, 'walltime': 0}
# Mistral2 9/9 (0 mults) 0.05 secs {'propags': 18683, 'cnt': 9, 'backtracks': 340, 'failures': 340, 'checks': 18683, 'walltime': 0.0}
# MiniSat 0/9 (9 mults) 0.19 secs {'propags': 0, 'cnt': 0, 'backtracks': 0, 'failures': 0, 'checks': 0, 'walltime': 0}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment