|
|
/* Graceful Tree Labeling Problem */
/* Author: Mike Appleby <mike@app.leby.org> */
/* The Graceful Labeling Problem for a tree G = (V, E), where V is the set of vertices and E is the set of edges, is to find a labeling of the vertices with the integers between 1 and |V| inclusive, such that no two vertices share a label, and such that each edge is uniquely identified by the positive, or absolute difference between the labels of its endpoints.
In other words, if vl are the vertex labels and el are the edge labels, then for every edge (u,v) in E, el[u,v]=abs(vl[u] - vl[v]).
https://en.wikipedia.org/wiki/Graceful_labeling */
set V;/* set of vertices */
set E within V cross V;/* set of edges */
set N := 1..card(V);/* vertex labels */
set M := 1..card(V)-1;/* edge labels */
var vx{V, N}, binary;/* binary encoding of vertex labels. vx[v,n] == 1 means vertex v has label n. */
s.t. vxa{v in V}: sum{n in N} vx[v,n] = 1;/* each vertex is assigned exactly one label. */
s.t. vxb{n in N}: sum{v in V} vx[v,n] = 1;/* each label is assigned to exactly one vertex. */
var vl{V}, integer, >= 1, <= card(V);/* integer encoding of vertex labels. vl[v] == n means vertex v has label n. */
s.t. vla{v in V}: vl[v] = sum{n in N} n * vx[v,n];/* by constraint vxa, exactly one of vx[v,n] == 1 and the rest are zero. So if vx[v,3] == 1, then vl[v] = 3. */
var ex{E, M}, binary;/* binary encoding of edge labels. ex[u,v,n] == 1 means edge (u,v) has label n. */
s.t. exa{(u,v) in E}: sum{m in M} ex[u,v,m] = 1;/* each edge is assigned exactly one label. */
s.t. exb{m in M}: sum{(u,v) in E} ex[u,v,m] = 1;/* each label is assigned to exactly one edge. */
var el{E}, integer, >= 1, <= card(E);/* integer encoding of edge labels. el[u,v] == n means edge (u,v) has label n. */
s.t. ela{(u,v) in E}: el[u,v] = sum{m in M} m * ex[u,v,m];/* similar to vla above, define integer encoding of edge labels in terms of the corresponding binary variable. */
var gt{E}, binary;/* gt[u,v] = 1 if vl[u] > vl[v] else 0. gt helps encode the absolute value constraint, below. */
s.t. elb{(u,v) in E}: el[u,v] >= vl[u] - vl[v];s.t. elc{(u,v) in E}: el[u,v] <= vl[u] - vl[v] + 2*card(V)*(1-gt[u,v]);s.t. eld{(u,v) in E}: el[u,v] >= vl[v] - vl[u];s.t. ele{(u,v) in E}: el[u,v] <= vl[v] - vl[u] + 2*card(V)*gt[u,v];
/* These four constraints together model the absolute value constraint of the graceful labeling problem: el[u,v] == abs(vl[u] - vl[v]). However, since the absolute value is a non-linear function, we transform it into a series of linear constraints, as above.
To see that these four constraints model the absolute value condition, consider the following cases:
if vl[u] > vl[v] and gt[u,v] == 0 then - ele is unsatisfiable, since the constraint ele amounts to
el[u,v] <= vl[v] - vl[u] + 0 (since gt[u,v] == 0) <= -1 (since vl[u] > vl[v])
but el[u,v] is declared with lower bound >= 1; hence, the constraints cannot be satisfied if vl[u] > vl[v] and gt[u,v] == 0.
if vl[u] > vl[v] and gt[u,v] == 1 then - elb and elc together are equivalent to
vl[u] - vl[v] <= el[u,v] <= vl[u] - vl[v], i.e. el[u,v] = vl[u] - vl[v] = abs(vl[u] - vl[v]) (since vl[u] > vl[v])
- eld and elc together are equivalent to
vl[v] - vl[u] <= el[u,v] <= vl[v] - vl[u] + 2|V|
the tightest possible bounds are
-1 <= el[u,v] <= |V|+1
which is satisfied since both bounds are looser than the constraints on el's variable declaration, namely
var el{E}, integer, >= 1, <= card(E);
where |E| = |V|-1
The cases for vl[v] > vl[u] are similar, but with roles reversed for elb/elc and eld/ele.
In other words, when vl[u] > vl[v], then gt[u,v] == 1, elb and elc together model the absolute value constraint, and ele and eld are satisfied due to bounds constraints on el. When vl[v] > vl[u], then gt[u,v] == 0, ele and eld model the absolute value constraint, and elb and elc are satisfied due to bounds constraints on el.
Note that vl[u] != vl[v], by a combination of constraints vxa, vxb, and vla. */
solve;
check 0 = card(N symdiff setof{v in V} vl[v]);/* every vertex label is assigned to one vertex */
check 0 = card(M symdiff setof{(u,v) in E} el[u,v]);/* every edge label is assigned to one edge */
check {(u,v) in E} el[u,v] = abs(vl[u] - vl[v]);/* every edge label for every edge (u,v) == abs(vl[u] - vl[v]) */
printf "vertices:\n";for{v in V} { printf "\t%s: %d\n", v, vl[v]; }
printf "edges:\n";printf "\torig\tvlabel\telabel\tabs(u-v)\n";for{(u,v) in E} { printf "\t(%s,%s)\t(%d,%d)\t%d\t%d\n", u, v, vl[u], vl[v], el[u,v], abs(vl[u]-vl[v]);}
data;
set V := a b c d e f g;set E := a b, a d, a g, b c, b e, e f;
end;
|
