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 \(n1\) arcs, assign unique integer labels \(1,\dots,n\) to the nodes and \(1,\dots,n1\) 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 \le \mathit{NodeLabel(i)} \le n\) and alldifferent
 \(1 \le \mathit{ArcLabel(i,j)} \le n1\) and alldifferent
 \(\mathit{ArcLabel}(i,j) = \mathit{NodeLabel}(i)\mathit{NodeLabel}(j)\)
The Z3 model is fairly highlevel, and we can model these conditions quite naturally.

The main issue is that Z3 does not have a builtin 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]), 
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
 The von Koch conjecture, http://yetanothermathprogrammingconsultant.blogspot.com/2017/09/thevonkochconjecture.html
 Graceful Labeling, https://en.wikipedia.org/wiki/Graceful_labeling
 Satisfiability modulo theories, https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
 https://github.com/Z3Prover/z3
 Z3 (computer), https://en.wikipedia.org/wiki/Z3_(computer)
No comments:
Post a Comment