From 7ce00f0b24f3f039d19fe496de4f8bce5267d4ef Mon Sep 17 00:00:00 2001
From: penguinn <michellewerth@hotmail.com>
Date: Thu, 20 Feb 2020 16:14:10 +0100
Subject: [PATCH] start nine prisoners
---
Nine_Prisoners.ipynb | 128 +++++++++++++++++++++++++++++++++++++++++++
1 file changed, 128 insertions(+)
create mode 100644 Nine_Prisoners.ipynb
diff --git a/Nine_Prisoners.ipynb b/Nine_Prisoners.ipynb
new file mode 100644
index 0000000..b516684
--- /dev/null
+++ b/Nine_Prisoners.ipynb
@@ -0,0 +1,128 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# Nine Prisoners\n",
+ "\n",
+ "An artice in [Quanta magazine](https://www.quantamagazine.org/150-year-old-math-design-problem-solved-20150609) mentions the following puzzle by Dudeney and popularized by Martin Gardner:\n",
+ "\n",
+ "*\"So in the spirit of Kirkman, we will leave the gentle reader with another brainteaser, a slight variation on the schoolgirl puzzle devised in 1917 by the British puzzle aficionado Henry Ernest Dudeney and later popularized by Martin Gardner: Nine prisoners are taken outdoors for exercise in rows of three, with each adjacent pair of prisoners linked by handcuffs, on each of the six weekdays (back in Dudeney’s less enlightened times, Saturday was still a weekday). Can the prisoners be arranged over the course of the six days so that each pair of prisoners shares handcuffs exactly once?\"*\n",
+ "\n",
+ "An encoding of this puzzle in B is relatively straightforward, thanks to the use of sets, sequences and permutations and universal quantification. To improve the performance, symmetry reductions were added by hand in the model below. The constant `arrange` contains the solution to our puzzle: the arrangement of the prisoners for every working day from `1` to `Days`.\n",
+ "\n",
+ "In this notebook we will create two visualizations. The first one will be a quite simple table and is defined in the `ANIMATION_FUNCTION` in the machine below. \n",
+ "To investigate the machine, we have to set up its constants and initialize it, with the two commands below the machine."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: NinePrisoners"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE NinePrisoners\n",
+ "DEFINITIONS\n",
+ " Prisoners == 1..9;\n",
+ " Days == 6;\n",
+ " Cuffs == {1,2, 4,5, 7,8 };\n",
+ " share(day,cuff) == {arrange(day)(cuff),arrange(day)(cuff+1)};\n",
+ "/*The animation function for a simple visualisation*/\n",
+ " ANIMATION_FUNCTION ==\n",
+ " {r,c,i| r:1..Days & c:1..3 & i = arrange(r)(c) } \\/\n",
+ " {r,c,i| r:1..Days & c:5..7 & i = arrange(r)(c-1) } \\/\n",
+ " {r,c,i| r:1..Days & c:9..11 & i = arrange(r)(c-2) };\n",
+ " ANIMATION_FUNCTION_DEFAULT == {r,c,i| r:1..Days & c:1..11 & i = \" \" }\n",
+ "CONSTANTS arrange\n",
+ "PROPERTIES\n",
+ "/* typing + permutation requirement */\n",
+ " arrange : (1..Days) --> perm(Prisoners) &\n",
+ "\n",
+ "/* symmetry breaking */\n",
+ " arrange(1) = %i.(i:Prisoners|i) &\n",
+ " !d.(d:1..Days =>\n",
+ " !c.(c:Prisoners & c mod 3 = 1 => arrange(d)(c) < arrange(d)(c+2))) &\n",
+ " !d.(d:1..Days =>\n",
+ " !c.(c:{1,3} => arrange(d)(c) < arrange(d)(c+3)))\n",
+ " &\n",
+ "\n",
+ "/* the constraint proper */\n",
+ " !(c,d).(c:Cuffs & d:2..Days =>\n",
+ " !(c1,d1).(d1<d & d1>0 & c1:Cuffs =>\n",
+ " share(d,c) /= share(d1,c1))\n",
+ " )\n",
+ "OPERATIONS\n",
+ " r <-- Neighbours(i) = PRE i:Prisoners THEN \n",
+ "/* compute for every day the neighbours of i */\n",
+ " r := %d.(d:1..Days |\n",
+ " UNION(x,c).( x:Prisoners & c:Cuffs & i: share(d,c)| share(d,c) \\ {i})\n",
+ " ) END\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 0: $initialise_machine()"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": []
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "codemirror_mode": "prob2_jupyter_repl",
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob2-jupyter-repl",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}
--
GitLab