von Koch and Z3

Replica of the Zuse Z3 [5].

In [1] we showed a MIP formulation to label a tree graph in a “graceful” way [2]. Here we use the SMT (Satisfiability Modulo Theories [3]) solver Z3 from Microsoft [4]. Z3 is a library and for this example we use the Python bindings. (Z3 is also the name of an early computer, see the picture above).

The problem can be stated as follows. Using a tree graph with \(n\) nodes and \(n-1\) arcs, assign unique integer labels \(1,\dots,n\) to the nodes and \(1,\dots,n-1\) to the arcs such that for an arc \((i,j)\) we have

\[\mathit{ArcLabel}(i,j) = |\mathit{NodeLabel}(i)-\mathit{NodeLabel}(j)|\]

We use again the small dataset:

On the right is one possible solution.

So our model needs to handle the following conditions:

1. \(1 \le \mathit{NodeLabel(i)} \le n\) and all-different
2. \(1 \le \mathit{ArcLabel(i,j)} \le n-1\) and all-different
3. \(\mathit{ArcLabel}(i,j) = |\mathit{NodeLabel}(i)-\mathit{NodeLabel}(j)|\)

The Z3 model is fairly high-level, and we can model these conditions quite naturally.

from z3 import * nodes = ['a','b','c','d','e','f','g'] network = [('a','b'),('a','d'),('a','g'), ('b','c'),('b','e'), ('e','f')] numnodes = len(nodes) numarcs = len(network) # nodes X = [ Int('%s' % nodes[i]) for i in range(numnodes) ] X_AllDifferent = Distinct( [ X[i] for i in range(numnodes) ] ) X_LB = And( [ X[i] >= 1 for i in range(numnodes) ] ) X_UB = And( [ X[i] <= numnodes for i in range(numnodes) ] ) X_cons = [ X_AllDifferent,X_LB,X_UB ] # arcs A = [ Int('%s.%s' % network[i]) for i in range(numarcs) ] A_AllDifferent = Distinct( [ A[i] for i in range(numarcs) ] ) A_LB = And( [ A[i] >= 1 for i in range(numarcs) ] ) A_UB = And( [ A[i] <= numarcs for i in range(numarcs) ] ) A_cons = [ A_AllDifferent,A_LB,A_UB ] # get node numbers of arcs node1 = [nodes.index(network[i][0]) for i in range(numarcs)] node2 = [nodes.index(network[i][1]) for i in range(numarcs)] # no built-in absolute value def Abs(x): return If(x >= 0,x,-x) # difference XA_cons = And([ A[i] == Abs(X[node1[i]]-X[node2[i]]) for i in range(numarcs) ]) all_cons = X_cons + A_cons + [ XA_cons ] solve(all_cons)

The main issue is that Z3 does not have a built-in Abs function. So, we implement our Abs using an If.

The output looks like:

[f = 5, b = 2, a = 7, c = 6, d = 1, e = 3, g = 4, e.f = 2, b.e = 1, b.c = 4, a.g = 3, a.d = 6, a.b = 5]

Enumerating all solutions

Like a MIP solver Z3 returns just one solution. We can enumerate all solutions by adding a constraint that forbids the current solution. For the above solution such a constraint can look like Or[f!=5,b!=2,a!=7,c!=6,d!=1,e!=3,g!=4]. A complete algorithm is:

s = Solver() s.add(all_cons) k = 0 res = [] while s.check() == sat: m = s.model() k = k + 1 sol = [m.evaluate(X[i]) for i in range(numnodes)] res = res + [(k,sol)] forbid = Or([X[i] != sol[i] for i in range(numnodes)]) s.add(forbid) print(res)

Indeed we also get our 52 solutions (only the node labels are reproduced here):

