1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
|
/* 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;
|
