## Table of Contents

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

^{
1
}

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 optimizer.add(Or(Bool(edge.v1), Bool(edge.v2))) # 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)])]

## Examples

## Footnotes

^{ 1 }

```
from z3 import *
```

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

imports.