from z3 import *

distances = [
  [   0, 2451,  713, 1018, 1631, 1374, 2408,  213, 2571,  875, 1420, 2145, 1972], # New York
  [2451,    0, 1745, 1524,  831, 1240,  959, 2596,  403, 1589, 1374,  357,  579], # Los Angeles
  [ 713, 1745,    0,  355,  920,  803, 1737,  851, 1858,  262,  940, 1453, 1260], # Chicago
  [1018, 1524,  355,    0,  700,  862, 1395, 1123, 1584,  466, 1056, 1280,  987], # Minneapolis
  [1631,  831,  920,  700,    0,  663, 1021, 1769,  949,  796,  879,  586,  371], # Denver
  [1374, 1240,  803,  862,  663,    0, 1681, 1551, 1765,  547,  225,  887,  999], # Dallas
  [2408,  959, 1737, 1395, 1021, 1681,    0, 2493,  678, 1724, 1891, 1114,  701], # Seattle
  [ 213, 2596,  851, 1123, 1769, 1551, 2493,    0, 2699, 1038, 1605, 2300, 2099], # Boston
  [2571,  403, 1858, 1584,  949, 1765,  678, 2699,    0, 1744, 1645,  653,  600], # San Francisco
  [ 875, 1589,  262,  466,  796,  547, 1724, 1038, 1744,    0,  679, 1272, 1162], # St. Louis
  [1420, 1374,  940, 1056,  879,  225, 1891, 1605, 1645,  679,    0, 1017, 1200], # Houston
  [2145,  357, 1453, 1280,  586,  887, 1114, 2300,  653, 1272, 1017,    0,  504], # Phoenix
  [1972,  579, 1260,  987,  371,  999,  701, 2099,  600, 1162,  1200,  504,   0]] # Salt Lake City

vs = [ Int("city" + str(i)) for i in range(0,13)]

solver = Solver()

def distance (x,y):
  global distances
  d = 999999
  for i in range (0,13):
    for j in range (0,13):
      if i != j: # make formula a bit smaller
        d = If(And(x == i, y == j), distances[i][j], d)
  return d

# all the city values must be in [0,12]
for i in range(0,13):
  solver.add(0 <= vs[i], vs[i] <= 12) 

# demand that we visit every city only once
solver.add(Distinct(vs))

# compute a Z3 expression for the overall distance
d = 0
for i in range(0,13):
  d = d + distance(vs[i], vs[(i + 1) % 13])

# bound for overall distance
solver.add (d <= 9000)
# we can fix the starting point of the loop arbitrarily (a bit faster)
solver.add(vs[0] == 0)

result = solver.check()

if result == z3.sat:
  model = solver.model()
  print model
  print "Overall distance:", model.eval(d)