[(1, [4, 1, 6, 5, 7, 3, 2]), (2, [1, 5, 2, 6, 3, 4, 7]), (3, [1, 5, 2, 7, 3, 4, 6]), (4, [2, 7, 5, 3, 1, 4, 6]), (5, [1, 7, 4, 2, 3, 5, 6]), (6, [2, 6, 4, 5, 1, 7, 3]), (7, [7, 3, 6, 1, 5, 4, 2]), (8, [7, 3, 6, 2, 5, 4, 1]), (9, [7, 1, 4, 6, 5, 3, 2]), (10, [6, 1, 3, 5, 7, 4, 2]), (11, [7, 1, 3, 4, 5, 6, 2]), (12, [7, 1, 3, 2, 5, 6, 4]), (13, [7, 1, 4, 2, 5, 3, 6]), (14, [7, 2, 4, 1, 5, 6, 3]), (15, [7, 2, 4, 3, 5, 6, 1]), (16, [6, 2, 4, 5, 7, 1, 3]), (17, [6, 2, 4, 3, 7, 1, 5]), (18, [5, 1, 4, 6, 7, 2, 3]), (19, [4, 1, 5, 6, 7, 2, 3]), (20, [3, 1, 5, 6, 7, 2, 4]), (21, [3, 1, 5, 4, 7, 2, 6]), (22, [4, 1, 5, 3, 7, 2, 6]), (23, [2, 1, 6, 5, 7, 3, 4]), (24, [2, 1, 6, 4, 7, 3, 5]), (25, [6, 1, 3, 2, 7, 4, 5]), (26, [4, 1, 6, 2, 7, 3, 5]), (27, [5, 1, 4, 3, 7, 2, 6]), (28, [5, 7, 3, 2, 1, 6, 4]), (29, [5, 2, 6, 3, 7, 1, 4]), (30, [2, 6, 4, 3, 1, 7, 5]), (31, [3, 7, 4, 2, 1, 6, 5]), (32, [1, 6, 4, 7, 3, 2, 5]), (33, [6, 7, 2, 3, 1, 5, 4]), (34, [1, 7, 5, 6, 3, 2, 4]), (35, [3, 6, 2, 5, 1, 7, 4]), (36, [1, 6, 2, 7, 5, 3, 4]), (37, [1, 6, 4, 5, 3, 2, 7]), (38, [1, 7, 5, 4, 3, 2, 6]), (39, [1, 6, 2, 4, 5, 3, 7]), (40, [5, 2, 6, 4, 7, 1, 3]), (41, [3, 7, 4, 5, 1, 6, 2]), (42, [7, 2, 6, 1, 3, 5, 4]), (43, [7, 2, 6, 4, 3, 5, 1]), (44, [3, 6, 2, 4, 1, 7, 5]), (45, [4, 7, 3, 2, 1, 6, 5]), (46, [2, 7, 5, 6, 1, 4, 3]), (47, [1, 7, 4, 6, 3, 5, 2]), (48, [4, 7, 2, 3, 1, 5, 6]), (49, [4, 7, 3, 5, 1, 6, 2]), (50, [5, 7, 3, 4, 1, 6, 2]), (51, [4, 7, 2, 6, 1, 5, 3]), (52, [6, 7, 2, 4, 1, 5, 3])]

The last model was infeasible and caused the loop to end. We can in fact print this model and see how all the cuts where added:

[Distinct(a, b, c, d, e, f, g), And(a >= 1, b >= 1, c >= 1, d >= 1, e >= 1, f >= 1, g >= 1), And(a <= 7, b <= 7, c <= 7, d <= 7, e <= 7, f <= 7, g <= 7), Distinct(a.b, a.d, a.g, b.c, b.e, e.f), And(a.b >= 1, a.d >= 1, a.g >= 1, b.c >= 1, b.e >= 1, e.f >= 1), And(a.b <= 6, a.d <= 6, a.g <= 6, b.c <= 6, b.e <= 6, e.f <= 6), And(a.b == If(a - b >= 0, a - b, -(a - b)), a.d == If(a - d >= 0, a - d, -(a - d)), a.g == If(a - g >= 0, a - g, -(a - g)), b.c == If(b - c >= 0, b - c, -(b - c)), b.e == If(b - e >= 0, b - e, -(b - e)), e.f == If(e - f >= 0, e - f, -(e - f))), Or(a != 4, b != 1, c != 6, d != 5, e != 7, f != 3, g != 2), Or(a != 1, b != 5, c != 2, d != 6, e != 3, f != 4, g != 7), Or(a != 1, b != 5, c != 2, d != 7, e != 3, f != 4, g != 6), Or(a != 2, b != 7, c != 5, d != 3, e != 1, f != 4, g != 6), Or(a != 1, b != 7, c != 4, d != 2, e != 3, f != 5, g != 6), Or(a != 2, b != 6, c != 4, d != 5, e != 1, f != 7, g != 3), Or(a != 7, b != 3, c != 6, d != 1, e != 5, f != 4, g != 2), Or(a != 7, b != 3, c != 6, d != 2, e != 5, f != 4, g != 1), Or(a != 7, b != 1, c != 4, d != 6, e != 5, f != 3, g != 2), Or(a != 6, b != 1, c != 3, d != 5, e != 7, f != 4, g != 2), Or(a != 7, b != 1, c != 3, d != 4, e != 5, f != 6, g != 2), Or(a != 7, b != 1, c != 3, d != 2, e != 5, f != 6, g != 4), Or(a != 7, b != 1, c != 4, d != 2, e != 5, f != 3, g != 6), Or(a != 7, b != 2, c != 4, d != 1, e != 5, f != 6, g != 3), Or(a != 7, b != 2, c != 4, d != 3, e != 5, f != 6, g != 1), Or(a != 6, b != 2, c != 4, d != 5, e != 7, f != 1, g != 3), Or(a != 6, b != 2, c != 4, d != 3, e != 7, f != 1, g != 5), Or(a != 5, b != 1, c != 4, d != 6, e != 7, f != 2, g != 3), Or(a != 4, b != 1, c != 5, d != 6, e != 7, f != 2, g != 3), Or(a != 3, b != 1, c != 5, d != 6, e != 7, f != 2, g != 4), Or(a != 3, b != 1, c != 5, d != 4, e != 7, f != 2, g != 6), Or(a != 4, b != 1, c != 5, d != 3, e != 7, f != 2, g != 6), Or(a != 2, b != 1, c != 6, d != 5, e != 7, f != 3, g != 4), Or(a != 2, b != 1, c != 6, d != 4, e != 7, f != 3, g != 5), Or(a != 6, b != 1, c != 3, d != 2, e != 7, f != 4, g != 5), Or(a != 4, b != 1, c != 6, d != 2, e != 7, f != 3, g != 5), Or(a != 5, b != 1, c != 4, d != 3, e != 7, f != 2, g != 6), Or(a != 5, b != 7, c != 3, d != 2, e != 1, f != 6, g != 4), Or(a != 5, b != 2, c != 6, d != 3, e != 7, f != 1, g != 4), Or(a != 2, b != 6, c != 4, d != 3, e != 1, f != 7, g != 5), Or(a != 3, b != 7, c != 4, d != 2, e != 1, f != 6, g != 5), Or(a != 1, b != 6, c != 4, d != 7, e != 3, f != 2, g != 5), Or(a != 6, b != 7, c != 2, d != 3, e != 1, f != 5, g != 4), Or(a != 1, b != 7, c != 5, d != 6, e != 3, f != 2, g != 4), Or(a != 3, b != 6, c != 2, d != 5, e != 1, f != 7, g != 4), Or(a != 1, b != 6, c != 2, d != 7, e != 5, f != 3, g != 4), Or(a != 1, b != 6, c != 4, d != 5, e != 3, f != 2, g != 7), Or(a != 1, b != 7, c != 5, d != 4, e != 3, f != 2, g != 6), Or(a != 1, b != 6, c != 2, d != 4, e != 5, f != 3, g != 7), Or(a != 5, b != 2, c != 6, d != 4, e != 7, f != 1, g != 3), Or(a != 3, b != 7, c != 4, d != 5, e != 1, f != 6, g != 2), Or(a != 7, b != 2, c != 6, d != 1, e != 3, f != 5, g != 4), Or(a != 7, b != 2, c != 6, d != 4, e != 3, f != 5, g != 1), Or(a != 3, b != 6, c != 2, d != 4, e != 1, f != 7, g != 5), Or(a != 4, b != 7, c != 3, d != 2, e != 1, f != 6, g != 5), Or(a != 2, b != 7, c != 5, d != 6, e != 1, f != 4, g != 3), Or(a != 1, b != 7, c != 4, d != 6, e != 3, f != 5, g != 2), Or(a != 4, b != 7, c != 2, d != 3, e != 1, f != 5, g != 6), Or(a != 4, b != 7, c != 3, d != 5, e != 1, f != 6, g != 2), Or(a != 5, b != 7, c != 3, d != 4, e != 1, f != 6, g != 2), Or(a != 4, b != 7, c != 2, d != 6, e != 1, f != 5, g != 3), Or(a != 6, b != 7, c != 2, d != 4, e != 1, f != 5, g != 3)]

References

1. The von Koch conjecture, http://yetanothermathprogrammingconsultant.blogspot.com/2017/09/the-von-koch-conjecture.html
2. Graceful Labeling, https://en.wikipedia.org/wiki/Graceful_labeling
3. Satisfiability modulo theories, https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
4. https://github.com/Z3Prover/z3
5. Z3 (computer), https://en.wikipedia.org/wiki/Z3_(computer)