# Finding Vertex Covers with Z3

For a (undirected) graph where is a set of vertices and is a set of edges, a vertex cover (VC) is defined as a subset so that .

In other words, it's a subset of the vertices that contains at least one of the two vertices of each edge.

The size of a VC is , the number of vertices it contains.

z3 is a theorem prover that can also be used to solve optimization problems, in this case finding a small vertex cover for a given graph.

## Imports and the Graph Class

```from collections import namedtuple
from random import choice, shuffle
from z3 import Bool, Int, Implies, If, Optimize, Or, Sum, is_true
```

First we need a way to represent edges and graphs. Inheriting from ``` namedtuple ``` is a nice trick to avoid boilerplate code.

```
Edge = namedtuple('Edge', 'v1 v2')

class Graph(namedtuple('Graph', 'vertices edges')):
# ...

```

## Generating Random Graphs

I'd like to try finding the vertex cover of different graphs but I don't want to define them by hand, so the next step is to add a method that generates random graphs. It works by selecting a random subset of all possible (undirected, hence the ``` v1 < v2 ``` ) edges.

```@staticmethod
def generate(num_vertices, num_edges):
"""
Generate a random graph with a given number of vertices and edges
"""

vertices = range(0, num_vertices)

edges = [Edge(v1, v2) for v1 in vertices for v2 in vertices if v1 < v2]
shuffle(edges)

return Graph(list(vertices), edges[:num_edges])
```

## Graphviz

Python's string representation of graphs is boring to look at, so why not render them using Graphviz? This function already includes an optional ``` cover ``` argument to highlight vertices that are part of the vertex cover we will compute later.

```def save_dot(self, path, cover=[]):
"""
Format graph in .dot format, optionally highlighting vertices
that are part of a vertex cover.
"""

with open(path, 'w') as f:
f.write('graph {\n')
f.write('  node [style=filled];\n')

for vertex in self.vertices:
if vertex in cover:
f.write(f'  {vertex} [label="{vertex}", fillcolor="red"];\n')
else:
f.write(f'  {vertex} [label="{vertex}"];\n')

for edge in self.edges:
f.write(f'  {edge.v1} -- {edge.v2};\n')

f.write('}\n')
```

### Example

Here's what this looks like for a graph with 5 vertices and 8 edges:

## Finding Vertex Covers

To find a vertex cover, we add a ``` Bool ``` variable for each vertex that will be true if the vertex if part of the vertex cover.

For an edge to be covered, at least one of it's vertices needs to be part of the cover (their respective variables need to be true).

We're not interested in any cover but in one that is as small as possible, so we define additional ``` _cost ``` ``` Int ``` variables for each vertex that are set to ``` 1 ``` if the vertex is part of the cover.

Then we tell the optimizer to minimize the sum of all cost variables, in effect minimizing the size of the VC.

```def find_vc(self):
"""
Find a vertex cover of minimal size in a graph
"""
optimizer = Optimize()

# If an edge is part of the vertex cover, it implies that both
# vertices are covered
for edge in self.edges:
# For an edge to be covered, at least one of its vertices must
# be part of the VC

# Each covered vertex adds 1 to the cover size
costs = []
for vertex in self.vertices:
cost = Int(f'{vertex}_cost')
optimizer.add(If(Bool(vertex), cost == 1, cost == 0))
costs.append(cost)

# We want the VC to be as small as possible
optimizer.minimize(Sum(costs))

if optimizer.check():
model = optimizer.model()
# The variables for vertices that are part of the cover
# are true in the model
return [v for v in self.vertices if is_true(model[Bool(v)])]
```

## Footnotes

1

``` from z3 import * ``` would be fine, too, but my Python Org Mode source blocks don't seem to work with ``` * ``` imports.

If you have an idea how this page could be improved or a comment send me a mail.