Z3Py　例題　巡回問題

11598 ワード
Z3 SAT Python Python テキストリンク

問題

以下の都市の集合と各2都市間の移動コストが与えられたとき、全ての都市をちょうど一度ずつ巡り出発地に戻る巡回路のうちで総移動コストが最小のものを求めろ。

回答

example_traveling_salesman.py
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, j+1) == map[i][j])

    for i in range(len(T)-1):
        s.add(f(T[i], T[i+1]) > 0)

    s.add([Distinct([T[i] for i in range(t_max-1)])])

    s.add(T[0] == 1)
    s.add(T[-1] == 1)

    s.add(Sum([f(T[i], T[i+1]) for i in range(t_max-1)]) < total_cost)

    print("total_cost=" + str(total_cost) + ":")
    print(s.check())
    if s.check() == sat:
        break

m = s.model()
for i in range(len(T)):
    print('T['+str(i)+']='+str(m[T[i]]))

route_cost = [map[m[T[i]].as_long()-1][m[T[i+1]].as_long()-1]
              for i in range(t_max-1)]

print(route_cost, sum(route_cost))

出力

total_cost=0:
unsat
total_cost=1:
unsat

～中略～

total_cost=11:
unsat
total_cost=12:
sat
T[0]=1
T[1]=2
T[2]=5
T[3]=6
T[4]=3
T[5]=4
T[6]=1
[2, 2, 1, 3, 2, 1] 11

解説

基本戦略はハノイの塔と同じ。初期状態から最終状態への一連の遷移状態が成立していることを確認する。
さらに、遷移コストの合計が〇以下とし、〇をすこしずつ大きくしていき、成立する解を求めることで、最小コストの経路を探索する。

MapはTrue、Falseではなく、各都市間の移動コストとし、0は移動できないと定義した。

他の例題

Z3Py個人的ポータル へ