Graph Coloring with SAT

This small page was written as supplementary material to the JKU's Logic course's first exercise sheet. I hope you have fun reading it and maybe learn something from it! I tried to build everything as small functions that you can use to build a bigger formula. This is also how you encode bigger and bigger problems. Divide and Conquer strikes again and morphs smart software engineering together with logical formulas.

Graph Coloring (or most commonly Vertex Coloring) is a common problem found again and again. In short, we have a graph with some vertices and some edges between these vertices . We want to color the graph using different colors.

What sounds easy is actually one of Karp's 21 NP-complete problems from 1972. This also means we could translate it into some other problem, solve that, and convert the solution back to a colored graph we can use! Let's do this with SAT.

Let's say we have the vertices and the edges . Can we color this graph with two colors 1 and 2?

For this implementation, we use the fancy itertools library provided by Python, allowing us to directly encode all combinations we need.

import sys
from itertools import combinations, product

V = { 'a', 'b', 'c' }
E = { ('a','b'), ('b','c'), ('c','a') }
C = { '1', '2' }

Each vertex must have a color. We therefore write a conjunction over disjunctions for each vertex' colors.

def color_each_vertex(V, C, f=sys.stdout):
    f.write('(')
    f.write(" & ".join(
        "(" +
        " | ".join([f"{v}_{c}" for c in C])
        + ")"
        for v in V))
    f.write(')\n')

color_each_vertex(V, C)

((a_1 | a_2) & (c_1 | c_2) & (b_1 | b_2))

We also need to say that each vertex has exactly one color. We effectively form an cardinality constraint. Many different variants for cardinality constraints exist, but here we focus on the most basic one: We say that not both colors are active at the same time.

def each_vertex_has_only_one_color(V, C, f=sys.stdout):
    f.write('(')
    f.write(' & '.join([f'!({a1}_{a2} & {b1}_{b2})'
                         for v in V
                         for (a1,a2),(b1,b2) in combinations(product(v, C), 2)]))
    f.write(')\n')

each_vertex_has_only_one_color(V, C)

(!(a_1 & a_2) & !(c_1 & c_2) & !(b_1 & b_2))

Now, we want each edge to not have the same color on both sides.

def encode_edges(E, C, f=sys.stdout):
    f.write('(')
    f.write(" & ".join([f"!({a}_{c} & {b}_{c})" for a,b in E for c in C]))
    f.write(')\n')

encode_edges(E, C)

(!(c_1 & a_1) & !(c_2 & a_2) & !(a_1 & b_1) & !(a_2 & b_2) & !(b_1 & c_1) & !(b_2 & c_2))

Now, we can combine everything into a formula! This code uses a small trick: We use Org Mode's (a nice mode for Emacs) raw output format and directly interpret the resulting text as another source block. By doing this, we generate ourselves some input for limboole that can be executed below, without first having to go somewhere else. We can of course also copy and paste the output into Limboole on the Go. Be sure to run a check for Satisfiability, not Validity.

We use a function to abstract over our problem, so we can re-use it later.

print('#+BEGIN_SRC limboole :mode s :exports both')

def graph_coloring(V, E, C, f=sys.stdout):
    color_each_vertex(V, C, f)
    f.write('&\n')
    each_vertex_has_only_one_color(V, C, f)
    f.write('&\n')
    encode_edges(E, C, f)

graph_coloring(V, E, C)

print('#+END_SRC')

((a_1 | a_2) & (c_1 | c_2) & (b_1 | b_2))
&
(!(a_1 & a_2) & !(c_1 & c_2) & !(b_1 & b_2))
&
(!(c_1 & a_1) & !(c_2 & a_2) & !(a_1 & b_1) & !(a_2 & b_2) & !(b_1 & c_1) & !(b_2 & c_2))

% UNSATISFIABLE formula

Now, if we add another color, can we satisfy the formula?

Yes! Let's see:

print('#+BEGIN_SRC limboole :mode s :exports both')

CC = C.union({'3'})
graph_coloring(V, E, CC)

print('#+END_SRC')

((a_1 | a_2 | a_3) & (c_1 | c_2 | c_3) & (b_1 | b_2 | b_3))
&
(!(a_1 & a_2) & !(a_1 & a_3) & !(a_2 & a_3) & !(c_1 & c_2) & !(c_1 & c_3) & !(c_2 & c_3) & !(b_1 & b_2) & !(b_1 & b_3) & !(b_2 & b_3))
&
(!(c_1 & a_1) & !(c_2 & a_2) & !(c_3 & a_3) & !(a_1 & b_1) & !(a_2 & b_2) & !(a_3 & b_3) & !(b_1 & c_1) & !(b_2 & c_2) & !(b_3 & c_3))

% SATISFIABLE formula (satisfying assignment follows)
b_1 = 1
b_3 = 0
b_2 = 0
a_1 = 0
a_3 = 1
a_2 = 0
c_1 = 0
c_3 = 0
c_2 = 1