simplex-glpk with modified glpk for fpgaHEADmaster

1 files changed, 152 insertions, 0 deletions

diff --git a/glpk-5.0/examples/graceful.mod b/glpk-5.0/examples/graceful.mod
new file mode 100644
index 0000000..4042065
--- /dev/null
+++ b/glpk-5.0/examples/graceful.mod
@@ -0,0 +1,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;