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!