# Graph Coloring with SAT

## Foreword

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.

## Introduction

*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.

## Problem Statement

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' }

## Constrain Vertices

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

## Constrain Colors to Only 1 per Vertex

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

## Encode Edges between Vertices

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

## Combining everything to generate the formula

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

## How many colors would we need?

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