Finding Vertex Covers with Z3

python z3

Table of Contents

For a (undirected) graph finding_vertex_covers_with_z3_b0af5bdcaadf3b35b6b3763247908c378ef836e3.svg where finding_vertex_covers_with_z3_a972fbd3e48c1bfc602014f0064e63fcaaa74568.svg is a set of vertices and finding_vertex_covers_with_z3_8c73571820b386db3f3b38c9954544041bc69219.svg is a set of edges, a vertex cover (VC) is defined as a subset finding_vertex_covers_with_z3_a669f9588e700ddc3c99da52214415c06232d280.svg so that finding_vertex_covers_with_z3_0eed93f8e88b8ef71f78d13f1a29b7088a99a191.svg .

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.

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]

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


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')
                f.write(f'  {vertex} [label="{vertex}"];\n')

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



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

    # We want the VC to be as small as possible

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


graph_00.svg graph_01.svg graph_02.svg graph_03.svg graph_04.svg graph_05.svg graph_06.svg graph_07.svg graph_08.svg graph_09.svg



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.