3-color.py

from z3.z3 import *

s = Solver()

V = 683
vs = []
for v in range(1, V + 1):
    vs.append(Int("v%03d" % v))
    s.add(vs[-1] >= 1)
    s.add(vs[-1] <= 3)

for line in open("graph.txt"):
    if not line.strip():
        continue
    a, b = map(int, line.strip().split())
    s.add(vs[a] != vs[b])

s.check()
model = s.model()
for v in sorted(model):
    print "v[%s] = %s" % (str(v)[1:], model[v])