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):
    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!

Boston Key Party: Graph 3-coloring with SAT solvers

Leave a Reply

Your email address will not be published. Required fields are marked *