# Boston Key Party: Graph 3-coloring with SAT solvers

The Boston Key Party was held between 4th and 6th of March 2016. A few colleagues of mine attended this event and asked for help with one particular problem:

Given a graph with 683 vertices and 1253 edges. Assign one of three colors to each vertex. No edge must connect two vertices of the same color.

Graph 3-coloring is a classic example of an NP-complete problem. So a SAT solver might be suitable for it as far as more efficient algorithms are not known.

Let’s solve this problem with an approach similar to an implementation I use in my master thesis: Generate the CNF using python, let a SAT solver do the hard work and parse the solver’s result back to python and print the assignment of colors to vertices.

The boolean logic is really simple: Every vertex gets assigned three boolean variables. We add the following constraints:

• Only one of three variables can be true.
• For every edge (s, t) we look up the corresponding colors for s and t: r1,g1,b1 and r2,g2,b2. We claim not both r1 and r2 can be true. Not both g1 and g2 can be true. Not both b1 and b2 can be true.

In code it looks like this:

def oneof3(w, a, b, c):

def notboth(w, a, b):

# constraints for colors of one vertex
for v, (red, green, blue) in graph.vertices.items():
oneof3(w, red, green, blue)

# constraint for edges
for (src, dst) in graph.edges:
r1, g1, b1 = graph.vertices[src]
r2, g2, b2 = graph.vertices[dst]
notboth(w, r1, r2)
notboth(w, g1, g2)
notboth(w, b1, b2)

The final source code looked like this (you need to adjust the path to the SAT solver executable; you should use lingeling):

#!/usr/bin/env python3

import re
import os
import sys
import logging
import tempfile
import itertools
import subprocess

# the output format is expected to be compatible with lingeling
SATSOLVER_EXECUTABLE = '/opt/lingeling-bal-2293bef-151109/lingeling'
SATSOLVER_TIMEOUT = None  # or specify an integer in seconds
VERTICES = 683

class Graph:
def __init__(self, nb_vertices):
self.edges = set()
self.nb_vertices = nb_vertices
self.vertices = {k: (3 * k + 1, 3 * k + 2, 3 * k + 3)
for k in range(nb_vertices)}

"""Read edges from a file containing '{src} {dest}' lines"""
with open(filepath) as fd:
for line in fd:
if line.startswith('#'):
continue
src, dst = [int(v) for v in line.split()]
assert 0 <= src < self.nb_vertices \
and 0 <= dst < self.nb_vertices, "vertex number invalid"

def get_assignment(self, model: set):
"""Given a set of positive or negative boolean variables,
return a dictionary assigning 1, 2 or 3 to every vertex
"""
ass = {}
for v, (r, g, b) in self.vertices.items():
assert (r in model) ^ (g in model) ^ (b in model)
assert (r not in model) | (g not in model) | (b not in model)
ass[v] = {r in model: 1, g in model: 2, b in model: 3}[True]
return ass

# storage/writer for CNF data

class CnfStorage:
def __init__(self, fd):
self.fd = fd
self.clauses = set()
self.nbvars = 0

self.nbvars = max(self.nbvars, max([abs(v) for v in ints]))

def finish(self):
self.fd.write('p cnf {} {}\n'.format(self.nbvars, len(self.clauses)))
for clause in self.clauses:
self.fd.write(' '.join([str(i) for i in clause]) + ' 0\n')
self.fd.flush()

# CNF primitives
#   Related: http://lukas-prokop.at/tools/truthtable/

def oneof3(w, a, b, c):

def notboth(w, a, b):

# constraints for colors of one vertex
for v, (red, green, blue) in graph.vertices.items():
oneof3(w, red, green, blue)

# constraint for edges
for (src, dst) in graph.edges:
r1, g1, b1 = graph.vertices[src]
r2, g2, b2 = graph.vertices[dst]
notboth(w, r1, r2)
notboth(w, g1, g2)
notboth(w, b1, b2)

# run the SAT solver

def run_solver(filepath):
"""Run SAT solver as subprocess. Return stdout"""
proc = subprocess.Popen(
[SATSOLVER_EXECUTABLE, filepath],
stdout=subprocess.PIPE, stderr=subprocess.PIPE)

try:
outs, errs = proc.communicate(timeout=SATSOLVER_TIMEOUT)
out = outs.decode('ascii')
except subprocess.TimeoutExpired:
proc.kill()
outs, errs = proc.communicate()
out = errs.decode('ascii')

if proc.returncode == 20:
raise RuntimeError('SAT solver returned UNSATisfiability')
if proc.returncode != 10:
errmsg = 'SAT solver returned error code {}: {}'
raise RuntimeError(errmsg.format(proc.returncode, errs))
return out

def interpret_output(out):
"""Read a model (set of positive/negative integers) from stdout"""
model = []
logging.debug(out)

something = False
for line in out.splitlines():
if line.startswith("v "):
matches = map(int, re.findall(" (-?\d+)", line))
something = True
for match in matches:
if match == 0:
# trailing zero
continue
assert -match not in model
model.append(match)

if not something:
raise RuntimeError("Model empty - most likely the SAT solver " +
"output is incompatible with lingeling")

return tuple(model)

if __name__ == '__main__':
if len(sys.argv) != 2:
print('usage: ./graph-3-coloring.py <edges.txt>')
sys.exit(1)

fd, filepath = tempfile.mkstemp(prefix='graph-3-coloring')

try:
# generate graph
graph = Graph(VERTICES)

# store CNF
w = CnfStorage(os.fdopen(fd, mode='w', encoding='ascii'))
w.finish()
logging.info("Finished generating CNF file")

# run SAT solver
out = run_solver(filepath)
model = interpret_output(out)
assignment = graph.get_assignment(model)

# print result
for vertex, color in assignment.items():
print('{}: {}'.format(vertex, color))
finally: