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):
w.add_clause(a, b, c)
w.add_clause(-a, -b, c)
w.add_clause(-a, b, -c)
w.add_clause(a, -b, -c)
w.add_clause(-a, -b, -c)
def notboth(w, a, b):
w.add_clause(-a, -b)
def add_constraints(graph, w):
# 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)}
def read_edges(self, filepath: str):
"""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"
self.edges.add((src, dst))
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
def add_clause(self, *ints):
self.nbvars = max(self.nbvars, max([abs(v) for v in ints]))
self.clauses.add(tuple(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):
w.add_clause(a, b, c)
w.add_clause(-a, -b, c)
w.add_clause(-a, b, -c)
w.add_clause(a, -b, -c)
w.add_clause(-a, -b, -c)
def notboth(w, a, b):
w.add_clause(-a, -b)
def add_constraints(graph, w):
# 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)
graph.read_edges(sys.argv[1])
logging.info("{} read".format(sys.argv[1]))
# store CNF
w = CnfStorage(os.fdopen(fd, mode='w', encoding='ascii'))
add_constraints(graph, w)
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:
os.unlink(filepath)

And how long did it take to run it? 0.9 seconds 😎

Thank you lingeling!