## Dependency graphs and topological sorting using Z3 SMT-solver

Topological sorting is an operation many programmers well familiar with: this is what "make" tool do when it find an order of items to process. Items not dependent of anything can be processed first. The most dependent items at the end.

Dependency graph is a graph and topological sorting is such a "contortion" of the graph, when you can see an order of items.

For example, let's create a sample graph in Wolfram Mathematica:

In[]:= g = Graph[{7 -> 1, 7 -> 0, 5 -> 1, 3 -> 0, 3 -> 4, 1 -> 2, 1 -> 6,
1 -> 4, 0 -> 6}, VertexLabels -> "Name"]


Each arrow shows that an item is needed by an item arrow pointing to, i.e., if "a -> b", then item "a" must be first processed, because "b" needs it, or "b" depends on "a".

How Mathematica would sort the dependency graph?

In[]:= TopologicalSort[g]
Out[]= {7, 3, 0, 5, 1, 4, 6, 2}


So you're going to process item 7, then 3, 0, and 2 at the very end.

The algorithm in the Wikipedia article is probably used in "make" and whatever IDE you use for building your code.

Also, many UNIX platforms had separate "tsort" utility: https://en.wikipedia.org/wiki/Tsort.

How would tsort sort the graph? I'm making the text file with input data:

7 1
7 0
5 1
3 0
3 4
1 2
1 6
1 4
0 6


And run tsort:

 % tsort tst
3
5
7
0
1
4
6
2


Now I'll use Z3 SMT-solver for topological sort, which is overkill, but quite spectacular: all we need to do is to add constraint for each edge (or "connection") in graph, if "a -> b", then "a" must be less then "b", where each variable reflects ordering.

#!/usr/bin/env python

from z3 import *

TOTAL=8

order=[Int('%d' % i) for i in range(TOTAL)]

s=Solver()
s.add(Distinct(order))
for i in range(TOTAL):
s.add(And(order[i]>=0, order[i]<TOTAL))

s.add(order[5]<order[1])

s.add(order[3]<order[4])
s.add(order[3]<order[0])

s.add(order[7]<order[0])
s.add(order[7]<order[1])

s.add(order[1]<order[2])
s.add(order[1]<order[4])
s.add(order[1]<order[6])

s.add(order[0]<order[6])

print s.check()

m=s.model()
order_to_print=[None]*(TOTAL)
for i in range(TOTAL):
order_to_print[m[order[i]].as_long()]=i

print order_to_print


Almost the same result, but also correct:

sat
[3, 5, 7, 0, 1, 2, 4, 6]


Please drop me email about any bug(s) and suggestion(s): dennis(@)yurichev.com.