Z3Py 例題 巡回問題 - Qiita

from z3 import * map = [ [0, 2, 3, 1, 0, 0], [2, 0, 0, 2, 2, 4], [3, 0, 0, 2, 2, 3], [1, 2, 2, 0, 2, 0], [0, 2, 2, 2, 0, 1], [0, 4, 3, 0, 1, 0] ] for total_cost in range(24): t_max = 7 T = [Int("T%s" % i) for i in range(t_max)] f = Function('f', IntSort(), IntSort(), IntSort()) s = Solver() s.add([And(1 <= T[i], T[i] <= 6) for i in range(len(T))]) for i in range(6): for j in range(6): s.add(f(i+1,