KenKen.py

# 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}