Z3Py 例題 グラフ彩色問題

問題

以下のグラフの各頂点に 1 から 3 の数を割り当て、隣接する頂点の異なるようにせよ。

回答

example_graph_coloring.py

from z3 import *

V = [Int('v%s' % i) for i in range(1, 5)]
edges = [[1, 2], [1, 3], [2, 3], [2, 4], [3, 4]]

s = Solver()
s.add([And(1 <= V[i], V[i] <= 3) for i in range(4)])
for x, y in edges:
    s.add(V[x-1] != V[y-1])

print(s.check())
print(s.model())

出力

sat
[v3 = 2, v1 = 3, v2 = 1, v4 = 3]

解説

s.add(V[x-1] != V[y-1]) edge（辺）がつながっているノード間が異なるという制約をつける。

他の例題

Z3Py個人的ポータル へ