From d488cbd4ddbe2e4e18733b0383b5b89cb9168603 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Mon, 14 May 2018 14:38:14 +0200
Subject: [PATCH] add golomb ruler and graph iso
---
notebooks/tutorials/prob_solver_intro.ipynb | 87 +++++++++++++++++++--
1 file changed, 82 insertions(+), 5 deletions(-)
diff --git a/notebooks/tutorials/prob_solver_intro.ipynb b/notebooks/tutorials/prob_solver_intro.ipynb
index f672d65..7752c94 100644
--- a/notebooks/tutorials/prob_solver_intro.ipynb
+++ b/notebooks/tutorials/prob_solver_intro.ipynb
@@ -13,7 +13,7 @@
},
{
"cell_type": "code",
- "execution_count": 1,
+ "execution_count": 2,
"metadata": {},
"outputs": [
{
@@ -22,7 +22,7 @@
"1024"
]
},
- "execution_count": 1,
+ "execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
@@ -588,12 +588,89 @@
" victim = \"Agatha\""
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## Golomb Ruler\n",
+ "A Golomb ruler with $n$ marks of length $len$ has the property that all distances between distinct marks are different\n",
+ "The following expresses the problem in B:"
+ ]
+ },
{
"cell_type": "code",
- "execution_count": null,
+ "execution_count": 1,
"metadata": {},
- "outputs": [],
- "source": []
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\ta = {(1↦0),(2↦2),(3↦6),(4↦9),(5↦14),(6↦24),(7↦25)}\n",
+ "\tlen = 25\n",
+ "\tn = 7"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "n=7 & len=25 &\n",
+ "a:1..n --> 0..len & !i.(i:2..n => a(i-1) < a(i)) & \n",
+ "!(i1,j1,i2,j2).(( i1>0 & i2>0 & j1<=n & j2 <= n & i1<j1 & i2<j2 & (i1,j1) /= (i2,j2)) => (a(j1)-a(i1) /= a(j2)-a(i2)))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## Graph Isomorphism\n",
+ "We can check two graphs $g1$ and $g2$ for isomporhism by trying to find a solution for the following predicate:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tn1 = \"a\"\n",
+ "\tiso = {(1↦\"c\"),(2↦\"a\"),(3↦\"b\")}\n",
+ "\tn2 = \"b\"\n",
+ "\tn3 = \"c\"\n",
+ "\tV = {1,2,3}\n",
+ "\tg1 = {(1↦2),(1↦3),(2↦3)}\n",
+ "\tg2 = {(\"a\"↦\"b\"),(\"c\"↦\"a\"),(\"c\"↦\"b\")}\n",
+ "\tv1 = 1\n",
+ "\tv2 = 2\n",
+ "\tv3 = 3\n",
+ "\tN = {\"a\",\"b\",\"c\"}"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "LET V,N,v1,v2,v3,n1,n2,n3 BE\n",
+ " v1=1 & v2=2 & v3=3 & n1=\"a\" & n2=\"b\" & n3=\"c\" &\n",
+ " V = {v1,v2,v3} & N = {n1,n2,n3}\n",
+ "IN\n",
+ "g1 = {v1 |->v2, v1|->v3, v2|->v3} &\n",
+ "g2 = {n3 |->n2, n3|->n1, n1|->n2} &\n",
+ "iso: V >->> N & !v.(v:V => iso[g1[{v}]] = g2[iso[{v}]])\n",
+ "END"
+ ]
},
{
"cell_type": "code",
--
GitLab