hidatoTest.py

# Hidato
#
# Sample Hidato Solver - Jim Bumgardner

from Numberjack import *

def get_neighbors(idx, width, height): # get list of indices of neighbor cells
    cx = idx % width
    cy = idx // width
    nebs = []
    for y in (-1,0,1):
        for x in (-1,0,1):
            if y == 0 and x == 0:
                continue
            (nx,ny) = (cx+x,cy+y)
            if nx >= 0 and nx < width and ny >= 0 and ny < height:
                nebs.append(ny*width + nx)
    return nebs

def build_legal_pairs(width,  height):
    tups = []
    nbr_cells = width*height
    for i in xrange(nbr_cells):
        for j in get_neighbors(i, width, height):
            tups.append((i,j))
    return tups


def solve(param, puzz):

    (width,height,givens) = (puzz[0][0], puzz[0][1], puzz[1])
    nbr_cells = width*height
    positions = VarArray(nbr_cells, nbr_cells)
    model = Model()
    model += AllDiff(positions)
    for n,v in enumerate(givens):
        if v != 0:
            model += (positions[v-1] == n)

    close_tuples = build_legal_pairs(width, height)
    for k in xrange(nbr_cells - 1):
      model += Table((positions[k], positions[k + 1]), close_tuples, type='support')

    solver = model.load(param['solver'])
    solver.setVerbosity(param['verbose'])

    if param['timeout'] > 0:
        solver.setTimeLimit(param['timeout'])  # enable timeout to segfault...

    solver.startNewSearch()
    res = solver.getNextSolution()
    if res == SAT:
        answer = [0 for i in xrange(nbr_cells)]
        for i in xrange(nbr_cells):
            answer[ positions[i].get_value() ] = i+1
        return ','.join(map(str,answer))
    elif res == 4:
        return "timeout"
    elif res == UNSAT:
        return "no answer"
    elif res == UNKNOWN:
        return "unknown"
    else:
        print "UNKNOWN RES: ",res

examplepuzzles = (

 ( # easier puzzle, 1 solution
    (7,7),
    (0,0,0,0,0,0,0,
     0,0,27,47,48,49,0,
     25,0,0,0,44,15,0,
     29,30,0,43,0,0,0,
     0,0,0,0,40,0,0,
     0,0,0,4,0,0,1,
     0,36,6,0,0,0,0)
    ),
  ( # another easier puzzle
     (7,7),
     (0,6,7,8,0,0,0,
      0,0,0,0,0,12,0,
      0,0,0,19,18,17,0,
      0,0,0,0,16,0,0,
      30,0,0,1,0,0,0,
      32,33,49,37,0,46,0,
      0,0,0,0,45,0,0)
  ),
  ( # pathological puzzle (multiple solutions, but hard to find one)
    (7,7),
    (0,0,0,0,0,0,0,
    0,0,0,0,0,0,0,
    0,0,0,0,0,0,0,
    0,0,0,0,0,0,25,
    0,0,0,1,0,0,0,
    0,0,49,0,0,0,0,
    0,0,0,0,0,0,0)
  )
)

if __name__ == '__main__':
    default = {'solver': 'Mistral', 'verbose': 0, 'timeout': 10}
    param = input(default)
    for n,puzz in enumerate(examplepuzzles):
      print "example %d:" % (n+1),solve(param, puzz)