hidatoTest2.py

# Hidato
#
# Sample Hidato Solver - Jim Bumgardner

from Numberjack import *
import random

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.reset(full=True)
    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 = (
  ( # causes segfault (has 1 valid solution)
    (7,7),
    (24, 23, 0, 21, 0, 0, 18, 
     0, 44, 43, 42, 41, 17, 0, 
     45, 0, 0, 0, 39, 15, 0, 
     0, 28, 0, 38, 37, 13, 0, 
     0, 30, 31, 0, 0, 11, 10, 
     48, 0, 0, 5, 0, 7, 0, 
     49, 0, 34, 0, 4, 1, 0)
  ),
 ( # 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, 1 solution
     (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)
    random.seed(2)
    for n,puzz in enumerate(examplepuzzles):
      print "example %d:" % (n+1),solve(param, puzz)