Finding Vertex Covers with Z3

Table of Contents

For a (undirected) graph finding_vertex_covers_with_z3_b0af5bdcaadf3b35b6b3763247908c378ef836e3.svg 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 finding_vertex_covers_with_z3_5f1da9e0b5e71abe07d3700d02ba45d260e21b70.svg , 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
        optimizer.add(Or(Bool(edge.v1), Bool(edge.v2)))

    # Each covered vertex adds 1 to the cover size.
    # We want the VC to be as small as possible
    costs = [If(Bool(vertex), 1, 0) for v in self.vertices]
    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

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.