diff --git a/docs/tutorials-notebook.rst b/docs/tutorials-notebook.rst index ff276ed81..05b62c6e9 100644 --- a/docs/tutorials-notebook.rst +++ b/docs/tutorials-notebook.rst @@ -4,13 +4,20 @@ Tutorials using Conjure notebook ================================ - We demonstrate the use of Conjure for some small problems. -See `conjure-notebook repository `_ for details. +Tutorials in this section are a copy of those in the tutorials section. +They are adapted to use the notebook extension for better interactivity. +We might add new tutorials using this style in the future. +See `conjure-notebook repository `_ for details. .. toctree:: :maxdepth: 1 tutorials/notebooks/KnapsackProblem + tutorials/notebooks/NurseRostering + tutorials/notebooks/Futoshiki + tutorials/notebooks/Semigroups,_Monoids_and_Groups + tutorials/notebooks/Handcrafting_Instance_Generators_in_Essence + tutorials/notebooks/SimplePermutations diff --git a/docs/tutorials/notebooks/Handcrafting_Instance_Generators_in_Essence.ipynb b/docs/tutorials/notebooks/Handcrafting_Instance_Generators_in_Essence.ipynb index caec2a30f..327331ffa 100644 --- a/docs/tutorials/notebooks/Handcrafting_Instance_Generators_in_Essence.ipynb +++ b/docs/tutorials/notebooks/Handcrafting_Instance_Generators_in_Essence.ipynb @@ -1,64 +1,49 @@ { - "nbformat": 4, - "nbformat_minor": 0, - "metadata": { - "colab": { - "provenance": [], - "authorship_tag": "ABX9TyOyOIxXu5LVVSWqJoksN5gj", - "include_colab_link": true - }, - "kernelspec": { - "name": "python3", - "display_name": "Python 3" - }, - "language_info": { - "name": "python" - } - }, "cells": [ { + "attachments": {}, "cell_type": "markdown", "metadata": { - "id": "view-in-github", - "colab_type": "text" + "colab_type": "text", + "id": "view-in-github" }, "source": [ "\"Open" ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "# Handcrafting Instance Generators in Essence" - ], "metadata": { "id": "b_9MbyOpkR9A" - } + }, + "source": [ + "# Handcrafting Instance Generators in Essence" + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "Original [Handcrafting Instance Generators in Essence](https://conjure.readthedocs.io/en/latest/tutorials.html#semigroups-monoids-and-groups) by Joan Espasa Arxer and Christopher Stone. Adapted by Alex Gallagher." - ], "metadata": { "id": "ws4OTYvkkU4Z" - } + }, + "source": [ + "Original [Handcrafting Instance Generators in Essence](https://conjure.readthedocs.io/en/latest/tutorials/knapsack_generator/KnapGen.html) by Joan Espasa Arxer and Christopher Stone. Adapted by Alex Gallagher." + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "In modelling it is common to create an abstract model that expects some input parameters (Also known as “instances”) which are required to run and test the model. In this tutorial we demonstrate how to use ESSENCE to handcraft a generator of instances that can be used to produce input parameters for a specific model." - ], "metadata": { "id": "Hyk7zGoUkiV8" - } + }, + "source": [ + "In modelling it is common to create an abstract model that expects some input parameters (Also known as “instances”) which are required to run and test the model. In this tutorial we demonstrate how to use ESSENCE to handcraft a generator of instances that can be used to produce input parameters for a specific model." + ] }, { "cell_type": "code", - "source": [ - "!source <(curl -s https://raw.githubusercontent.com/conjure-cp/conjure-notebook/v0.0.2/scripts/install-colab.sh)\n", - "%load_ext conjure" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/", @@ -67,11 +52,10 @@ "id": "h8yaBmeymi1R", "outputId": "3da82d46-c6b8-4df8-b11a-e9faeba2b74a" }, - "execution_count": null, "outputs": [ { - "output_type": "stream", "name": "stdout", + "output_type": "stream", "text": [ " % Total % Received % Xferd Average Speed Time Time Time Current\n", " Dload Upload Total Spent Left Speed\n", @@ -83,249 +67,45 @@ ] }, { - "output_type": "display_data", "data": { + "application/javascript": "\"use strict\";\n\nCodeMirror.defineMode(\"text/conjure\", function (config) {\n\n var isOperatorChar = /[+\\-*=<>%^\\/]/;\n\n var keywords = {\n \"forall\": true,\n \"allDifferent\": true,\n \"allDiff\": true,\n \"alldifferent_except\": true,\n \"dim\": true,\n \"toSet\": true,\n \"toMSet\": true,\n \"toRelation\": true,\n \"maximising\": true,\n \"minimising\": true,\n \"forAll\": true,\n \"exists\": true,\n \"toInt\": true,\n \"sum\": true,\n \"be\": true,\n \"bijective\": true,\n \"bool\": true,\n \"by\": true,\n \"complete\": true,\n \"defined\": true,\n \"domain\": true,\n \"in\": true,\n \"or\": true,\n \"and\": true,\n \"false\": true,\n \"find\": true,\n \"from\": true,\n \"function\": true,\n \"given\": true,\n \"image\": true,\n \"indexed\": true,\n \"injective\": true,\n \"int\": true,\n \"intersect\": true,\n \"freq\": true,\n \"lambda\": true,\n \"language\": true,\n \"letting\": true,\n \"matrix\": true,\n \"maxNumParts\": true,\n \"maxOccur\": true,\n \"maxPartSize\": true,\n \"maxSize\": true,\n \"minNumParts\": true,\n \"minOccur\": true,\n \"minPartSize\": true,\n \"minSize\": true,\n \"mset\": true,\n \"numParts\": true,\n \"of\": true,\n \"partial\": true,\n \"partition\": true,\n \"partSize\": true,\n \"preImage\": true,\n \"quantifier\": true,\n \"range\": true,\n \"regular\": true,\n \"relation\": true,\n \"representation\": true,\n \"set\": true,\n \"size\": true,\n \"subset\": true,\n \"subsetEq\": true,\n \"such\": true,\n \"supset\": true,\n \"supsetEq\": true,\n \"surjective\": true,\n \"that\": true,\n \"together\": true,\n \"enum\": true,\n \"total\": true,\n \"true\": true,\n \"new\": true,\n \"type\": true,\n \"tuple\": true,\n \"union\": true,\n \"where\": true,\n \"branching\": true,\n \"on\": true\n }; \n var punc = \":;,.(){}[]\";\n\n function tokenBase(stream, state) {\n var ch = stream.next();\n if (ch == '\"') {\n state.tokenize.push(tokenString);\n return tokenString(stream, state);\n }\n if (/[\\d\\.]/.test(ch)) {\n if (ch == \".\") {\n stream.match(/^[0-9]+([eE][\\-+]?[0-9]+)?/);\n } else if (ch == \"0\") {\n stream.match(/^[xX][0-9a-fA-F]+/) || stream.match(/^0[0-7]+/);\n } else {\n stream.match(/^[0-9]*\\.?[0-9]*([eE][\\-+]?[0-9]+)?/);\n }\n return \"number\";\n }\n if (ch == \"/\") {\n if (stream.eat(\"*\")) {\n state.tokenize.push(tokenComment);\n return tokenComment(stream, state);\n }\n }\n if (ch == \"$\") {\n stream.skipToEnd();\n return \"comment\";\n }\n if (isOperatorChar.test(ch)) {\n stream.eatWhile(isOperatorChar);\n return \"operator\";\n }\n if (punc.indexOf(ch) > -1) {\n return \"punctuation\";\n }\n stream.eatWhile(/[\\w\\$_\\xa1-\\uffff]/);\n var cur = stream.current();\n \n if (keywords.propertyIsEnumerable(cur)) {\n return \"keyword\";\n }\n return \"variable\";\n }\n\n function tokenComment(stream, state) {\n var maybeEnd = false, ch;\n while (ch = stream.next()) {\n if (ch == \"/\" && maybeEnd) {\n state.tokenize.pop();\n break;\n }\n maybeEnd = (ch == \"*\");\n }\n return \"comment\";\n }\n\n function tokenUntilClosingParen() {\n var depth = 0;\n return function (stream, state, prev) {\n var inner = tokenBase(stream, state, prev);\n console.log(\"untilClosing\", inner, stream.current());\n if (inner == \"punctuation\") {\n if (stream.current() == \"(\") {\n ++depth;\n } else if (stream.current() == \")\") {\n if (depth == 0) {\n stream.backUp(1)\n state.tokenize.pop()\n return state.tokenize[state.tokenize.length - 1](stream, state)\n } else {\n --depth;\n }\n }\n }\n return inner;\n }\n }\n\n function tokenString(stream, state) {\n var escaped = false, next, end = false;\n while ((next = stream.next()) != null) {\n if (next == '(' && escaped) {\n state.tokenize.push(tokenUntilClosingParen());\n return \"string\";\n }\n if (next == '\"' && !escaped) { end = true; break; }\n escaped = !escaped && next == \"\\\\\";\n }\n if (end || !escaped)\n state.tokenize.pop();\n return \"string\";\n }\n\n return {\n startState: function (basecolumn) {\n return {\n tokenize: []\n };\n },\n\n token: function (stream, state) {\n if (stream.eatSpace()) return null;\n var style = (state.tokenize[state.tokenize.length - 1] || tokenBase)(stream, state);\n console.log(\"token\", style);\n return style;\n },\n\n blockCommentStart: \"/*\",\n blockCommentEnd: \"*/\",\n lineComment: \"$\"\n };\n});\n\n\nCodeMirror.defineMIME(\"text/conjure\", \"text/conjure\");\n\nrequire(['notebook/js/codecell'], function (codecell) {\n codecell.CodeCell.options_default.highlight_modes['magic_text/conjure'] = { 'reg': [/%?%conjure/] };\n Jupyter.notebook.events.one('kernel_ready.Kernel', function () {\n Jupyter.notebook.get_cells().map(function (cell) {\n if (cell.cell_type == 'code') { cell.auto_highlight(); }\n });\n });\n});\n\n", "text/plain": [ "" - ], - "application/javascript": [ - "\"use strict\";\n", - "\n", - "CodeMirror.defineMode(\"text/conjure\", function (config) {\n", - "\n", - " var isOperatorChar = /[+\\-*=<>%^\\/]/;\n", - "\n", - " var keywords = {\n", - " \"forall\": true,\n", - " \"allDifferent\": true,\n", - " \"allDiff\": true,\n", - " \"alldifferent_except\": true,\n", - " \"dim\": true,\n", - " \"toSet\": true,\n", - " \"toMSet\": true,\n", - " \"toRelation\": true,\n", - " \"maximising\": true,\n", - " \"minimising\": true,\n", - " \"forAll\": true,\n", - " \"exists\": true,\n", - " \"toInt\": true,\n", - " \"sum\": true,\n", - " \"be\": true,\n", - " \"bijective\": true,\n", - " \"bool\": true,\n", - " \"by\": true,\n", - " \"complete\": true,\n", - " \"defined\": true,\n", - " \"domain\": true,\n", - " \"in\": true,\n", - " \"or\": true,\n", - " \"and\": true,\n", - " \"false\": true,\n", - " \"find\": true,\n", - " \"from\": true,\n", - " \"function\": true,\n", - " \"given\": true,\n", - " \"image\": true,\n", - " \"indexed\": true,\n", - " \"injective\": true,\n", - " \"int\": true,\n", - " \"intersect\": true,\n", - " \"freq\": true,\n", - " \"lambda\": true,\n", - " \"language\": true,\n", - " \"letting\": true,\n", - " \"matrix\": true,\n", - " \"maxNumParts\": true,\n", - " \"maxOccur\": true,\n", - " \"maxPartSize\": true,\n", - " \"maxSize\": true,\n", - " \"minNumParts\": true,\n", - " \"minOccur\": true,\n", - " \"minPartSize\": true,\n", - " \"minSize\": true,\n", - " \"mset\": true,\n", - " \"numParts\": true,\n", - " \"of\": true,\n", - " \"partial\": true,\n", - " \"partition\": true,\n", - " \"partSize\": true,\n", - " \"preImage\": true,\n", - " \"quantifier\": true,\n", - " \"range\": true,\n", - " \"regular\": true,\n", - " \"relation\": true,\n", - " \"representation\": true,\n", - " \"set\": true,\n", - " \"size\": true,\n", - " \"subset\": true,\n", - " \"subsetEq\": true,\n", - " \"such\": true,\n", - " \"supset\": true,\n", - " \"supsetEq\": true,\n", - " \"surjective\": true,\n", - " \"that\": true,\n", - " \"together\": true,\n", - " \"enum\": true,\n", - " \"total\": true,\n", - " \"true\": true,\n", - " \"new\": true,\n", - " \"type\": true,\n", - " \"tuple\": true,\n", - " \"union\": true,\n", - " \"where\": true,\n", - " \"branching\": true,\n", - " \"on\": true\n", - " }; \n", - " var punc = \":;,.(){}[]\";\n", - "\n", - " function tokenBase(stream, state) {\n", - " var ch = stream.next();\n", - " if (ch == '\"') {\n", - " state.tokenize.push(tokenString);\n", - " return tokenString(stream, state);\n", - " }\n", - " if (/[\\d\\.]/.test(ch)) {\n", - " if (ch == \".\") {\n", - " stream.match(/^[0-9]+([eE][\\-+]?[0-9]+)?/);\n", - " } else if (ch == \"0\") {\n", - " stream.match(/^[xX][0-9a-fA-F]+/) || stream.match(/^0[0-7]+/);\n", - " } else {\n", - " stream.match(/^[0-9]*\\.?[0-9]*([eE][\\-+]?[0-9]+)?/);\n", - " }\n", - " return \"number\";\n", - " }\n", - " if (ch == \"/\") {\n", - " if (stream.eat(\"*\")) {\n", - " state.tokenize.push(tokenComment);\n", - " return tokenComment(stream, state);\n", - " }\n", - " }\n", - " if (ch == \"$\") {\n", - " stream.skipToEnd();\n", - " return \"comment\";\n", - " }\n", - " if (isOperatorChar.test(ch)) {\n", - " stream.eatWhile(isOperatorChar);\n", - " return \"operator\";\n", - " }\n", - " if (punc.indexOf(ch) > -1) {\n", - " return \"punctuation\";\n", - " }\n", - " stream.eatWhile(/[\\w\\$_\\xa1-\\uffff]/);\n", - " var cur = stream.current();\n", - " \n", - " if (keywords.propertyIsEnumerable(cur)) {\n", - " return \"keyword\";\n", - " }\n", - " return \"variable\";\n", - " }\n", - "\n", - " function tokenComment(stream, state) {\n", - " var maybeEnd = false, ch;\n", - " while (ch = stream.next()) {\n", - " if (ch == \"/\" && maybeEnd) {\n", - " state.tokenize.pop();\n", - " break;\n", - " }\n", - " maybeEnd = (ch == \"*\");\n", - " }\n", - " return \"comment\";\n", - " }\n", - "\n", - " function tokenUntilClosingParen() {\n", - " var depth = 0;\n", - " return function (stream, state, prev) {\n", - " var inner = tokenBase(stream, state, prev);\n", - " console.log(\"untilClosing\", inner, stream.current());\n", - " if (inner == \"punctuation\") {\n", - " if (stream.current() == \"(\") {\n", - " ++depth;\n", - " } else if (stream.current() == \")\") {\n", - " if (depth == 0) {\n", - " stream.backUp(1)\n", - " state.tokenize.pop()\n", - " return state.tokenize[state.tokenize.length - 1](stream, state)\n", - " } else {\n", - " --depth;\n", - " }\n", - " }\n", - " }\n", - " return inner;\n", - " }\n", - " }\n", - "\n", - " function tokenString(stream, state) {\n", - " var escaped = false, next, end = false;\n", - " while ((next = stream.next()) != null) {\n", - " if (next == '(' && escaped) {\n", - " state.tokenize.push(tokenUntilClosingParen());\n", - " return \"string\";\n", - " }\n", - " if (next == '\"' && !escaped) { end = true; break; }\n", - " escaped = !escaped && next == \"\\\\\";\n", - " }\n", - " if (end || !escaped)\n", - " state.tokenize.pop();\n", - " return \"string\";\n", - " }\n", - "\n", - " return {\n", - " startState: function (basecolumn) {\n", - " return {\n", - " tokenize: []\n", - " };\n", - " },\n", - "\n", - " token: function (stream, state) {\n", - " if (stream.eatSpace()) return null;\n", - " var style = (state.tokenize[state.tokenize.length - 1] || tokenBase)(stream, state);\n", - " console.log(\"token\", style);\n", - " return style;\n", - " },\n", - "\n", - " blockCommentStart: \"/*\",\n", - " blockCommentEnd: \"*/\",\n", - " lineComment: \"$\"\n", - " };\n", - "});\n", - "\n", - "\n", - "CodeMirror.defineMIME(\"text/conjure\", \"text/conjure\");\n", - "\n", - "require(['notebook/js/codecell'], function (codecell) {\n", - " codecell.CodeCell.options_default.highlight_modes['magic_text/conjure'] = { 'reg': [/%?%conjure/] };\n", - " Jupyter.notebook.events.one('kernel_ready.Kernel', function () {\n", - " Jupyter.notebook.get_cells().map(function (cell) {\n", - " if (cell.cell_type == 'code') { cell.auto_highlight(); }\n", - " });\n", - " });\n", - "});\n", - "\n" ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "stream", "name": "stdout", + "output_type": "stream", "text": [ "Conjure extension is loaded.\n", "For usage help run: %conjure_help\n" ] } + ], + "source": [ + "!source <(curl -s https://raw.githubusercontent.com/conjure-cp/conjure-notebook/v0.0.2/scripts/install-colab.sh)\n", + "%load_ext conjure" ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "## Instances for the Knapsack problem" - ], "metadata": { "id": "7DlRahOslGIO" - } + }, + "source": [ + "## Instances for the Knapsack problem" + ] }, { + "attachments": {}, "cell_type": "markdown", + "metadata": { + "id": "yByksQbYmFwO" + }, "source": [ "This model from the [Knapsack Problem](https://conjure.readthedocs.io/en/latest/tutorials.html#the-knapsack-problem) has 4 different “given” statements :\n", "\n", @@ -339,19 +119,17 @@ "\n", "\n", "\n" - ], - "metadata": { - "id": "yByksQbYmFwO" - } + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "The first parameter is fairly simple and we can even write this parameter with some value by hand as seen below." - ], "metadata": { "id": "xXdYIQKvmXOv" - } + }, + "source": [ + "The first parameter is fairly simple and we can even write this parameter with some value by hand as seen below." + ] }, { "cell_type": "code", @@ -365,14 +143,14 @@ }, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{}" ] }, + "execution_count": 2, "metadata": {}, - "execution_count": 2 + "output_type": "execute_result" } ], "source": [ @@ -381,23 +159,18 @@ ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "The remaining 3 parameters are more complex and labourious to be defined (too much work to be done by hand!) so we are going to write an ESSENCE specification that will create them for us. The fundamental starting step is writing find statements for each variable we wish to generate and ensure that the names of the variable (identifiers) are left unchanged. We can do so by writing:" - ], "metadata": { "id": "_EiqQ1uAnht9" - } + }, + "source": [ + "The remaining 3 parameters are more complex and labourious to be defined (too much work to be done by hand!) so we are going to write an ESSENCE specification that will create them for us. The fundamental starting step is writing find statements for each variable we wish to generate and ensure that the names of the variable (identifiers) are left unchanged. We can do so by writing:" + ] }, { "cell_type": "code", - "source": [ - "%%conjure\n", - "letting items be domain int(1..number_items)\n", - "find weight: function (total) items --> int(1..1000)\n", - "find gain: function (total) items --> int(1..1000)\n", - "find capacity: int(1..5000)" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -405,10 +178,8 @@ "id": "cDYM3WlAn0Lb", "outputId": "15308a29-c827-4f47-d71a-02bf82d93c64" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{'capacity': 1,\n", @@ -454,37 +225,42 @@ " '9': 1}}" ] }, + "execution_count": 3, "metadata": {}, - "execution_count": 3 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure\n", + "letting items be domain int(1..number_items)\n", + "find weight: function (total) items --> int(1..1000)\n", + "find gain: function (total) items --> int(1..1000)\n", + "find capacity: int(1..5000)" ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "Solving the above model (by running the cell above) will create a set of parameters for our knapsack model. However, these instances are not interesting enough yet." - ], "metadata": { "id": "L3_5bdbxn-_6" - } + }, + "source": [ + "Solving the above model (by running the cell above) will create a set of parameters for our knapsack model. However, these instances are not interesting enough yet." + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "We can make our instances more interesting by adding constraints into our generator’s model. The first thing we notice is that all values assigned are identical, a bit TOO symmetrical for our taste. One simple solution to this issue is ensuring that all weights and gains assignments are associated with distinct values. This can be done by imposing [injectivity](https://en.wikipedia.org/wiki/Injective_function) as a property of the function." - ], "metadata": { "id": "WqMwmD0OoGs4" - } + }, + "source": [ + "We can make our instances more interesting by adding constraints into our generator’s model. The first thing we notice is that all values assigned are identical, a bit TOO symmetrical for our taste. One simple solution to this issue is ensuring that all weights and gains assignments are associated with distinct values. This can be done by imposing [injectivity](https://en.wikipedia.org/wiki/Injective_function) as a property of the function." + ] }, { "cell_type": "code", - "source": [ - "%%conjure\n", - "find weight: function (total, injective) items --> int(1..1000)\n", - "find gain: function (total, injective) items --> int(1..1000)\n", - "find capacity: int(1..5000)" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -492,10 +268,8 @@ "id": "LGHHUkfXoZOg", "outputId": "bb95af51-7709-42f9-b4f8-82a0e0c0ca93" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{'capacity': 1,\n", @@ -541,47 +315,51 @@ " '9': 1}}" ] }, + "execution_count": 12, "metadata": {}, - "execution_count": 12 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure\n", + "find weight: function (total, injective) items --> int(1..1000)\n", + "find gain: function (total, injective) items --> int(1..1000)\n", + "find capacity: int(1..5000)" ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "Running this gives us a slighly more interesting parameters set but it is not there yet The specific order that appears in the results is solver dependent. The default solver used by conjure is Minion and we can use an optional flag to have the variables assigned in a random order. This can be done with this command:" - ], "metadata": { "id": "RqTcTMtuoitZ" - } + }, + "source": [ + "Running this gives us a slighly more interesting parameters set but it is not there yet The specific order that appears in the results is solver dependent. The default solver used by conjure is Minion and we can use an optional flag to have the variables assigned in a random order. This can be done with this command:" + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "`--solver-options=-randomiseorder`" - ], "metadata": { "id": "Zzg57cEHonBQ" - } + }, + "source": [ + "`--solver-options=-randomiseorder`" + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "Alternatively one can use another solver that uses randomness by default" - ], "metadata": { "id": "qTeTX8s-oqjp" - } + }, + "source": [ + "Alternatively one can use another solver that uses randomness by default" + ] }, { "cell_type": "code", - "source": [ - "%%conjure --solver=minion --solver-options='-randomiseorder'\n", - "\n", - "find weight: function (total, injective) items --> int(1..1000)\n", - "find gain: function (total, injective) items --> int(1..1000)\n", - "find capacity: int(1..5000)" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -589,10 +367,8 @@ "id": "v1vnAK0kouNI", "outputId": "c81ad75f-51f0-4bb8-877c-75bd50d690a5" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{'capacity': 4354,\n", @@ -638,25 +414,32 @@ " '9': 194}}" ] }, + "execution_count": 4, "metadata": {}, - "execution_count": 4 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure --solver=minion --solver-options='-randomiseorder'\n", + "\n", + "find weight: function (total, injective) items --> int(1..1000)\n", + "find gain: function (total, injective) items --> int(1..1000)\n", + "find capacity: int(1..5000)" ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "Now it is starting to look more like a proper instance. At this point we can add some knowledge about the problem to formulate some constraints that will ensure that the instances are not trivial. ie when the sum of all the weights is smaller than the capacity so we can’t put all the objects in the knapsack or when all the objects are heavier than the capacity so that no object can be picked. Thefore we add constraints such as:" - ], "metadata": { "id": "Y3zFC4dTtn-s" - } + }, + "source": [ + "Now it is starting to look more like a proper instance. At this point we can add some knowledge about the problem to formulate some constraints that will ensure that the instances are not trivial. ie when the sum of all the weights is smaller than the capacity so we can’t put all the objects in the knapsack or when all the objects are heavier than the capacity so that no object can be picked. Thefore we add constraints such as:" + ] }, { "cell_type": "code", - "source": [ - "%conjure_clear" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -664,29 +447,22 @@ "id": "xtRJ0LK5ueb3", "outputId": "d277f389-ce6f-4070-e556-42d64da10989" }, - "execution_count": null, "outputs": [ { - "output_type": "stream", "name": "stdout", + "output_type": "stream", "text": [ "Conjure model cleared\n" ] } + ], + "source": [ + "%conjure_clear" ] }, { "cell_type": "code", - "source": [ - "%%conjure\n", - "letting number_items be 20\n", - "letting items be domain int(1..number_items)\n", - "find weight: function (total, injective) items --> int(1..1000)\n", - "find gain: function (total, injective) items --> int(1..1000)\n", - "find capacity: int(1..5000)\n", - "\n", - "such that (sum ([w | (_,w) <- weight]) > capacity*2)," - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -694,10 +470,8 @@ "id": "st_At4HvuFtD", "outputId": "b809637a-5f87-4848-df0f-29c41cf34227" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{'capacity': 43,\n", @@ -743,27 +517,35 @@ " '9': 9}}" ] }, + "execution_count": 26, "metadata": {}, - "execution_count": 26 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure\n", + "letting number_items be 20\n", + "letting items be domain int(1..number_items)\n", + "find weight: function (total, injective) items --> int(1..1000)\n", + "find gain: function (total, injective) items --> int(1..1000)\n", + "find capacity: int(1..5000)\n", + "\n", + "such that (sum ([w | (_,w) <- weight]) > capacity*2)," ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "This means that the sum of all the weights should be greater than twice the capacity of the knapsack. From this we can expect that on average no more than half of the objects will fit in the knapsack. The expression `[w | (_,w) <- weight]` is a list [comprehension](https://en.wikipedia.org/wiki/List_comprehension) that extracts all right hand values of the `weight` function. The underscore character means we do not care about the left hand side values. To ensure that the solver does not take it too far we impose an upper bound using a similar constraint. We impose that the sum of the objects weights 5 times the capacity of the knapsack, so we can expect that only between 20% and 50% of the items will fit in the knapsack in each instance." - ], "metadata": { "id": "XH7Q2h2Qux0G" - } + }, + "source": [ + "This means that the sum of all the weights should be greater than twice the capacity of the knapsack. From this we can expect that on average no more than half of the objects will fit in the knapsack. The expression `[w | (_,w) <- weight]` is a list [comprehension](https://en.wikipedia.org/wiki/List_comprehension) that extracts all right hand values of the `weight` function. The underscore character means we do not care about the left hand side values. To ensure that the solver does not take it too far we impose an upper bound using a similar constraint. We impose that the sum of the objects weights 5 times the capacity of the knapsack, so we can expect that only between 20% and 50% of the items will fit in the knapsack in each instance." + ] }, { "cell_type": "code", - "source": [ - "%%conjure\n", - "\n", - "such that (sum ([w | (_,w) <- weight]) < capacity*5)," - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -771,10 +553,8 @@ "id": "RGBsge0yu-LK", "outputId": "c7baf91c-74b5-4701-89a7-17a123492b5b" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{'capacity': 43,\n", @@ -820,27 +600,30 @@ " '9': 9}}" ] }, + "execution_count": 27, "metadata": {}, - "execution_count": 27 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure\n", + "\n", + "such that (sum ([w | (_,w) <- weight]) < capacity*5)," ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "At this point it will be harder to see specific properties of the instances just by eyeballing the parameters but we can be confident that the properties we have imposed are there. We can add some more constraints to refine the values of the instances for practice/exercise by enforcing that no object is heavier than a third of the knapsack capacity" - ], "metadata": { "id": "UAohhHG1vXFZ" - } + }, + "source": [ + "At this point it will be harder to see specific properties of the instances just by eyeballing the parameters but we can be confident that the properties we have imposed are there. We can add some more constraints to refine the values of the instances for practice/exercise by enforcing that no object is heavier than a third of the knapsack capacity" + ] }, { "cell_type": "code", - "source": [ - "%%conjure\n", - "\n", - "such that forAll (_,w) in weight . w < capacity / 3," - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -848,11 +631,10 @@ "id": "UPeiW9bOvZcJ", "outputId": "70de71bf-c701-4222-9547-fea521c33e47" }, - "execution_count": null, "outputs": [ { - "output_type": "stream", "name": "stderr", + "output_type": "stream", "text": [ "Exception: Error:\n", " Savile Row stdout: Created output file for domain filtering conjure-output/model000001.eprime-minion\n", @@ -868,24 +650,26 @@ "\n" ] } + ], + "source": [ + "%%conjure\n", + "\n", + "such that forAll (_,w) in weight . w < capacity / 3," ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "On top of that we can enfore a constraint on the density of the values in each object by limiting the ratio between the weight and gain of each specific object with:" - ], "metadata": { "id": "cEy6PLNavc_T" - } + }, + "source": [ + "On top of that we can enfore a constraint on the density of the values in each object by limiting the ratio between the weight and gain of each specific object with:" + ] }, { "cell_type": "code", - "source": [ - "%%conjure\n", - "such that forAll element : items .\n", - " gain(element) <= 3*weight(element)" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -893,10 +677,8 @@ "id": "46OeSVrBvhOX", "outputId": "7ef012a2-d030-4dec-e3a8-2d5055042351" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{'capacity': 16,\n", @@ -942,13 +724,23 @@ " '9': 3}}" ] }, + "execution_count": 29, "metadata": {}, - "execution_count": 29 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure\n", + "such that forAll element : items .\n", + " gain(element) <= 3*weight(element)" ] }, { + "attachments": {}, "cell_type": "markdown", + "metadata": { + "id": "kr7LfH5Svrxx" + }, "source": [ "After running all cells, we can take the output solution and run the Knapsack Problem solution on it.\n", "\n", @@ -957,10 +749,23 @@ "If your computer is powerful enough you can try larger values in “letting number_items be 20” (40-50 items will already produce substantially harder instances) Like for other forms of modelling writing instance generators is in large part an art. If this is not your kind of thing and you would like a fully automated system that can produce instances you may check out this [method](https://link.springer.com/chapter/10.1007/978-3-030-30048-7_1)\n", "\n", "(code available [here](https://github.com/stacs-cp/CP2019-InstanceGen))" - ], - "metadata": { - "id": "kr7LfH5Svrxx" - } + ] + } + ], + "metadata": { + "colab": { + "authorship_tag": "ABX9TyOyOIxXu5LVVSWqJoksN5gj", + "include_colab_link": true, + "provenance": [] + }, + "kernelspec": { + "display_name": "Python 3", + "name": "python3" + }, + "language_info": { + "name": "python" } - ] -} \ No newline at end of file + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/docs/tutorials/notebooks/KnapsackProblem.ipynb b/docs/tutorials/notebooks/KnapsackProblem.ipynb index 7ea425b39..3a9ba8042 100644 --- a/docs/tutorials/notebooks/KnapsackProblem.ipynb +++ b/docs/tutorials/notebooks/KnapsackProblem.ipynb @@ -28,7 +28,7 @@ "id": "5I6cwwqhH19R" }, "source": [ - "Original [The Knapsack Problem](https://conjure.readthedocs.io/en/latest/tutorials.html#the-knapsack-problem) by Saad Attieh and Christopher Stone. Adapted by Alex Gallagher." + "Original [The Knapsack Problem](https://conjure.readthedocs.io/en/latest/tutorials/knapsack.html) by Saad Attieh and Christopher Stone. Adapted by Alex Gallagher." ] }, { @@ -90,7 +90,7 @@ "id": "fU4y3zCXMNgX" }, "source": [ - "##Model Explained" + "## Model Explained" ] }, { diff --git a/docs/tutorials/notebooks/NurseRostering.ipynb b/docs/tutorials/notebooks/NurseRostering.ipynb index 248e51e0f..230366d1d 100644 --- a/docs/tutorials/notebooks/NurseRostering.ipynb +++ b/docs/tutorials/notebooks/NurseRostering.ipynb @@ -1,34 +1,38 @@ { "cells": [ { + "attachments": {}, "cell_type": "markdown", "metadata": { - "id": "view-in-github", - "colab_type": "text" + "colab_type": "text", + "id": "view-in-github" }, "source": [ "\"Open" ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "G0mPqC-63XVl" }, "source": [ - "#Nurse Rostering" + "# Nurse Rostering" ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "sT5HA7OR3a_f" }, "source": [ - "Original [Nurse Rostering](https://conjure.readthedocs.io/en/latest/tutorials.html#nurse-rostering) by András Salamon, Nguyen Dang and Saad Attieh. Adapted by Alex Gallagher." + "Original [Nurse Rostering](https://conjure.readthedocs.io/en/latest/tutorials/NurseRostering.html) by András Salamon, Nguyen Dang and Saad Attieh. Adapted by Alex Gallagher." ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "eyp734R43ttT" @@ -52,8 +56,8 @@ }, "outputs": [ { - "output_type": "stream", "name": "stdout", + "output_type": "stream", "text": [ "Installing Conjure...\n", "Conjure: The Automated Constraint Modelling Tool\n", @@ -62,231 +66,18 @@ ] }, { - "output_type": "display_data", "data": { + "application/javascript": "\"use strict\";\n\nCodeMirror.defineMode(\"text/conjure\", function (config) {\n\n var isOperatorChar = /[+\\-*=<>%^\\/]/;\n\n var keywords = {\n \"forall\": true,\n \"allDifferent\": true,\n \"allDiff\": true,\n \"alldifferent_except\": true,\n \"dim\": true,\n \"toSet\": true,\n \"toMSet\": true,\n \"toRelation\": true,\n \"maximising\": true,\n \"minimising\": true,\n \"forAll\": true,\n \"exists\": true,\n \"toInt\": true,\n \"sum\": true,\n \"be\": true,\n \"bijective\": true,\n \"bool\": true,\n \"by\": true,\n \"complete\": true,\n \"defined\": true,\n \"domain\": true,\n \"in\": true,\n \"or\": true,\n \"and\": true,\n \"false\": true,\n \"find\": true,\n \"from\": true,\n \"function\": true,\n \"given\": true,\n \"image\": true,\n \"indexed\": true,\n \"injective\": true,\n \"int\": true,\n \"intersect\": true,\n \"freq\": true,\n \"lambda\": true,\n \"language\": true,\n \"letting\": true,\n \"matrix\": true,\n \"maxNumParts\": true,\n \"maxOccur\": true,\n \"maxPartSize\": true,\n \"maxSize\": true,\n \"minNumParts\": true,\n \"minOccur\": true,\n \"minPartSize\": true,\n \"minSize\": true,\n \"mset\": true,\n \"numParts\": true,\n \"of\": true,\n \"partial\": true,\n \"partition\": true,\n \"partSize\": true,\n \"preImage\": true,\n \"quantifier\": true,\n \"range\": true,\n \"regular\": true,\n \"relation\": true,\n \"representation\": true,\n \"set\": true,\n \"size\": true,\n \"subset\": true,\n \"subsetEq\": true,\n \"such\": true,\n \"supset\": true,\n \"supsetEq\": true,\n \"surjective\": true,\n \"that\": true,\n \"together\": true,\n \"enum\": true,\n \"total\": true,\n \"true\": true,\n \"new\": true,\n \"type\": true,\n \"tuple\": true,\n \"union\": true,\n \"where\": true,\n \"branching\": true,\n \"on\": true\n }; \n var punc = \":;,.(){}[]\";\n\n function tokenBase(stream, state) {\n var ch = stream.next();\n if (ch == '\"') {\n state.tokenize.push(tokenString);\n return tokenString(stream, state);\n }\n if (/[\\d\\.]/.test(ch)) {\n if (ch == \".\") {\n stream.match(/^[0-9]+([eE][\\-+]?[0-9]+)?/);\n } else if (ch == \"0\") {\n stream.match(/^[xX][0-9a-fA-F]+/) || stream.match(/^0[0-7]+/);\n } else {\n stream.match(/^[0-9]*\\.?[0-9]*([eE][\\-+]?[0-9]+)?/);\n }\n return \"number\";\n }\n if (ch == \"/\") {\n if (stream.eat(\"*\")) {\n state.tokenize.push(tokenComment);\n return tokenComment(stream, state);\n }\n }\n if (ch == \"$\") {\n stream.skipToEnd();\n return \"comment\";\n }\n if (isOperatorChar.test(ch)) {\n stream.eatWhile(isOperatorChar);\n return \"operator\";\n }\n if (punc.indexOf(ch) > -1) {\n return \"punctuation\";\n }\n stream.eatWhile(/[\\w\\$_\\xa1-\\uffff]/);\n var cur = stream.current();\n \n if (keywords.propertyIsEnumerable(cur)) {\n return \"keyword\";\n }\n return \"variable\";\n }\n\n function tokenComment(stream, state) {\n var maybeEnd = false, ch;\n while (ch = stream.next()) {\n if (ch == \"/\" && maybeEnd) {\n state.tokenize.pop();\n break;\n }\n maybeEnd = (ch == \"*\");\n }\n return \"comment\";\n }\n\n function tokenUntilClosingParen() {\n var depth = 0;\n return function (stream, state, prev) {\n var inner = tokenBase(stream, state, prev);\n console.log(\"untilClosing\", inner, stream.current());\n if (inner == \"punctuation\") {\n if (stream.current() == \"(\") {\n ++depth;\n } else if (stream.current() == \")\") {\n if (depth == 0) {\n stream.backUp(1)\n state.tokenize.pop()\n return state.tokenize[state.tokenize.length - 1](stream, state)\n } else {\n --depth;\n }\n }\n }\n return inner;\n }\n }\n\n function tokenString(stream, state) {\n var escaped = false, next, end = false;\n while ((next = stream.next()) != null) {\n if (next == '(' && escaped) {\n state.tokenize.push(tokenUntilClosingParen());\n return \"string\";\n }\n if (next == '\"' && !escaped) { end = true; break; }\n escaped = !escaped && next == \"\\\\\";\n }\n if (end || !escaped)\n state.tokenize.pop();\n return \"string\";\n }\n\n return {\n startState: function (basecolumn) {\n return {\n tokenize: []\n };\n },\n\n token: function (stream, state) {\n if (stream.eatSpace()) return null;\n var style = (state.tokenize[state.tokenize.length - 1] || tokenBase)(stream, state);\n console.log(\"token\", style);\n return style;\n },\n\n blockCommentStart: \"/*\",\n blockCommentEnd: \"*/\",\n lineComment: \"$\"\n };\n});\n\n\nCodeMirror.defineMIME(\"text/conjure\", \"text/conjure\");\n\nrequire(['notebook/js/codecell'], function (codecell) {\n codecell.CodeCell.options_default.highlight_modes['magic_text/conjure'] = { 'reg': [/%?%conjure/] };\n Jupyter.notebook.events.one('kernel_ready.Kernel', function () {\n Jupyter.notebook.get_cells().map(function (cell) {\n if (cell.cell_type == 'code') { cell.auto_highlight(); }\n });\n });\n});\n\n", "text/plain": [ "" - ], - "application/javascript": [ - "\"use strict\";\n", - "\n", - "CodeMirror.defineMode(\"text/conjure\", function (config) {\n", - "\n", - " var isOperatorChar = /[+\\-*=<>%^\\/]/;\n", - "\n", - " var keywords = {\n", - " \"forall\": true,\n", - " \"allDifferent\": true,\n", - " \"allDiff\": true,\n", - " \"alldifferent_except\": true,\n", - " \"dim\": true,\n", - " \"toSet\": true,\n", - " \"toMSet\": true,\n", - " \"toRelation\": true,\n", - " \"maximising\": true,\n", - " \"minimising\": true,\n", - " \"forAll\": true,\n", - " \"exists\": true,\n", - " \"toInt\": true,\n", - " \"sum\": true,\n", - " \"be\": true,\n", - " \"bijective\": true,\n", - " \"bool\": true,\n", - " \"by\": true,\n", - " \"complete\": true,\n", - " \"defined\": true,\n", - " \"domain\": true,\n", - " \"in\": true,\n", - " \"or\": true,\n", - " \"and\": true,\n", - " \"false\": true,\n", - " \"find\": true,\n", - " \"from\": true,\n", - " \"function\": true,\n", - " \"given\": true,\n", - " \"image\": true,\n", - " \"indexed\": true,\n", - " \"injective\": true,\n", - " \"int\": true,\n", - " \"intersect\": true,\n", - " \"freq\": true,\n", - " \"lambda\": true,\n", - " \"language\": true,\n", - " \"letting\": true,\n", - " \"matrix\": true,\n", - " \"maxNumParts\": true,\n", - " \"maxOccur\": true,\n", - " \"maxPartSize\": true,\n", - " \"maxSize\": true,\n", - " \"minNumParts\": true,\n", - " \"minOccur\": true,\n", - " \"minPartSize\": true,\n", - " \"minSize\": true,\n", - " \"mset\": true,\n", - " \"numParts\": true,\n", - " \"of\": true,\n", - " \"partial\": true,\n", - " \"partition\": true,\n", - " \"partSize\": true,\n", - " \"preImage\": true,\n", - " \"quantifier\": true,\n", - " \"range\": true,\n", - " \"regular\": true,\n", - " \"relation\": true,\n", - " \"representation\": true,\n", - " \"set\": true,\n", - " \"size\": true,\n", - " \"subset\": true,\n", - " \"subsetEq\": true,\n", - " \"such\": true,\n", - " \"supset\": true,\n", - " \"supsetEq\": true,\n", - " \"surjective\": true,\n", - " \"that\": true,\n", - " \"together\": true,\n", - " \"enum\": true,\n", - " \"total\": true,\n", - " \"true\": true,\n", - " \"new\": true,\n", - " \"type\": true,\n", - " \"tuple\": true,\n", - " \"union\": true,\n", - " \"where\": true,\n", - " \"branching\": true,\n", - " \"on\": true\n", - " }; \n", - " var punc = \":;,.(){}[]\";\n", - "\n", - " function tokenBase(stream, state) {\n", - " var ch = stream.next();\n", - " if (ch == '\"') {\n", - " state.tokenize.push(tokenString);\n", - " return tokenString(stream, state);\n", - " }\n", - " if (/[\\d\\.]/.test(ch)) {\n", - " if (ch == \".\") {\n", - " stream.match(/^[0-9]+([eE][\\-+]?[0-9]+)?/);\n", - " } else if (ch == \"0\") {\n", - " stream.match(/^[xX][0-9a-fA-F]+/) || stream.match(/^0[0-7]+/);\n", - " } else {\n", - " stream.match(/^[0-9]*\\.?[0-9]*([eE][\\-+]?[0-9]+)?/);\n", - " }\n", - " return \"number\";\n", - " }\n", - " if (ch == \"/\") {\n", - " if (stream.eat(\"*\")) {\n", - " state.tokenize.push(tokenComment);\n", - " return tokenComment(stream, state);\n", - " }\n", - " }\n", - " if (ch == \"$\") {\n", - " stream.skipToEnd();\n", - " return \"comment\";\n", - " }\n", - " if (isOperatorChar.test(ch)) {\n", - " stream.eatWhile(isOperatorChar);\n", - " return \"operator\";\n", - " }\n", - " if (punc.indexOf(ch) > -1) {\n", - " return \"punctuation\";\n", - " }\n", - " stream.eatWhile(/[\\w\\$_\\xa1-\\uffff]/);\n", - " var cur = stream.current();\n", - " \n", - " if (keywords.propertyIsEnumerable(cur)) {\n", - " return \"keyword\";\n", - " }\n", - " return \"variable\";\n", - " }\n", - "\n", - " function tokenComment(stream, state) {\n", - " var maybeEnd = false, ch;\n", - " while (ch = stream.next()) {\n", - " if (ch == \"/\" && maybeEnd) {\n", - " state.tokenize.pop();\n", - " break;\n", - " }\n", - " maybeEnd = (ch == \"*\");\n", - " }\n", - " return \"comment\";\n", - " }\n", - "\n", - " function tokenUntilClosingParen() {\n", - " var depth = 0;\n", - " return function (stream, state, prev) {\n", - " var inner = tokenBase(stream, state, prev);\n", - " console.log(\"untilClosing\", inner, stream.current());\n", - " if (inner == \"punctuation\") {\n", - " if (stream.current() == \"(\") {\n", - " ++depth;\n", - " } else if (stream.current() == \")\") {\n", - " if (depth == 0) {\n", - " stream.backUp(1)\n", - " state.tokenize.pop()\n", - " return state.tokenize[state.tokenize.length - 1](stream, state)\n", - " } else {\n", - " --depth;\n", - " }\n", - " }\n", - " }\n", - " return inner;\n", - " }\n", - " }\n", - "\n", - " function tokenString(stream, state) {\n", - " var escaped = false, next, end = false;\n", - " while ((next = stream.next()) != null) {\n", - " if (next == '(' && escaped) {\n", - " state.tokenize.push(tokenUntilClosingParen());\n", - " return \"string\";\n", - " }\n", - " if (next == '\"' && !escaped) { end = true; break; }\n", - " escaped = !escaped && next == \"\\\\\";\n", - " }\n", - " if (end || !escaped)\n", - " state.tokenize.pop();\n", - " return \"string\";\n", - " }\n", - "\n", - " return {\n", - " startState: function (basecolumn) {\n", - " return {\n", - " tokenize: []\n", - " };\n", - " },\n", - "\n", - " token: function (stream, state) {\n", - " if (stream.eatSpace()) return null;\n", - " var style = (state.tokenize[state.tokenize.length - 1] || tokenBase)(stream, state);\n", - " console.log(\"token\", style);\n", - " return style;\n", - " },\n", - "\n", - " blockCommentStart: \"/*\",\n", - " blockCommentEnd: \"*/\",\n", - " lineComment: \"$\"\n", - " };\n", - "});\n", - "\n", - "\n", - "CodeMirror.defineMIME(\"text/conjure\", \"text/conjure\");\n", - "\n", - "require(['notebook/js/codecell'], function (codecell) {\n", - " codecell.CodeCell.options_default.highlight_modes['magic_text/conjure'] = { 'reg': [/%?%conjure/] };\n", - " Jupyter.notebook.events.one('kernel_ready.Kernel', function () {\n", - " Jupyter.notebook.get_cells().map(function (cell) {\n", - " if (cell.cell_type == 'code') { cell.auto_highlight(); }\n", - " });\n", - " });\n", - "});\n", - "\n" ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "stream", "name": "stdout", + "output_type": "stream", "text": [ "Conjure extension is loaded.\n", "For usage help run: %conjure_help\n" @@ -299,15 +90,17 @@ ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "cFk1jIuP38LE" }, "source": [ - "##Initial specification" + "## Initial specification" ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "JwAsti574JRJ" @@ -317,6 +110,7 @@ ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "T1zikM3e9xl-" @@ -358,6 +152,7 @@ ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "jOAzUfPt-lYH" @@ -367,6 +162,7 @@ ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "_7i2Q2GG-utJ" @@ -387,14 +183,14 @@ }, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{}" ] }, + "execution_count": 2, "metadata": {}, - "execution_count": 2 + "output_type": "execute_result" } ], "source": [ @@ -420,6 +216,7 @@ ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "GZWxlTxR_Mc0" @@ -429,15 +226,17 @@ ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "qsGFV5Dv_OOQ" }, "source": [ - "##Changing an overly restrictive assumption" + "## Changing an overly restrictive assumption" ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "fv7fysoh_QtW" @@ -461,8 +260,8 @@ }, "outputs": [ { - "output_type": "stream", "name": "stderr", + "output_type": "stream", "text": [ "Exception: Error:\n", " In a 'such that' statement:\n", @@ -497,6 +296,7 @@ ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "kE06me_J_09p" @@ -510,15 +310,17 @@ ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "0uBBIwlX_9am" }, "source": [ - "##Final model" + "## Final model" ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "6QotfeQu__8C" @@ -528,6 +330,7 @@ ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "ISY-4C0-AGHi" @@ -549,6 +352,7 @@ ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "8LptUFIwAV4v" @@ -558,6 +362,7 @@ ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "Lg0TdcXwAbx_" @@ -601,6 +406,7 @@ ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "KvbAlL_O_hrQ" @@ -613,16 +419,16 @@ "cell_type": "code", "execution_count": 6, "metadata": { - "id": "vm7aSCAp_2LF", "colab": { "base_uri": "https://localhost:8080/" }, + "id": "vm7aSCAp_2LF", "outputId": "d7adbd4e-54cd-465d-bb97-bcd8f9c5558f" }, "outputs": [ { - "output_type": "stream", "name": "stdout", + "output_type": "stream", "text": [ "[[[1, 2], 'Early'], [[1, 3], 'Early'], [[1, 4], 'Late'], [[1, 5], 'Late'], [[2, 2], 'Early'], [[2, 3], 'Late'], [[2, 4], 'Night'], [[2, 5], 'Night'], [[3, 2], 'Early'], [[3, 3], 'Late'], [[3, 4], 'Night'], [[4, 5], 'Night'], [[5, 2], 'Early'], [[5, 3], 'Late'], [[5, 4], 'Night'], [[5, 5], 'Night'], [[6, 1], 'Early'], [[6, 2], 'Early'], [[6, 3], 'Late'], [[6, 4], 'Night'], [[7, 4], 'Night'], [[7, 5], 'Late']]\n" ] @@ -633,6 +439,7 @@ ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "vZZnYwBxANRW" @@ -653,7 +460,6 @@ }, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{'roster': [[[1, 2], 'Early'],\n", @@ -680,8 +486,9 @@ " [[7, 5], 'Late']]}" ] }, + "execution_count": 5, "metadata": {}, - "execution_count": 5 + "output_type": "execute_result" } ], "source": [ @@ -709,6 +516,7 @@ ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "jav2lI9SA1mf" @@ -718,6 +526,7 @@ ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "OZwGGTmKPqOQ" @@ -727,6 +536,7 @@ ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "6XoriFZKPu0L" @@ -750,6 +560,7 @@ ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "-1_QNf5HTYz-" @@ -770,7 +581,6 @@ }, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{'roster': [[[1, 2], 'Early'],\n", @@ -797,8 +607,9 @@ " [[7, 5], 'Late']]}" ] }, + "execution_count": 8, "metadata": {}, - "execution_count": 8 + "output_type": "execute_result" } ], "source": [ @@ -826,15 +637,17 @@ ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "oEO7p5otBLGj" }, "source": [ - "##Representations" + "## Visualisations" ] }, { + "attachments": {}, "cell_type": "markdown", "metadata": { "id": "vpX_tZdQBOGH" @@ -856,15 +669,553 @@ }, "outputs": [ { - "output_type": "execute_result", "data": { - "image/svg+xml": "\n\n\n\n\n\nparent\n\n\ncluster1\n\nDay 1\n\n\ncluster2\n\nDay 2\n\n\ncluster3\n\nDay 3\n\n\ncluster4\n\nDay 4\n\n\ncluster5\n\nDay 5\n\n\ncluster6\n\nDay 6\n\n\ncluster7\n\nDay 7\n\n\n\nLate1\n\n\n\n\nLate\n\n\n\n0\n\n\n\n\nNurse ID: 4\n\n\n\nLate1->0\n\n\n\n\n\n1\n\n\n\n\nNurse ID: 5\n\n\n\nLate1->1\n\n\n\n\n\nEarly1\n\n\n\n\nEarly\n\n\n\n2\n\n\n\n\nNurse ID: 2\n\n\n\nEarly1->2\n\n\n\n\n\n3\n\n\n\n\nNurse ID: 3\n\n\n\nEarly1->3\n\n\n\n\n\nEarly2\n\n\n\n\nEarly\n\n\n\n\nNight2\n\n\n\n\nNight\n\n\n\n4\n\n\n\n\nNurse ID: 4\n\n\n\nNight2->4\n\n\n\n\n\n5\n\n\n\n\nNurse ID: 5\n\n\n\nNight2->5\n\n\n\n\n\nLate2\n\n\n\n\nLate\n\n\n\n6\n\n\n\n\nNurse ID: 3\n\n\n\nLate2->6\n\n\n\n\n\n7\n\n\n\n\nNurse ID: 2\n\n\n\nEarly2->7\n\n\n\n\n\nEarly3\n\n\n\n\nEarly\n\n\n\n\nNight3\n\n\n\n\nNight\n\n\n\n8\n\n\n\n\nNurse ID: 4\n\n\n\nNight3->8\n\n\n\n\n\nLate3\n\n\n\n\nLate\n\n\n\n9\n\n\n\n\nNurse ID: 3\n\n\n\nLate3->9\n\n\n\n\n\n10\n\n\n\n\nNurse ID: 2\n\n\n\nEarly3->10\n\n\n\n\n\nNight4\n\n\n\n\nNight\n\n\n\n\n11\n\n\n\n\nNurse ID: 5\n\n\n\nNight4->11\n\n\n\n\n\nEarly5\n\n\n\n\nEarly\n\n\n\n\nNight5\n\n\n\n\nNight\n\n\n\n12\n\n\n\n\nNurse ID: 4\n\n\n\nNight5->12\n\n\n\n\n\n13\n\n\n\n\nNurse ID: 5\n\n\n\nNight5->13\n\n\n\n\n\nLate6\n\n\n\n\nLate\n\n\n\n\nLate5\n\n\n\n\nLate\n\n\n\n14\n\n\n\n\nNurse ID: 3\n\n\n\nLate5->14\n\n\n\n\n\n15\n\n\n\n\nNurse ID: 2\n\n\n\nEarly5->15\n\n\n\n\n\nNight6\n\n\n\n\nNight\n\n\n\n16\n\n\n\n\nNurse ID: 4\n\n\n\nNight6->16\n\n\n\n\n\n17\n\n\n\n\nNurse ID: 3\n\n\n\nLate6->17\n\n\n\n\n\nEarly6\n\n\n\n\nEarly\n\n\n\n18\n\n\n\n\nNurse ID: 1\n\n\n\nEarly6->18\n\n\n\n\n\n19\n\n\n\n\nNurse ID: 2\n\n\n\nEarly6->19\n\n\n\n\n\nLate7\n\n\n\n\nLate\n\n\n\n\nNight7\n\n\n\n\nNight\n\n\n\n20\n\n\n\n\nNurse ID: 4\n\n\n\nNight7->20\n\n\n\n\n\n21\n\n\n\n\nNurse ID: 5\n\n\n\nLate7->21\n\n\n\n\n\n", + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "parent\n", + "\n", + "\n", + "cluster1\n", + "\n", + "Day 1\n", + "\n", + "\n", + "cluster2\n", + "\n", + "Day 2\n", + "\n", + "\n", + "cluster3\n", + "\n", + "Day 3\n", + "\n", + "\n", + "cluster4\n", + "\n", + "Day 4\n", + "\n", + "\n", + "cluster5\n", + "\n", + "Day 5\n", + "\n", + "\n", + "cluster6\n", + "\n", + "Day 6\n", + "\n", + "\n", + "cluster7\n", + "\n", + "Day 7\n", + "\n", + "\n", + "\n", + "Late1\n", + "\n", + "\n", + "\n", + "\n", + "Late\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 4\n", + "\n", + "\n", + "\n", + "Late1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 5\n", + "\n", + "\n", + "\n", + "Late1->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Early1\n", + "\n", + "\n", + "\n", + "\n", + "Early\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 2\n", + "\n", + "\n", + "\n", + "Early1->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 3\n", + "\n", + "\n", + "\n", + "Early1->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Early2\n", + "\n", + "\n", + "\n", + "\n", + "Early\n", + "\n", + "\n", + "\n", + "\n", + "Night2\n", + "\n", + "\n", + "\n", + "\n", + "Night\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 4\n", + "\n", + "\n", + "\n", + "Night2->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 5\n", + "\n", + "\n", + "\n", + "Night2->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Late2\n", + "\n", + "\n", + "\n", + "\n", + "Late\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 3\n", + "\n", + "\n", + "\n", + "Late2->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 2\n", + "\n", + "\n", + "\n", + "Early2->7\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Early3\n", + "\n", + "\n", + "\n", + "\n", + "Early\n", + "\n", + "\n", + "\n", + "\n", + "Night3\n", + "\n", + "\n", + "\n", + "\n", + "Night\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 4\n", + "\n", + "\n", + "\n", + "Night3->8\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Late3\n", + "\n", + "\n", + "\n", + "\n", + "Late\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 3\n", + "\n", + "\n", + "\n", + "Late3->9\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "10\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 2\n", + "\n", + "\n", + "\n", + "Early3->10\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Night4\n", + "\n", + "\n", + "\n", + "\n", + "Night\n", + "\n", + "\n", + "\n", + "\n", + "11\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 5\n", + "\n", + "\n", + "\n", + "Night4->11\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Early5\n", + "\n", + "\n", + "\n", + "\n", + "Early\n", + "\n", + "\n", + "\n", + "\n", + "Night5\n", + "\n", + "\n", + "\n", + "\n", + "Night\n", + "\n", + "\n", + "\n", + "12\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 4\n", + "\n", + "\n", + "\n", + "Night5->12\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "13\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 5\n", + "\n", + "\n", + "\n", + "Night5->13\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Late6\n", + "\n", + "\n", + "\n", + "\n", + "Late\n", + "\n", + "\n", + "\n", + "\n", + "Late5\n", + "\n", + "\n", + "\n", + "\n", + "Late\n", + "\n", + "\n", + "\n", + "14\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 3\n", + "\n", + "\n", + "\n", + "Late5->14\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "15\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 2\n", + "\n", + "\n", + "\n", + "Early5->15\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Night6\n", + "\n", + "\n", + "\n", + "\n", + "Night\n", + "\n", + "\n", + "\n", + "16\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 4\n", + "\n", + "\n", + "\n", + "Night6->16\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "17\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 3\n", + "\n", + "\n", + "\n", + "Late6->17\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Early6\n", + "\n", + "\n", + "\n", + "\n", + "Early\n", + "\n", + "\n", + "\n", + "18\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 1\n", + "\n", + "\n", + "\n", + "Early6->18\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "19\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 2\n", + "\n", + "\n", + "\n", + "Early6->19\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Late7\n", + "\n", + "\n", + "\n", + "\n", + "Late\n", + "\n", + "\n", + "\n", + "\n", + "Night7\n", + "\n", + "\n", + "\n", + "\n", + "Night\n", + "\n", + "\n", + "\n", + "20\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 4\n", + "\n", + "\n", + "\n", + "Night7->20\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "21\n", + "\n", + "\n", + "\n", + "\n", + "Nurse ID: 5\n", + "\n", + "\n", + "\n", + "Late7->21\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], "text/plain": [ "" ] }, + "execution_count": 24, "metadata": {}, - "execution_count": 24 + "output_type": "execute_result" } ], "source": [ @@ -883,15 +1234,15 @@ "for day in range (1, nDays+1):\n", " with p.subgraph(name='cluster'+str(day), node_attr={'shape': 'box3d', 'color': 'purple', 'style':'rounded'}) as c:\n", " for item in roster:\n", - " #if it is the selected day\n", + " # if it is the selected day\n", " if item[0][0] == day:\n", - " #add the time of day if it doesn't exist already\n", + " # add the time of day if it doesn't exist already\n", " c.node(str(item[1])+str(day), item[1])\n", - " #print(str(item[1])+str(day))\n", - " #add the nurse\n", + " # print(str(item[1])+str(day))\n", + " # add the nurse\n", " c.node(str(id), \"Nurse ID: \" + str(item[0][1]), color='orange')\n", - " #print(str(id), \"nurse: \", str(item[0][1]))\n", - " #add the edge\n", + " # print(str(id), \"nurse: \", str(item[0][1]))\n", + " # add the edge\n", " edges.append([str(item[1])+str(day), str(id)])\n", " id=id+1\n", " c.attr(label=\"Day \"+str(day))\n", @@ -912,36 +1263,608 @@ ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "We can also display the roster as the timetable for each nurse:" - ], "metadata": { "id": "LMSsgljnrY8m" - } + }, + "source": [ + "We can also display the roster as the timetable for each nurse:" + ] }, { "cell_type": "code", "execution_count": 10, "metadata": { - "id": "d-bgk-0-PITw", "colab": { "base_uri": "https://localhost:8080/", "height": 1000 }, + "id": "d-bgk-0-PITw", "outputId": "0ec19cd7-3ede-47c0-b8b9-ce5e5a29b537" }, "outputs": [ { - "output_type": "execute_result", "data": { - "image/svg+xml": "\n\n\n\n\n\nparent\n\n\ncluster1\n\nNurse 1\n\n\ncluster2\n\nNurse 2\n\n\ncluster3\n\nNurse 3\n\n\ncluster4\n\nNurse 4\n\n\ncluster5\n\nNurse 5\n\n\n\n0\n\n\n\n\nDay 6\n\n\n\n0Early1\n\n\n\n\nEarly\n\n\n\n0->0Early1\n\n\n\n\n\n5\n\n\n\n\nDay 1\n\n\n\n\n1\n\n\n\n\nDay 6\n\n\n\n1Early2\n\n\n\n\nEarly\n\n\n\n1->1Early2\n\n\n\n\n\n2\n\n\n\n\nDay 5\n\n\n\n2Early2\n\n\n\n\nEarly\n\n\n\n2->2Early2\n\n\n\n\n\n3\n\n\n\n\nDay 3\n\n\n\n3Early2\n\n\n\n\nEarly\n\n\n\n3->3Early2\n\n\n\n\n\n4\n\n\n\n\nDay 2\n\n\n\n4Early2\n\n\n\n\nEarly\n\n\n\n4->4Early2\n\n\n\n\n\n5Early2\n\n\n\n\nEarly\n\n\n\n5->5Early2\n\n\n\n\n\n10\n\n\n\n\nDay 1\n\n\n\n\n6\n\n\n\n\nDay 6\n\n\n\n6Late3\n\n\n\n\nLate\n\n\n\n6->6Late3\n\n\n\n\n\n7\n\n\n\n\nDay 5\n\n\n\n7Late3\n\n\n\n\nLate\n\n\n\n7->7Late3\n\n\n\n\n\n8\n\n\n\n\nDay 3\n\n\n\n8Late3\n\n\n\n\nLate\n\n\n\n8->8Late3\n\n\n\n\n\n9\n\n\n\n\nDay 2\n\n\n\n9Late3\n\n\n\n\nLate\n\n\n\n9->9Late3\n\n\n\n\n\n10Early3\n\n\n\n\nEarly\n\n\n\n10->10Early3\n\n\n\n\n\n16\n\n\n\n\nDay 1\n\n\n\n\n11\n\n\n\n\nDay 7\n\n\n\n11Night4\n\n\n\n\nNight\n\n\n\n11->11Night4\n\n\n\n\n\n12\n\n\n\n\nDay 6\n\n\n\n12Night4\n\n\n\n\nNight\n\n\n\n12->12Night4\n\n\n\n\n\n13\n\n\n\n\nDay 5\n\n\n\n13Night4\n\n\n\n\nNight\n\n\n\n13->13Night4\n\n\n\n\n\n14\n\n\n\n\nDay 3\n\n\n\n14Night4\n\n\n\n\nNight\n\n\n\n14->14Night4\n\n\n\n\n\n15\n\n\n\n\nDay 2\n\n\n\n15Night4\n\n\n\n\nNight\n\n\n\n15->15Night4\n\n\n\n\n\n16Late4\n\n\n\n\nLate\n\n\n\n16->16Late4\n\n\n\n\n\n21\n\n\n\n\nDay 1\n\n\n\n\n17\n\n\n\n\nDay 7\n\n\n\n17Late5\n\n\n\n\nLate\n\n\n\n17->17Late5\n\n\n\n\n\n18\n\n\n\n\nDay 5\n\n\n\n18Night5\n\n\n\n\nNight\n\n\n\n18->18Night5\n\n\n\n\n\n19\n\n\n\n\nDay 4\n\n\n\n19Night5\n\n\n\n\nNight\n\n\n\n19->19Night5\n\n\n\n\n\n20\n\n\n\n\nDay 2\n\n\n\n20Night5\n\n\n\n\nNight\n\n\n\n20->20Night5\n\n\n\n\n\n21Late5\n\n\n\n\nLate\n\n\n\n21->21Late5\n\n\n\n\n\n", + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "parent\n", + "\n", + "\n", + "cluster1\n", + "\n", + "Nurse 1\n", + "\n", + "\n", + "cluster2\n", + "\n", + "Nurse 2\n", + "\n", + "\n", + "cluster3\n", + "\n", + "Nurse 3\n", + "\n", + "\n", + "cluster4\n", + "\n", + "Nurse 4\n", + "\n", + "\n", + "cluster5\n", + "\n", + "Nurse 5\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "\n", + "Day 6\n", + "\n", + "\n", + "\n", + "0Early1\n", + "\n", + "\n", + "\n", + "\n", + "Early\n", + "\n", + "\n", + "\n", + "0->0Early1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "\n", + "Day 1\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "Day 6\n", + "\n", + "\n", + "\n", + "1Early2\n", + "\n", + "\n", + "\n", + "\n", + "Early\n", + "\n", + "\n", + "\n", + "1->1Early2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "\n", + "Day 5\n", + "\n", + "\n", + "\n", + "2Early2\n", + "\n", + "\n", + "\n", + "\n", + "Early\n", + "\n", + "\n", + "\n", + "2->2Early2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "\n", + "Day 3\n", + "\n", + "\n", + "\n", + "3Early2\n", + "\n", + "\n", + "\n", + "\n", + "Early\n", + "\n", + "\n", + "\n", + "3->3Early2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "\n", + "Day 2\n", + "\n", + "\n", + "\n", + "4Early2\n", + "\n", + "\n", + "\n", + "\n", + "Early\n", + "\n", + "\n", + "\n", + "4->4Early2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "5Early2\n", + "\n", + "\n", + "\n", + "\n", + "Early\n", + "\n", + "\n", + "\n", + "5->5Early2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "10\n", + "\n", + "\n", + "\n", + "\n", + "Day 1\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "\n", + "Day 6\n", + "\n", + "\n", + "\n", + "6Late3\n", + "\n", + "\n", + "\n", + "\n", + "Late\n", + "\n", + "\n", + "\n", + "6->6Late3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "\n", + "Day 5\n", + "\n", + "\n", + "\n", + "7Late3\n", + "\n", + "\n", + "\n", + "\n", + "Late\n", + "\n", + "\n", + "\n", + "7->7Late3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "\n", + "Day 3\n", + "\n", + "\n", + "\n", + "8Late3\n", + "\n", + "\n", + "\n", + "\n", + "Late\n", + "\n", + "\n", + "\n", + "8->8Late3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "\n", + "\n", + "Day 2\n", + "\n", + "\n", + "\n", + "9Late3\n", + "\n", + "\n", + "\n", + "\n", + "Late\n", + "\n", + "\n", + "\n", + "9->9Late3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "10Early3\n", + "\n", + "\n", + "\n", + "\n", + "Early\n", + "\n", + "\n", + "\n", + "10->10Early3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "16\n", + "\n", + "\n", + "\n", + "\n", + "Day 1\n", + "\n", + "\n", + "\n", + "\n", + "11\n", + "\n", + "\n", + "\n", + "\n", + "Day 7\n", + "\n", + "\n", + "\n", + "11Night4\n", + "\n", + "\n", + "\n", + "\n", + "Night\n", + "\n", + "\n", + "\n", + "11->11Night4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "12\n", + "\n", + "\n", + "\n", + "\n", + "Day 6\n", + "\n", + "\n", + "\n", + "12Night4\n", + "\n", + "\n", + "\n", + "\n", + "Night\n", + "\n", + "\n", + "\n", + "12->12Night4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "13\n", + "\n", + "\n", + "\n", + "\n", + "Day 5\n", + "\n", + "\n", + "\n", + "13Night4\n", + "\n", + "\n", + "\n", + "\n", + "Night\n", + "\n", + "\n", + "\n", + "13->13Night4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "14\n", + "\n", + "\n", + "\n", + "\n", + "Day 3\n", + "\n", + "\n", + "\n", + "14Night4\n", + "\n", + "\n", + "\n", + "\n", + "Night\n", + "\n", + "\n", + "\n", + "14->14Night4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "15\n", + "\n", + "\n", + "\n", + "\n", + "Day 2\n", + "\n", + "\n", + "\n", + "15Night4\n", + "\n", + "\n", + "\n", + "\n", + "Night\n", + "\n", + "\n", + "\n", + "15->15Night4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "16Late4\n", + "\n", + "\n", + "\n", + "\n", + "Late\n", + "\n", + "\n", + "\n", + "16->16Late4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "21\n", + "\n", + "\n", + "\n", + "\n", + "Day 1\n", + "\n", + "\n", + "\n", + "\n", + "17\n", + "\n", + "\n", + "\n", + "\n", + "Day 7\n", + "\n", + "\n", + "\n", + "17Late5\n", + "\n", + "\n", + "\n", + "\n", + "Late\n", + "\n", + "\n", + "\n", + "17->17Late5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "18\n", + "\n", + "\n", + "\n", + "\n", + "Day 5\n", + "\n", + "\n", + "\n", + "18Night5\n", + "\n", + "\n", + "\n", + "\n", + "Night\n", + "\n", + "\n", + "\n", + "18->18Night5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "19\n", + "\n", + "\n", + "\n", + "\n", + "Day 4\n", + "\n", + "\n", + "\n", + "19Night5\n", + "\n", + "\n", + "\n", + "\n", + "Night\n", + "\n", + "\n", + "\n", + "19->19Night5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "20\n", + "\n", + "\n", + "\n", + "\n", + "Day 2\n", + "\n", + "\n", + "\n", + "20Night5\n", + "\n", + "\n", + "\n", + "\n", + "Night\n", + "\n", + "\n", + "\n", + "20->20Night5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "21Late5\n", + "\n", + "\n", + "\n", + "\n", + "Late\n", + "\n", + "\n", + "\n", + "21->21Late5\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], "text/plain": [ "" ] }, + "execution_count": 10, "metadata": {}, - "execution_count": 10 + "output_type": "execute_result" } ], "source": [ @@ -960,16 +1883,16 @@ " with p.subgraph(name='cluster'+str(nurse), node_attr={'shape': 'box3d', 'color': 'purple', 'style':'rounded'}) as c:\n", " \n", " for item in roster:\n", - " #if it is the selected nurse\n", + " # if it is the selected nurse\n", " if item[0][1] == nurse:\n", " \n", - " #add the day\n", + " # add the day\n", " c.node(str(id), \"Day \" + str(item[0][0]), color='orange')\n", "\n", - " #add the time of day\n", + " # add the time of day\n", " c.node((str(id) + str(item[1]))+str(nurse), item[1])\n", " \n", - " #add the edge\n", + " # add the edge\n", " edges.append([str(id), (str(id) + str(item[1]))+str(nurse)])\n", " id=id+1\n", " c.attr(label=\"Nurse \"+str(nurse))\n", @@ -995,9 +1918,9 @@ "collapsed_sections": [ "qsGFV5Dv_OOQ" ], + "include_colab_link": true, "provenance": [], - "toc_visible": true, - "include_colab_link": true + "toc_visible": true }, "kernelspec": { "display_name": "Python 3", diff --git a/docs/tutorials/notebooks/Semigroups,_Monoids_and_Groups.ipynb b/docs/tutorials/notebooks/Semigroups,_Monoids_and_Groups.ipynb index 6b383c8bf..dcddcd765 100644 --- a/docs/tutorials/notebooks/Semigroups,_Monoids_and_Groups.ipynb +++ b/docs/tutorials/notebooks/Semigroups,_Monoids_and_Groups.ipynb @@ -1,64 +1,49 @@ { - "nbformat": 4, - "nbformat_minor": 0, - "metadata": { - "colab": { - "provenance": [], - "authorship_tag": "ABX9TyNmwuGfH/vOYeP0Tj5vUcu/", - "include_colab_link": true - }, - "kernelspec": { - "name": "python3", - "display_name": "Python 3" - }, - "language_info": { - "name": "python" - } - }, "cells": [ { + "attachments": {}, "cell_type": "markdown", "metadata": { - "id": "view-in-github", - "colab_type": "text" + "colab_type": "text", + "id": "view-in-github" }, "source": [ "\"Open" ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "# Semigroups, Monoids and Groups" - ], "metadata": { "id": "tlwA1gWxaq7u" - } + }, + "source": [ + "# Semigroups, Monoids and Groups" + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "Original [Semigroups, Monoids and Groups](https://conjure.readthedocs.io/en/latest/tutorials.html#semigroups-monoids-and-groups) by Chris Jefferson and Alice Lynch. Adapted by Alex Gallagher." - ], "metadata": { "id": "3kKmC_37a2uo" - } + }, + "source": [ + "Original [Semigroups, Monoids and Groups](https://conjure.readthedocs.io/en/latest/tutorials/Groups.html) by Chris Jefferson and Alice Lynch. Adapted by Alex Gallagher." + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "This tutorial discusses how to model semigroups, monoids and groups in Essence." - ], "metadata": { "id": "Tly_igpYbNYM" - } + }, + "source": [ + "This tutorial discusses how to model semigroups, monoids and groups in Essence." + ] }, { "cell_type": "code", - "source": [ - "!source <(curl -s https://raw.githubusercontent.com/conjure-cp/conjure-notebook/v0.0.2/scripts/install-colab.sh)\n", - "%load_ext conjure" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/", @@ -67,11 +52,10 @@ "id": "0RYHwN9UcZ0A", "outputId": "a740cb25-36a7-4a06-95bd-9a546aa001ea" }, - "execution_count": null, "outputs": [ { - "output_type": "stream", "name": "stdout", + "output_type": "stream", "text": [ " % Total % Received % Xferd Average Speed Time Time Time Current\n", " Dload Upload Total Spent Left Speed\n", @@ -83,291 +67,79 @@ ] }, { - "output_type": "display_data", "data": { + "application/javascript": "\"use strict\";\n\nCodeMirror.defineMode(\"text/conjure\", function (config) {\n\n var isOperatorChar = /[+\\-*=<>%^\\/]/;\n\n var keywords = {\n \"forall\": true,\n \"allDifferent\": true,\n \"allDiff\": true,\n \"alldifferent_except\": true,\n \"dim\": true,\n \"toSet\": true,\n \"toMSet\": true,\n \"toRelation\": true,\n \"maximising\": true,\n \"minimising\": true,\n \"forAll\": true,\n \"exists\": true,\n \"toInt\": true,\n \"sum\": true,\n \"be\": true,\n \"bijective\": true,\n \"bool\": true,\n \"by\": true,\n \"complete\": true,\n \"defined\": true,\n \"domain\": true,\n \"in\": true,\n \"or\": true,\n \"and\": true,\n \"false\": true,\n \"find\": true,\n \"from\": true,\n \"function\": true,\n \"given\": true,\n \"image\": true,\n \"indexed\": true,\n \"injective\": true,\n \"int\": true,\n \"intersect\": true,\n \"freq\": true,\n \"lambda\": true,\n \"language\": true,\n \"letting\": true,\n \"matrix\": true,\n \"maxNumParts\": true,\n \"maxOccur\": true,\n \"maxPartSize\": true,\n \"maxSize\": true,\n \"minNumParts\": true,\n \"minOccur\": true,\n \"minPartSize\": true,\n \"minSize\": true,\n \"mset\": true,\n \"numParts\": true,\n \"of\": true,\n \"partial\": true,\n \"partition\": true,\n \"partSize\": true,\n \"preImage\": true,\n \"quantifier\": true,\n \"range\": true,\n \"regular\": true,\n \"relation\": true,\n \"representation\": true,\n \"set\": true,\n \"size\": true,\n \"subset\": true,\n \"subsetEq\": true,\n \"such\": true,\n \"supset\": true,\n \"supsetEq\": true,\n \"surjective\": true,\n \"that\": true,\n \"together\": true,\n \"enum\": true,\n \"total\": true,\n \"true\": true,\n \"new\": true,\n \"type\": true,\n \"tuple\": true,\n \"union\": true,\n \"where\": true,\n \"branching\": true,\n \"on\": true\n }; \n var punc = \":;,.(){}[]\";\n\n function tokenBase(stream, state) {\n var ch = stream.next();\n if (ch == '\"') {\n state.tokenize.push(tokenString);\n return tokenString(stream, state);\n }\n if (/[\\d\\.]/.test(ch)) {\n if (ch == \".\") {\n stream.match(/^[0-9]+([eE][\\-+]?[0-9]+)?/);\n } else if (ch == \"0\") {\n stream.match(/^[xX][0-9a-fA-F]+/) || stream.match(/^0[0-7]+/);\n } else {\n stream.match(/^[0-9]*\\.?[0-9]*([eE][\\-+]?[0-9]+)?/);\n }\n return \"number\";\n }\n if (ch == \"/\") {\n if (stream.eat(\"*\")) {\n state.tokenize.push(tokenComment);\n return tokenComment(stream, state);\n }\n }\n if (ch == \"$\") {\n stream.skipToEnd();\n return \"comment\";\n }\n if (isOperatorChar.test(ch)) {\n stream.eatWhile(isOperatorChar);\n return \"operator\";\n }\n if (punc.indexOf(ch) > -1) {\n return \"punctuation\";\n }\n stream.eatWhile(/[\\w\\$_\\xa1-\\uffff]/);\n var cur = stream.current();\n \n if (keywords.propertyIsEnumerable(cur)) {\n return \"keyword\";\n }\n return \"variable\";\n }\n\n function tokenComment(stream, state) {\n var maybeEnd = false, ch;\n while (ch = stream.next()) {\n if (ch == \"/\" && maybeEnd) {\n state.tokenize.pop();\n break;\n }\n maybeEnd = (ch == \"*\");\n }\n return \"comment\";\n }\n\n function tokenUntilClosingParen() {\n var depth = 0;\n return function (stream, state, prev) {\n var inner = tokenBase(stream, state, prev);\n console.log(\"untilClosing\", inner, stream.current());\n if (inner == \"punctuation\") {\n if (stream.current() == \"(\") {\n ++depth;\n } else if (stream.current() == \")\") {\n if (depth == 0) {\n stream.backUp(1)\n state.tokenize.pop()\n return state.tokenize[state.tokenize.length - 1](stream, state)\n } else {\n --depth;\n }\n }\n }\n return inner;\n }\n }\n\n function tokenString(stream, state) {\n var escaped = false, next, end = false;\n while ((next = stream.next()) != null) {\n if (next == '(' && escaped) {\n state.tokenize.push(tokenUntilClosingParen());\n return \"string\";\n }\n if (next == '\"' && !escaped) { end = true; break; }\n escaped = !escaped && next == \"\\\\\";\n }\n if (end || !escaped)\n state.tokenize.pop();\n return \"string\";\n }\n\n return {\n startState: function (basecolumn) {\n return {\n tokenize: []\n };\n },\n\n token: function (stream, state) {\n if (stream.eatSpace()) return null;\n var style = (state.tokenize[state.tokenize.length - 1] || tokenBase)(stream, state);\n console.log(\"token\", style);\n return style;\n },\n\n blockCommentStart: \"/*\",\n blockCommentEnd: \"*/\",\n lineComment: \"$\"\n };\n});\n\n\nCodeMirror.defineMIME(\"text/conjure\", \"text/conjure\");\n\nrequire(['notebook/js/codecell'], function (codecell) {\n codecell.CodeCell.options_default.highlight_modes['magic_text/conjure'] = { 'reg': [/%?%conjure/] };\n Jupyter.notebook.events.one('kernel_ready.Kernel', function () {\n Jupyter.notebook.get_cells().map(function (cell) {\n if (cell.cell_type == 'code') { cell.auto_highlight(); }\n });\n });\n});\n\n", "text/plain": [ "" - ], - "application/javascript": [ - "\"use strict\";\n", - "\n", - "CodeMirror.defineMode(\"text/conjure\", function (config) {\n", - "\n", - " var isOperatorChar = /[+\\-*=<>%^\\/]/;\n", - "\n", - " var keywords = {\n", - " \"forall\": true,\n", - " \"allDifferent\": true,\n", - " \"allDiff\": true,\n", - " \"alldifferent_except\": true,\n", - " \"dim\": true,\n", - " \"toSet\": true,\n", - " \"toMSet\": true,\n", - " \"toRelation\": true,\n", - " \"maximising\": true,\n", - " \"minimising\": true,\n", - " \"forAll\": true,\n", - " \"exists\": true,\n", - " \"toInt\": true,\n", - " \"sum\": true,\n", - " \"be\": true,\n", - " \"bijective\": true,\n", - " \"bool\": true,\n", - " \"by\": true,\n", - " \"complete\": true,\n", - " \"defined\": true,\n", - " \"domain\": true,\n", - " \"in\": true,\n", - " \"or\": true,\n", - " \"and\": true,\n", - " \"false\": true,\n", - " \"find\": true,\n", - " \"from\": true,\n", - " \"function\": true,\n", - " \"given\": true,\n", - " \"image\": true,\n", - " \"indexed\": true,\n", - " \"injective\": true,\n", - " \"int\": true,\n", - " \"intersect\": true,\n", - " \"freq\": true,\n", - " \"lambda\": true,\n", - " \"language\": true,\n", - " \"letting\": true,\n", - " \"matrix\": true,\n", - " \"maxNumParts\": true,\n", - " \"maxOccur\": true,\n", - " \"maxPartSize\": true,\n", - " \"maxSize\": true,\n", - " \"minNumParts\": true,\n", - " \"minOccur\": true,\n", - " \"minPartSize\": true,\n", - " \"minSize\": true,\n", - " \"mset\": true,\n", - " \"numParts\": true,\n", - " \"of\": true,\n", - " \"partial\": true,\n", - " \"partition\": true,\n", - " \"partSize\": true,\n", - " \"preImage\": true,\n", - " \"quantifier\": true,\n", - " \"range\": true,\n", - " \"regular\": true,\n", - " \"relation\": true,\n", - " \"representation\": true,\n", - " \"set\": true,\n", - " \"size\": true,\n", - " \"subset\": true,\n", - " \"subsetEq\": true,\n", - " \"such\": true,\n", - " \"supset\": true,\n", - " \"supsetEq\": true,\n", - " \"surjective\": true,\n", - " \"that\": true,\n", - " \"together\": true,\n", - " \"enum\": true,\n", - " \"total\": true,\n", - " \"true\": true,\n", - " \"new\": true,\n", - " \"type\": true,\n", - " \"tuple\": true,\n", - " \"union\": true,\n", - " \"where\": true,\n", - " \"branching\": true,\n", - " \"on\": true\n", - " }; \n", - " var punc = \":;,.(){}[]\";\n", - "\n", - " function tokenBase(stream, state) {\n", - " var ch = stream.next();\n", - " if (ch == '\"') {\n", - " state.tokenize.push(tokenString);\n", - " return tokenString(stream, state);\n", - " }\n", - " if (/[\\d\\.]/.test(ch)) {\n", - " if (ch == \".\") {\n", - " stream.match(/^[0-9]+([eE][\\-+]?[0-9]+)?/);\n", - " } else if (ch == \"0\") {\n", - " stream.match(/^[xX][0-9a-fA-F]+/) || stream.match(/^0[0-7]+/);\n", - " } else {\n", - " stream.match(/^[0-9]*\\.?[0-9]*([eE][\\-+]?[0-9]+)?/);\n", - " }\n", - " return \"number\";\n", - " }\n", - " if (ch == \"/\") {\n", - " if (stream.eat(\"*\")) {\n", - " state.tokenize.push(tokenComment);\n", - " return tokenComment(stream, state);\n", - " }\n", - " }\n", - " if (ch == \"$\") {\n", - " stream.skipToEnd();\n", - " return \"comment\";\n", - " }\n", - " if (isOperatorChar.test(ch)) {\n", - " stream.eatWhile(isOperatorChar);\n", - " return \"operator\";\n", - " }\n", - " if (punc.indexOf(ch) > -1) {\n", - " return \"punctuation\";\n", - " }\n", - " stream.eatWhile(/[\\w\\$_\\xa1-\\uffff]/);\n", - " var cur = stream.current();\n", - " \n", - " if (keywords.propertyIsEnumerable(cur)) {\n", - " return \"keyword\";\n", - " }\n", - " return \"variable\";\n", - " }\n", - "\n", - " function tokenComment(stream, state) {\n", - " var maybeEnd = false, ch;\n", - " while (ch = stream.next()) {\n", - " if (ch == \"/\" && maybeEnd) {\n", - " state.tokenize.pop();\n", - " break;\n", - " }\n", - " maybeEnd = (ch == \"*\");\n", - " }\n", - " return \"comment\";\n", - " }\n", - "\n", - " function tokenUntilClosingParen() {\n", - " var depth = 0;\n", - " return function (stream, state, prev) {\n", - " var inner = tokenBase(stream, state, prev);\n", - " console.log(\"untilClosing\", inner, stream.current());\n", - " if (inner == \"punctuation\") {\n", - " if (stream.current() == \"(\") {\n", - " ++depth;\n", - " } else if (stream.current() == \")\") {\n", - " if (depth == 0) {\n", - " stream.backUp(1)\n", - " state.tokenize.pop()\n", - " return state.tokenize[state.tokenize.length - 1](stream, state)\n", - " } else {\n", - " --depth;\n", - " }\n", - " }\n", - " }\n", - " return inner;\n", - " }\n", - " }\n", - "\n", - " function tokenString(stream, state) {\n", - " var escaped = false, next, end = false;\n", - " while ((next = stream.next()) != null) {\n", - " if (next == '(' && escaped) {\n", - " state.tokenize.push(tokenUntilClosingParen());\n", - " return \"string\";\n", - " }\n", - " if (next == '\"' && !escaped) { end = true; break; }\n", - " escaped = !escaped && next == \"\\\\\";\n", - " }\n", - " if (end || !escaped)\n", - " state.tokenize.pop();\n", - " return \"string\";\n", - " }\n", - "\n", - " return {\n", - " startState: function (basecolumn) {\n", - " return {\n", - " tokenize: []\n", - " };\n", - " },\n", - "\n", - " token: function (stream, state) {\n", - " if (stream.eatSpace()) return null;\n", - " var style = (state.tokenize[state.tokenize.length - 1] || tokenBase)(stream, state);\n", - " console.log(\"token\", style);\n", - " return style;\n", - " },\n", - "\n", - " blockCommentStart: \"/*\",\n", - " blockCommentEnd: \"*/\",\n", - " lineComment: \"$\"\n", - " };\n", - "});\n", - "\n", - "\n", - "CodeMirror.defineMIME(\"text/conjure\", \"text/conjure\");\n", - "\n", - "require(['notebook/js/codecell'], function (codecell) {\n", - " codecell.CodeCell.options_default.highlight_modes['magic_text/conjure'] = { 'reg': [/%?%conjure/] };\n", - " Jupyter.notebook.events.one('kernel_ready.Kernel', function () {\n", - " Jupyter.notebook.get_cells().map(function (cell) {\n", - " if (cell.cell_type == 'code') { cell.auto_highlight(); }\n", - " });\n", - " });\n", - "});\n", - "\n" ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "stream", "name": "stdout", + "output_type": "stream", "text": [ "Conjure extension is loaded.\n", "For usage help run: %conjure_help\n" ] } + ], + "source": [ + "!source <(curl -s https://raw.githubusercontent.com/conjure-cp/conjure-notebook/v0.0.2/scripts/install-colab.sh)\n", + "%load_ext conjure" ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "## The Problem" - ], "metadata": { "id": "IIXm6aerbQEv" - } + }, + "source": [ + "## The Problem" + ] }, { + "attachments": {}, "cell_type": "markdown", + "metadata": { + "id": "8_84KDprbpLq" + }, "source": [ "Semigroups, monoids and groups are all examples of binary operations, with added conditions.\n", "\n", "\n", "We will begin by building a binary operation. A binary relation `R` on a domain `S` is a two-argument function which maps two elements of `S` to a third element of `S`. We will make `S` be the integers from `1` to `n`, for some given `n`." - ], - "metadata": { - "id": "8_84KDprbpLq" - } + ] }, { + "attachments": {}, "cell_type": "markdown", + "metadata": { + "id": "aP09RDjCc03v" + }, "source": [ "We make a new type of size `n` to represent the set the operation is defined on. We then define a function from `(S,S)` to `S`. Technically, this function doesn’t take two arguments - it takes a single argument which is a pair of values from `S`. This is mathematically the same, but will change how we use `R`.\n", "\n", "\n", "We will begin by creating a solution to this, for `n = 4`." - ], - "metadata": { - "id": "aP09RDjCc03v" - } + ] }, { "cell_type": "code", - "source": [ - "n = 4" - ], + "execution_count": null, "metadata": { "id": "WutDydBpcrlm" }, - "execution_count": null, - "outputs": [] + "outputs": [], + "source": [ + "n = 4" + ] }, { "cell_type": "code", - "source": [ - "%%conjure\n", - "given n : int\n", - "letting S be domain int(1..n)\n", - "\n", - "find R : function(total) (S,S) --> S" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -375,10 +147,8 @@ "id": "ruoE-Rc-b-eP", "outputId": "2404a163-69b6-466e-86a0-ef24f370ba85" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{'R': [[[1, 1], 1],\n", @@ -399,63 +169,66 @@ " [[4, 4], 1]]}" ] }, + "execution_count": 4, "metadata": {}, - "execution_count": 4 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure\n", + "given n : int\n", + "letting S be domain int(1..n)\n", + "\n", + "find R : function(total) (S,S) --> S" ] }, { + "attachments": {}, "cell_type": "markdown", + "metadata": { + "id": "d6aN2lyydSpa" + }, "source": [ "At the moment this is quite boring, as the function can take any value at all! Asking Conjure how many solutions this problem has is unreasonable, but we can figure it out with maths:\n", "\n", "416 = 4,294,967,296\n", "\n", "Let’s try adding some constraints." - ], - "metadata": { - "id": "d6aN2lyydSpa" - } + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "##Semigroups" - ], "metadata": { "id": "7fJvxGbLd3Rp" - } + }, + "source": [ + "## Semigroups" + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "The simplest object we will consider is a **semigroup**. A semigroup adds one constraint to our binary operation, **associativity**. A binary operation is associative if for all i,j and k in S, R(i,R(j,k)) = R((R(i,j),k). This might look very abstract, but it is true of many binary operations, for example given integers i,j and k, (i+j)+k = i+(j+k), and (i * j) * k = i * (j * k)." - ], "metadata": { "id": "s7QuRhtUd52X" - } + }, + "source": [ + "The simplest object we will consider is a **semigroup**. A semigroup adds one constraint to our binary operation, **associativity**. A binary operation is associative if for all i,j and k in S, R(i,R(j,k)) = R((R(i,j),k). This might look very abstract, but it is true of many binary operations, for example given integers i,j and k, (i+j)+k = i+(j+k), and (i * j) * k = i * (j * k)." + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "We begin by saying we want to check `forAll i,j,k: S`. The strangest bit is all of the brackets seem doubled. Your vision isn’t failing, this is because `M` is a one argument function (and we use `M(x)` to apply `M` to `x`), but `M` takes a tuple as its argument (which we write as `(i,j)`), so to apply `M` to `i` and `j` we write `M((i,j))`." - ], "metadata": { "id": "0gWAIm26eGVv" - } + }, + "source": [ + "We begin by saying we want to check `forAll i,j,k: S`. The strangest bit is all of the brackets seem doubled. Your vision isn’t failing, this is because `M` is a one argument function (and we use `M(x)` to apply `M` to `x`), but `M` takes a tuple as its argument (which we write as `(i,j)`), so to apply `M` to `i` and `j` we write `M((i,j))`." + ] }, { "cell_type": "code", - "source": [ - "%%conjure\n", - "letting S be domain int(1..n)\n", - "\n", - "find R : function(total) (S,S) --> S\n", - "\n", - "such that\n", - "\n", - "forAll i,j,k: S. R((i,R((j,k)))) = R((R((i,j)),k))" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -463,10 +236,8 @@ "id": "E5hy8Xe7ebsM", "outputId": "e878e0f2-d253-46eb-c723-7eed146e726d" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{'R': [[[1, 1], 1],\n", @@ -487,56 +258,57 @@ " [[4, 4], 1]]}" ] }, + "execution_count": 6, "metadata": {}, - "execution_count": 6 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure\n", + "letting S be domain int(1..n)\n", + "\n", + "find R : function(total) (S,S) --> S\n", + "\n", + "such that\n", + "\n", + "forAll i,j,k: S. R((i,R((j,k)))) = R((R((i,j)),k))" ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "The first result is still the same, but there are fewer solutions to be found now - only 3,492. Is this correct? It’s always good to check. This number was first published in 1955, by George E. Forsythe, in his paper “SWAC Computes 126 Distinct Semigroups of Order 4”. Where does the number 126 come from? This small number comes from ignoring cases where the semigroup is the same except for rearranging the numbers 1,2,3,4. The number we found, 3,492, is found in the paper." - ], "metadata": { "id": "uQBnwZarenjL" - } + }, + "source": [ + "The first result is still the same, but there are fewer solutions to be found now - only 3,492. Is this correct? It’s always good to check. This number was first published in 1955, by George E. Forsythe, in his paper “SWAC Computes 126 Distinct Semigroups of Order 4”. Where does the number 126 come from? This small number comes from ignoring cases where the semigroup is the same except for rearranging the numbers 1,2,3,4. The number we found, 3,492, is found in the paper." + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "##Monoids" - ], "metadata": { "id": "Kxr07DIuex8m" - } + }, + "source": [ + "## Monoids" + ] }, { + "attachments": {}, "cell_type": "markdown", + "metadata": { + "id": "kHVypWgQe6Fr" + }, "source": [ "Let’s move further to monoids. A monoid is a semigroup with an extra condition, there has to exist some element of the semigroup, which we will call *e*, which acts as an **identity**. An **identity** is an element such that for all `i` in `S`, `R(e,i) = R(i,e) = e`.\n", "\n", "Firstly we will add a variable to store the value of this `e`, and then add the extra constraint which makes it an identity:" - ], - "metadata": { - "id": "kHVypWgQe6Fr" - } + ] }, { "cell_type": "code", - "source": [ - "%%conjure\n", - "\n", - "letting S be domain int(1..n)\n", - "\n", - "find R : function (total) (S,S) --> S\n", - "\n", - "find e : S\n", - "\n", - "such that\n", - "\n", - "forAll i,j,k: S. R((i,R((j,k)))) = R((R((i,j)),k)),\n", - "forAll i : S. R((e,i)) = i /\\ R((i,e)) = i," - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -544,10 +316,8 @@ "id": "6d9Bng1hfpEm", "outputId": "e95c22bf-cd3f-4d3e-f37a-70ea909351b6" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{'R': [[[1, 1], 1],\n", @@ -570,59 +340,61 @@ " 'inv': {'1': 1, '2': 2, '3': 3, '4': 4}}" ] }, + "execution_count": 12, "metadata": {}, - "execution_count": 12 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure\n", + "\n", + "letting S be domain int(1..n)\n", + "\n", + "find R : function (total) (S,S) --> S\n", + "\n", + "find e : S\n", + "\n", + "such that\n", + "\n", + "forAll i,j,k: S. R((i,R((j,k)))) = R((R((i,j)),k)),\n", + "forAll i : S. R((e,i)) = i /\\ R((i,e)) = i," ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "We now have only 624 solutions! We can check this by looking at the amazing online encyclopedia of integer sequences https://oeis.org/A058153 , which tells us there are indeed 624 “labelled monoids” of order n." - ], "metadata": { "id": "8UUknSEagk34" - } + }, + "source": [ + "We now have only 624 solutions! We can check this by looking at the amazing online encyclopedia of integer sequences https://oeis.org/A058153 , which tells us there are indeed 624 “labelled monoids” of order n." + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "##Groups" - ], "metadata": { "id": "2gudg9KYgp6R" - } + }, + "source": [ + "## Groups" + ] }, { + "attachments": {}, "cell_type": "markdown", + "metadata": { + "id": "eWHVoUvPgrbh" + }, "source": [ "Finally, let us move to groups. Groups add one important requirement, the concept of an inverse. Given some `i` in `S`, `j` is an inverse of `i` if `R((i,j)) = R((j,i)) = e`, where `e` is our already existing identity.\n", "\n", "We will store the inverses as an extra array, and then add this final constraint:" - ], - "metadata": { - "id": "eWHVoUvPgrbh" - } + ] }, { "cell_type": "code", - "source": [ - "%%conjure\n", - "letting S be domain int(1..n)\n", - "\n", - "find R : function (total) (S,S) --> S\n", - "\n", - "find e : S\n", - "\n", - "find inv: function S --> S\n", - "\n", - "such that\n", - "\n", - "forAll i,j,k: S. R((i,R((j,k)))) = R((R((i,j)),k)),\n", - "forAll i : S. R((e,i)) = i /\\ R((i,e)) = i,\n", - "\n", - "forAll i : S. R((i,inv(i))) = e /\\ R((inv(i),i)) = e" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -630,10 +402,8 @@ "id": "kjnJufr6g7RP", "outputId": "d612e8b4-54a2-4c5a-8651-1dd386771596" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{'R': [[[1, 1], 1],\n", @@ -656,24 +426,11 @@ " 'inv': {'1': 1, '2': 2, '3': 3, '4': 4}}" ] }, + "execution_count": 9, "metadata": {}, - "execution_count": 9 + "output_type": "execute_result" } - ] - }, - { - "cell_type": "markdown", - "source": [ - "This solution has much more going on than our previous ones! For example, each row and column contains the numbers from `1` to `4`, in some order. This (and many, many other results) are true for all groups (but we won’t prove this here!). This problem only has 16 solutions, and once we removed the groups which are made by just swapping around 1,2,3 and 4, we would find there was only 2 groups! The extra structure means there are only a small number of groups for each size, compared to the number of semigroups and monoids.\n", - "\n", - "There are many special types of groups; we will consider just one here, abelian groups. A group is abelian if for all `i` and `j` in `S`, `R((i,j)) = R((j,i))`. Let’s add this condition!" ], - "metadata": { - "id": "HAdxspUohyta" - } - }, - { - "cell_type": "code", "source": [ "%%conjure\n", "letting S be domain int(1..n)\n", @@ -688,9 +445,25 @@ "\n", "forAll i,j,k: S. R((i,R((j,k)))) = R((R((i,j)),k)),\n", "forAll i : S. R((e,i)) = i /\\ R((i,e)) = i,\n", - "forAll i : S. R((i,inv(i))) = e /\\ R((inv(i),i)) = e,\n", - "forAll i,j : S. R((i,j)) = R((j,i))" - ], + "\n", + "forAll i : S. R((i,inv(i))) = e /\\ R((inv(i),i)) = e" + ] + }, + { + "attachments": {}, + "cell_type": "markdown", + "metadata": { + "id": "HAdxspUohyta" + }, + "source": [ + "This solution has much more going on than our previous ones! For example, each row and column contains the numbers from `1` to `4`, in some order. This (and many, many other results) are true for all groups (but we won’t prove this here!). This problem only has 16 solutions, and once we removed the groups which are made by just swapping around 1,2,3 and 4, we would find there was only 2 groups! The extra structure means there are only a small number of groups for each size, compared to the number of semigroups and monoids.\n", + "\n", + "There are many special types of groups; we will consider just one here, abelian groups. A group is abelian if for all `i` and `j` in `S`, `R((i,j)) = R((j,i))`. Let’s add this condition!" + ] + }, + { + "cell_type": "code", + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -698,10 +471,8 @@ "id": "Kunrbz0-iXhY", "outputId": "2a1b5af6-f56e-4ba4-fc1e-c6f55b8be553" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{'R': [[[1, 1], 1],\n", @@ -724,19 +495,54 @@ " 'inv': {'1': 1, '2': 2, '3': 3, '4': 4}}" ] }, + "execution_count": 11, "metadata": {}, - "execution_count": 11 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure\n", + "letting S be domain int(1..n)\n", + "\n", + "find R : function (total) (S,S) --> S\n", + "\n", + "find e : S\n", + "\n", + "find inv: function S --> S\n", + "\n", + "such that\n", + "\n", + "forAll i,j,k: S. R((i,R((j,k)))) = R((R((i,j)),k)),\n", + "forAll i : S. R((e,i)) = i /\\ R((i,e)) = i,\n", + "forAll i : S. R((i,inv(i))) = e /\\ R((inv(i),i)) = e,\n", + "forAll i,j : S. R((i,j)) = R((j,i))" ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "This gives us the same first solution. In fact, there is the same number of solutions (16) to this problem as the previous one, proving that all groups of size 4 are abelian! In fact, the smallest non-abelian group is size 60, and that is beyond the size of problems we can find all solutions to with our current, simple model." - ], "metadata": { "id": "yZDLJ0G6ifkn" - } + }, + "source": [ + "This gives us the same first solution. In fact, there is the same number of solutions (16) to this problem as the previous one, proving that all groups of size 4 are abelian! In fact, the smallest non-abelian group is size 60, and that is beyond the size of problems we can find all solutions to with our current, simple model." + ] + } + ], + "metadata": { + "colab": { + "authorship_tag": "ABX9TyNmwuGfH/vOYeP0Tj5vUcu/", + "include_colab_link": true, + "provenance": [] + }, + "kernelspec": { + "display_name": "Python 3", + "name": "python3" + }, + "language_info": { + "name": "python" } - ] -} \ No newline at end of file + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/docs/tutorials/notebooks/SimplePermutations.ipynb b/docs/tutorials/notebooks/SimplePermutations.ipynb index 51e4e878f..3d4c740f0 100644 --- a/docs/tutorials/notebooks/SimplePermutations.ipynb +++ b/docs/tutorials/notebooks/SimplePermutations.ipynb @@ -1,93 +1,81 @@ { - "nbformat": 4, - "nbformat_minor": 0, - "metadata": { - "colab": { - "provenance": [], - "authorship_tag": "ABX9TyPeoxDmDrpY9z9gXZGQBH/P", - "include_colab_link": true - }, - "kernelspec": { - "name": "python3", - "display_name": "Python 3" - }, - "language_info": { - "name": "python" - } - }, "cells": [ { + "attachments": {}, "cell_type": "markdown", "metadata": { - "id": "view-in-github", - "colab_type": "text" + "colab_type": "text", + "id": "view-in-github" }, "source": [ "\"Open" ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "# Simple Permutations" - ], "metadata": { "id": "ui5YqwoFv7LV" - } + }, + "source": [ + "# Simple Permutations" + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "Original [Simple Permutations](https://conjure.readthedocs.io/en/latest/tutorials.html#simple-permutations) by Ruth Hoffmann and Gökberk Koçak, edited by András Salamon. Adapted by Alex Gallagher." - ], "metadata": { "id": "U-HzMB6vs1Zw" - } + }, + "source": [ + "Original [Simple Permutations](https://conjure.readthedocs.io/en/latest/tutorials/simple_perm/simple_perm.html) by Ruth Hoffmann and Gökberk Koçak, edited by András Salamon. Adapted by Alex Gallagher." + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "## Problem" - ], "metadata": { "id": "2mcDxfXktRkP" - } + }, + "source": [ + "## Problem" + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "Let a permutation be a sequence of length ***n*** consisting of numbers between 1 and ***n***, in any order with each number occurring exactly once." - ], "metadata": { "id": "vD4QRyo5tVXd" - } + }, + "source": [ + "Let a permutation be a sequence of length ***n*** consisting of numbers between 1 and ***n***, in any order with each number occurring exactly once." + ] }, { + "attachments": {}, "cell_type": "markdown", + "metadata": { + "id": "0lb1eDuYtlM8" + }, "source": [ "An interval in a permutation **σ** is a factor of contiguous values of **σ** such that their indices are consecutive. For example, in the permutation **π=346978215**,\n", "**π(4)π(5)π(6)=978** is an interval, whereas **π(1)π(2)π(3)π(4)=3469** is not. It is easy to see that every permutation of length ***n*** has intervals of length 0, 1 and ***n***, at least. The permutations of length ***n*** that only contain intervals of length 0, 1 and ***n*** are said to be simple. So for example the permutation **π=346978215** is not simple as we have seen in the example above that it contains an interval, on the other hand \n", "**σ=526184937** is simple as there are no intervals of length strictly greater than 1, except the whole of **σ**. See [Hof15](https://conjure.readthedocs.io/en/latest/zreferences.html#id6) for more information on permutation patterns and simple permutations." - ], - "metadata": { - "id": "0lb1eDuYtlM8" - } + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "## Parameter" - ], "metadata": { "id": "Xaie69Fh1n_M" - } + }, + "source": [ + "## Parameter" + ] }, { "cell_type": "code", - "source": [ - "!source <(curl -s https://raw.githubusercontent.com/conjure-cp/conjure-notebook/v0.0.2/scripts/install-colab.sh)\n", - "%load_ext conjure" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/", @@ -96,11 +84,10 @@ "id": "Ez_RQBSQw0DV", "outputId": "a1408b64-36d6-44b0-fec2-962b8929e2a3" }, - "execution_count": null, "outputs": [ { - "output_type": "stream", "name": "stdout", + "output_type": "stream", "text": [ "Installing Conjure...\n", "Conjure: The Automated Constraint Modelling Tool\n", @@ -109,244 +96,32 @@ ] }, { - "output_type": "display_data", "data": { + "application/javascript": "\"use strict\";\n\nCodeMirror.defineMode(\"text/conjure\", function (config) {\n\n var isOperatorChar = /[+\\-*=<>%^\\/]/;\n\n var keywords = {\n \"forall\": true,\n \"allDifferent\": true,\n \"allDiff\": true,\n \"alldifferent_except\": true,\n \"dim\": true,\n \"toSet\": true,\n \"toMSet\": true,\n \"toRelation\": true,\n \"maximising\": true,\n \"minimising\": true,\n \"forAll\": true,\n \"exists\": true,\n \"toInt\": true,\n \"sum\": true,\n \"be\": true,\n \"bijective\": true,\n \"bool\": true,\n \"by\": true,\n \"complete\": true,\n \"defined\": true,\n \"domain\": true,\n \"in\": true,\n \"or\": true,\n \"and\": true,\n \"false\": true,\n \"find\": true,\n \"from\": true,\n \"function\": true,\n \"given\": true,\n \"image\": true,\n \"indexed\": true,\n \"injective\": true,\n \"int\": true,\n \"intersect\": true,\n \"freq\": true,\n \"lambda\": true,\n \"language\": true,\n \"letting\": true,\n \"matrix\": true,\n \"maxNumParts\": true,\n \"maxOccur\": true,\n \"maxPartSize\": true,\n \"maxSize\": true,\n \"minNumParts\": true,\n \"minOccur\": true,\n \"minPartSize\": true,\n \"minSize\": true,\n \"mset\": true,\n \"numParts\": true,\n \"of\": true,\n \"partial\": true,\n \"partition\": true,\n \"partSize\": true,\n \"preImage\": true,\n \"quantifier\": true,\n \"range\": true,\n \"regular\": true,\n \"relation\": true,\n \"representation\": true,\n \"set\": true,\n \"size\": true,\n \"subset\": true,\n \"subsetEq\": true,\n \"such\": true,\n \"supset\": true,\n \"supsetEq\": true,\n \"surjective\": true,\n \"that\": true,\n \"together\": true,\n \"enum\": true,\n \"total\": true,\n \"true\": true,\n \"new\": true,\n \"type\": true,\n \"tuple\": true,\n \"union\": true,\n \"where\": true,\n \"branching\": true,\n \"on\": true\n }; \n var punc = \":;,.(){}[]\";\n\n function tokenBase(stream, state) {\n var ch = stream.next();\n if (ch == '\"') {\n state.tokenize.push(tokenString);\n return tokenString(stream, state);\n }\n if (/[\\d\\.]/.test(ch)) {\n if (ch == \".\") {\n stream.match(/^[0-9]+([eE][\\-+]?[0-9]+)?/);\n } else if (ch == \"0\") {\n stream.match(/^[xX][0-9a-fA-F]+/) || stream.match(/^0[0-7]+/);\n } else {\n stream.match(/^[0-9]*\\.?[0-9]*([eE][\\-+]?[0-9]+)?/);\n }\n return \"number\";\n }\n if (ch == \"/\") {\n if (stream.eat(\"*\")) {\n state.tokenize.push(tokenComment);\n return tokenComment(stream, state);\n }\n }\n if (ch == \"$\") {\n stream.skipToEnd();\n return \"comment\";\n }\n if (isOperatorChar.test(ch)) {\n stream.eatWhile(isOperatorChar);\n return \"operator\";\n }\n if (punc.indexOf(ch) > -1) {\n return \"punctuation\";\n }\n stream.eatWhile(/[\\w\\$_\\xa1-\\uffff]/);\n var cur = stream.current();\n \n if (keywords.propertyIsEnumerable(cur)) {\n return \"keyword\";\n }\n return \"variable\";\n }\n\n function tokenComment(stream, state) {\n var maybeEnd = false, ch;\n while (ch = stream.next()) {\n if (ch == \"/\" && maybeEnd) {\n state.tokenize.pop();\n break;\n }\n maybeEnd = (ch == \"*\");\n }\n return \"comment\";\n }\n\n function tokenUntilClosingParen() {\n var depth = 0;\n return function (stream, state, prev) {\n var inner = tokenBase(stream, state, prev);\n console.log(\"untilClosing\", inner, stream.current());\n if (inner == \"punctuation\") {\n if (stream.current() == \"(\") {\n ++depth;\n } else if (stream.current() == \")\") {\n if (depth == 0) {\n stream.backUp(1)\n state.tokenize.pop()\n return state.tokenize[state.tokenize.length - 1](stream, state)\n } else {\n --depth;\n }\n }\n }\n return inner;\n }\n }\n\n function tokenString(stream, state) {\n var escaped = false, next, end = false;\n while ((next = stream.next()) != null) {\n if (next == '(' && escaped) {\n state.tokenize.push(tokenUntilClosingParen());\n return \"string\";\n }\n if (next == '\"' && !escaped) { end = true; break; }\n escaped = !escaped && next == \"\\\\\";\n }\n if (end || !escaped)\n state.tokenize.pop();\n return \"string\";\n }\n\n return {\n startState: function (basecolumn) {\n return {\n tokenize: []\n };\n },\n\n token: function (stream, state) {\n if (stream.eatSpace()) return null;\n var style = (state.tokenize[state.tokenize.length - 1] || tokenBase)(stream, state);\n console.log(\"token\", style);\n return style;\n },\n\n blockCommentStart: \"/*\",\n blockCommentEnd: \"*/\",\n lineComment: \"$\"\n };\n});\n\n\nCodeMirror.defineMIME(\"text/conjure\", \"text/conjure\");\n\nrequire(['notebook/js/codecell'], function (codecell) {\n codecell.CodeCell.options_default.highlight_modes['magic_text/conjure'] = { 'reg': [/%?%conjure/] };\n Jupyter.notebook.events.one('kernel_ready.Kernel', function () {\n Jupyter.notebook.get_cells().map(function (cell) {\n if (cell.cell_type == 'code') { cell.auto_highlight(); }\n });\n });\n});\n\n", "text/plain": [ "" - ], - "application/javascript": [ - "\"use strict\";\n", - "\n", - "CodeMirror.defineMode(\"text/conjure\", function (config) {\n", - "\n", - " var isOperatorChar = /[+\\-*=<>%^\\/]/;\n", - "\n", - " var keywords = {\n", - " \"forall\": true,\n", - " \"allDifferent\": true,\n", - " \"allDiff\": true,\n", - " \"alldifferent_except\": true,\n", - " \"dim\": true,\n", - " \"toSet\": true,\n", - " \"toMSet\": true,\n", - " \"toRelation\": true,\n", - " \"maximising\": true,\n", - " \"minimising\": true,\n", - " \"forAll\": true,\n", - " \"exists\": true,\n", - " \"toInt\": true,\n", - " \"sum\": true,\n", - " \"be\": true,\n", - " \"bijective\": true,\n", - " \"bool\": true,\n", - " \"by\": true,\n", - " \"complete\": true,\n", - " \"defined\": true,\n", - " \"domain\": true,\n", - " \"in\": true,\n", - " \"or\": true,\n", - " \"and\": true,\n", - " \"false\": true,\n", - " \"find\": true,\n", - " \"from\": true,\n", - " \"function\": true,\n", - " \"given\": true,\n", - " \"image\": true,\n", - " \"indexed\": true,\n", - " \"injective\": true,\n", - " \"int\": true,\n", - " \"intersect\": true,\n", - " \"freq\": true,\n", - " \"lambda\": true,\n", - " \"language\": true,\n", - " \"letting\": true,\n", - " \"matrix\": true,\n", - " \"maxNumParts\": true,\n", - " \"maxOccur\": true,\n", - " \"maxPartSize\": true,\n", - " \"maxSize\": true,\n", - " \"minNumParts\": true,\n", - " \"minOccur\": true,\n", - " \"minPartSize\": true,\n", - " \"minSize\": true,\n", - " \"mset\": true,\n", - " \"numParts\": true,\n", - " \"of\": true,\n", - " \"partial\": true,\n", - " \"partition\": true,\n", - " \"partSize\": true,\n", - " \"preImage\": true,\n", - " \"quantifier\": true,\n", - " \"range\": true,\n", - " \"regular\": true,\n", - " \"relation\": true,\n", - " \"representation\": true,\n", - " \"set\": true,\n", - " \"size\": true,\n", - " \"subset\": true,\n", - " \"subsetEq\": true,\n", - " \"such\": true,\n", - " \"supset\": true,\n", - " \"supsetEq\": true,\n", - " \"surjective\": true,\n", - " \"that\": true,\n", - " \"together\": true,\n", - " \"enum\": true,\n", - " \"total\": true,\n", - " \"true\": true,\n", - " \"new\": true,\n", - " \"type\": true,\n", - " \"tuple\": true,\n", - " \"union\": true,\n", - " \"where\": true,\n", - " \"branching\": true,\n", - " \"on\": true\n", - " }; \n", - " var punc = \":;,.(){}[]\";\n", - "\n", - " function tokenBase(stream, state) {\n", - " var ch = stream.next();\n", - " if (ch == '\"') {\n", - " state.tokenize.push(tokenString);\n", - " return tokenString(stream, state);\n", - " }\n", - " if (/[\\d\\.]/.test(ch)) {\n", - " if (ch == \".\") {\n", - " stream.match(/^[0-9]+([eE][\\-+]?[0-9]+)?/);\n", - " } else if (ch == \"0\") {\n", - " stream.match(/^[xX][0-9a-fA-F]+/) || stream.match(/^0[0-7]+/);\n", - " } else {\n", - " stream.match(/^[0-9]*\\.?[0-9]*([eE][\\-+]?[0-9]+)?/);\n", - " }\n", - " return \"number\";\n", - " }\n", - " if (ch == \"/\") {\n", - " if (stream.eat(\"*\")) {\n", - " state.tokenize.push(tokenComment);\n", - " return tokenComment(stream, state);\n", - " }\n", - " }\n", - " if (ch == \"$\") {\n", - " stream.skipToEnd();\n", - " return \"comment\";\n", - " }\n", - " if (isOperatorChar.test(ch)) {\n", - " stream.eatWhile(isOperatorChar);\n", - " return \"operator\";\n", - " }\n", - " if (punc.indexOf(ch) > -1) {\n", - " return \"punctuation\";\n", - " }\n", - " stream.eatWhile(/[\\w\\$_\\xa1-\\uffff]/);\n", - " var cur = stream.current();\n", - " \n", - " if (keywords.propertyIsEnumerable(cur)) {\n", - " return \"keyword\";\n", - " }\n", - " return \"variable\";\n", - " }\n", - "\n", - " function tokenComment(stream, state) {\n", - " var maybeEnd = false, ch;\n", - " while (ch = stream.next()) {\n", - " if (ch == \"/\" && maybeEnd) {\n", - " state.tokenize.pop();\n", - " break;\n", - " }\n", - " maybeEnd = (ch == \"*\");\n", - " }\n", - " return \"comment\";\n", - " }\n", - "\n", - " function tokenUntilClosingParen() {\n", - " var depth = 0;\n", - " return function (stream, state, prev) {\n", - " var inner = tokenBase(stream, state, prev);\n", - " console.log(\"untilClosing\", inner, stream.current());\n", - " if (inner == \"punctuation\") {\n", - " if (stream.current() == \"(\") {\n", - " ++depth;\n", - " } else if (stream.current() == \")\") {\n", - " if (depth == 0) {\n", - " stream.backUp(1)\n", - " state.tokenize.pop()\n", - " return state.tokenize[state.tokenize.length - 1](stream, state)\n", - " } else {\n", - " --depth;\n", - " }\n", - " }\n", - " }\n", - " return inner;\n", - " }\n", - " }\n", - "\n", - " function tokenString(stream, state) {\n", - " var escaped = false, next, end = false;\n", - " while ((next = stream.next()) != null) {\n", - " if (next == '(' && escaped) {\n", - " state.tokenize.push(tokenUntilClosingParen());\n", - " return \"string\";\n", - " }\n", - " if (next == '\"' && !escaped) { end = true; break; }\n", - " escaped = !escaped && next == \"\\\\\";\n", - " }\n", - " if (end || !escaped)\n", - " state.tokenize.pop();\n", - " return \"string\";\n", - " }\n", - "\n", - " return {\n", - " startState: function (basecolumn) {\n", - " return {\n", - " tokenize: []\n", - " };\n", - " },\n", - "\n", - " token: function (stream, state) {\n", - " if (stream.eatSpace()) return null;\n", - " var style = (state.tokenize[state.tokenize.length - 1] || tokenBase)(stream, state);\n", - " console.log(\"token\", style);\n", - " return style;\n", - " },\n", - "\n", - " blockCommentStart: \"/*\",\n", - " blockCommentEnd: \"*/\",\n", - " lineComment: \"$\"\n", - " };\n", - "});\n", - "\n", - "\n", - "CodeMirror.defineMIME(\"text/conjure\", \"text/conjure\");\n", - "\n", - "require(['notebook/js/codecell'], function (codecell) {\n", - " codecell.CodeCell.options_default.highlight_modes['magic_text/conjure'] = { 'reg': [/%?%conjure/] };\n", - " Jupyter.notebook.events.one('kernel_ready.Kernel', function () {\n", - " Jupyter.notebook.get_cells().map(function (cell) {\n", - " if (cell.cell_type == 'code') { cell.auto_highlight(); }\n", - " });\n", - " });\n", - "});\n", - "\n" ] }, - "metadata": {} + "metadata": {}, + "output_type": "display_data" }, { - "output_type": "stream", "name": "stdout", + "output_type": "stream", "text": [ "Conjure extension is loaded.\n", "For usage help run: %conjure_help\n" ] } + ], + "source": [ + "!source <(curl -s https://raw.githubusercontent.com/conjure-cp/conjure-notebook/v0.0.2/scripts/install-colab.sh)\n", + "%load_ext conjure" ] }, { "cell_type": "code", - "source": [ - "%%conjure\n", - "letting n be 5" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -354,44 +129,46 @@ "id": "KwusJPeEwu1s", "outputId": "ec3d4168-2451-4a08-adc3-096d38d12fef" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{}" ] }, + "execution_count": 2, "metadata": {}, - "execution_count": 2 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure\n", + "letting n be 5" ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "## Enumeration/Generation Model" - ], "metadata": { "id": "Ita9c8GMvqB-" - } + }, + "source": [ + "## Enumeration/Generation Model" + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "We define the size of the permutation to be `n` and we are trying to find all the permutations `perm` to contain the integers 1 to `n`, by specifying that it is `bijective`." - ], "metadata": { "id": "uekUqin9xitZ" - } + }, + "source": [ + "We define the size of the permutation to be `n` and we are trying to find all the permutations `perm` to contain the integers 1 to `n`, by specifying that it is `bijective`." + ] }, { "cell_type": "code", - "source": [ - "%%conjure\n", - "find perm : sequence (bijective, size n) of int(1..n)" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -399,38 +176,39 @@ "id": "fS_FucWHxcQL", "outputId": "f71c97fb-e119-463b-c883-e0f1db1387f2" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{'perm': [1, 2, 3, 4, 5]}" ] }, + "execution_count": 3, "metadata": {}, - "execution_count": 3 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure\n", + "find perm : sequence (bijective, size n) of int(1..n)" ] }, { + "attachments": {}, "cell_type": "markdown", + "metadata": { + "id": "X4xBuOqPyGfP" + }, "source": [ "The idea of our approach is the property of an interval, where when sorted it creates a complete range. This can be translated to checking that the difference between the maximal and the minimal elements of the interval is not equal to the cardinality of the interval.\n", "\n", "\n", "We have one constraint to say that there are only intervals of length 0,1 and `n`. This constraint is defined as a matrix comprehension, which will build a matrix consisting of only boolean entries. We then check the matrix with an `and` constraint, to spot if there are any `false` entries, which would mean that we have an interval." - ], - "metadata": { - "id": "X4xBuOqPyGfP" - } + ] }, { "cell_type": "code", - "source": [ - "%%conjure\n", - "letting example be [ num | num : int(1..5), num != 3 ]" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -438,41 +216,36 @@ "id": "R68A-dhzysUM", "outputId": "b7f25d30-e6b8-4ec3-f33e-bc6cafd14161" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{'perm': [1, 2, 3, 4, 5]}" ] }, + "execution_count": 4, "metadata": {}, - "execution_count": 4 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure\n", + "letting example be [ num | num : int(1..5), num != 3 ]" ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "This is an example which creates a 1-dimensional matrix of `num`s where none of the entries are `3`. We allow also for `letting` statements inside the matrix comprehensions, which allow us to define intermediary statements." - ], "metadata": { "id": "LKPdMqnQ7PCY" - } + }, + "source": [ + "This is an example which creates a 1-dimensional matrix of `num`s where none of the entries are `3`. We allow also for `letting` statements inside the matrix comprehensions, which allow us to define intermediary statements." + ] }, { "cell_type": "code", - "source": [ - "%%conjure\n", - "such that\n", - " and([ max(subs) - min(subs) + 1 != |subs| |\n", - " i : int(1..n-1), j : int(2..n),\n", - " i < j,\n", - " !(i = 1 /\\ j = n),\n", - " letting subs be [perm(k) | k : int(i..j)]]\n", - " )" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -480,68 +253,72 @@ "id": "zu4FYxB7yUoW", "outputId": "878d5a91-9df7-481b-a4d0-18cd65b3bb49" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{'perm': [2, 4, 1, 5, 3]}" ] }, + "execution_count": 5, "metadata": {}, - "execution_count": 5 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure\n", + "such that\n", + " and([ max(subs) - min(subs) + 1 != |subs| |\n", + " i : int(1..n-1), j : int(2..n),\n", + " i < j,\n", + " !(i = 1 /\\ j = n),\n", + " letting subs be [perm(k) | k : int(i..j)]]\n", + " )" ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "We extract `i` and `j` to be the beginning and the end of the interval, and we need to make sure that `i` is less than `j` to have the right order. As we do not want to include the whole permutation as an interval, we restrict that `i` and `j` cannot be simultaneously at the respective ends of the permutation. The final line of the comprehension sets up the continuous subsequences. On the left hand side of the matrix comprehension we use the interval property that when it is turned into a sorted set it is a complete range." - ], "metadata": { "id": "Cf1BEeDg1glo" - } + }, + "source": [ + "We extract `i` and `j` to be the beginning and the end of the interval, and we need to make sure that `i` is less than `j` to have the right order. As we do not want to include the whole permutation as an interval, we restrict that `i` and `j` cannot be simultaneously at the respective ends of the permutation. The final line of the comprehension sets up the continuous subsequences. On the left hand side of the matrix comprehension we use the interval property that when it is turned into a sorted set it is a complete range." + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "## Solving" - ], "metadata": { "id": "tvH81f_y2I_X" - } + }, + "source": [ + "## Solving" + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "Using **n = 5**, the sample solution is `'perm': [2, 4, 1, 5, 3]`." - ], "metadata": { "id": "EL2YTOB52OPk" - } + }, + "source": [ + "Using **n = 5**, the sample solution is `'perm': [2, 4, 1, 5, 3]`." + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "To find all solutions, type:" - ], "metadata": { "id": "S-m9cSca2kpn" - } + }, + "source": [ + "To find all solutions, type:" + ] }, { "cell_type": "code", - "source": [ - "%%conjure --number-of-solutions=all\n", - "such that\n", - " and([ max(subs) - min(subs) + 1 != |subs| |\n", - " i : int(1..n-1), j : int(2..n),\n", - " i < j,\n", - " !(i = 1 /\\ j = n),\n", - " letting subs be [perm(k) | k : int(i..j)]]\n", - " )" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -549,10 +326,8 @@ "id": "eWYFmqAD2qBk", "outputId": "4ca16f13-36fe-40af-e5f8-f149096b4f8d" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "[{'perm': [2, 4, 1, 5, 3]},\n", @@ -563,43 +338,55 @@ " {'perm': [4, 2, 5, 1, 3]}]" ] }, + "execution_count": 6, "metadata": {}, - "execution_count": 6 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure --number-of-solutions=all\n", + "such that\n", + " and([ max(subs) - min(subs) + 1 != |subs| |\n", + " i : int(1..n-1), j : int(2..n),\n", + " i < j,\n", + " !(i = 1 /\\ j = n),\n", + " letting subs be [perm(k) | k : int(i..j)]]\n", + " )" ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "For `n be 5` you should get 6 solutions." - ], "metadata": { "id": "LQwpDusy21y5" - } + }, + "source": [ + "For `n be 5` you should get 6 solutions." + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "## Checking Model with Instances" - ], "metadata": { "id": "i1bwy9HI29f6" - } + }, + "source": [ + "## Checking Model with Instances" + ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "What the model will tell us is that the permutation is simple (true) or not." - ], "metadata": { "id": "GN0CK3Ch3dRW" - } + }, + "source": [ + "What the model will tell us is that the permutation is simple (true) or not." + ] }, { "cell_type": "code", - "source": [ - "%conjure_clear" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -607,24 +394,22 @@ "id": "ZM-TXupi4Crb", "outputId": "7db6ea45-864d-45e6-b2ff-cc0a9f37a6f9" }, - "execution_count": null, "outputs": [ { - "output_type": "stream", "name": "stdout", + "output_type": "stream", "text": [ "Conjure model cleared\n" ] } + ], + "source": [ + "%conjure_clear" ] }, { "cell_type": "code", - "source": [ - "%%conjure\n", - "letting n be 5\n", - "letting perm be sequence( 1, 4, 2, 5, 3)" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -632,33 +417,27 @@ "id": "m--asAoP34hS", "outputId": "22e285f5-c529-4089-90ef-64de80414981" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{}" ] }, + "execution_count": 8, "metadata": {}, - "execution_count": 8 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure\n", + "letting n be 5\n", + "letting perm be sequence( 1, 4, 2, 5, 3)" ] }, { "cell_type": "code", - "source": [ - "%%conjure\n", - "find result : bool\n", - "such that\n", - " result = and([ max(subs) - min(subs) + 1 != |subs| |\n", - " i : int(1..n-1), j : int(2..n),\n", - " i < j,\n", - " !(i = 1 /\\ j = n),\n", - " letting subs be [perm(k) | k : int(i..j)]]\n", - " )" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -666,34 +445,43 @@ "id": "sA6J8xfk3HE3", "outputId": "39c5de0c-d436-416f-bc11-67d2bed424ed" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{'result': False}" ] }, + "execution_count": 9, "metadata": {}, - "execution_count": 9 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure\n", + "find result : bool\n", + "such that\n", + " result = and([ max(subs) - min(subs) + 1 != |subs| |\n", + " i : int(1..n-1), j : int(2..n),\n", + " i < j,\n", + " !(i = 1 /\\ j = n),\n", + " letting subs be [perm(k) | k : int(i..j)]]\n", + " )" ] }, { + "attachments": {}, "cell_type": "markdown", - "source": [ - "This is a non-simple permutation." - ], "metadata": { "id": "sFsXCCIl4Lbt" - } + }, + "source": [ + "This is a non-simple permutation." + ] }, { "cell_type": "code", - "source": [ - "%conjure_clear" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -701,24 +489,22 @@ "id": "8IOTBuUw4ctW", "outputId": "3fa5a06b-1c09-4868-dac2-081fd3f55e69" }, - "execution_count": null, "outputs": [ { - "output_type": "stream", "name": "stdout", + "output_type": "stream", "text": [ "Conjure model cleared\n" ] } + ], + "source": [ + "%conjure_clear" ] }, { "cell_type": "code", - "source": [ - "%%conjure\n", - "letting n be 5\n", - "letting perm be sequence(2, 4, 1, 5, 3)" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -726,33 +512,27 @@ "id": "m392EGci4QrA", "outputId": "2add3fd7-b24d-4622-d4f7-df543d8b5ce9" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{}" ] }, + "execution_count": 11, "metadata": {}, - "execution_count": 11 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure\n", + "letting n be 5\n", + "letting perm be sequence(2, 4, 1, 5, 3)" ] }, { "cell_type": "code", - "source": [ - "%%conjure\n", - "find result : bool\n", - "such that\n", - " result = and([ max(subs) - min(subs) + 1 != |subs| |\n", - " i : int(1..n-1), j : int(2..n),\n", - " i < j,\n", - " !(i = 1 /\\ j = n),\n", - " letting subs be [perm(k) | k : int(i..j)]]\n", - " )" - ], + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -760,35 +540,20 @@ "id": "iIJvB6FM4Zkj", "outputId": "f85d46dc-90c9-4bf4-ca96-da964a3792e3" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { "text/plain": [ "{'result': True}" ] }, + "execution_count": 12, "metadata": {}, - "execution_count": 12 + "output_type": "execute_result" } - ] - }, - { - "cell_type": "markdown", - "source": [ - "It is important to clear the model between instances when redefining variables. If we attempt to run the test again without using `%conjure_clear`, the solutions will not reflect the instance provided in the cell." ], - "metadata": { - "id": "woAjLCyW4iUP" - } - }, - { - "cell_type": "code", "source": [ "%%conjure\n", - "letting n be 5\n", - "letting perm be sequence( 1, 4, 2, 5, 3)\n", "find result : bool\n", "such that\n", " result = and([ max(subs) - min(subs) + 1 != |subs| |\n", @@ -797,7 +562,21 @@ " !(i = 1 /\\ j = n),\n", " letting subs be [perm(k) | k : int(i..j)]]\n", " )" - ], + ] + }, + { + "attachments": {}, + "cell_type": "markdown", + "metadata": { + "id": "woAjLCyW4iUP" + }, + "source": [ + "It is important to clear the model between instances when redefining variables. If we attempt to run the test again without using `%conjure_clear`, the solutions will not reflect the instance provided in the cell." + ] + }, + { + "cell_type": "code", + "execution_count": null, "metadata": { "colab": { "base_uri": "https://localhost:8080/" @@ -805,22 +584,50 @@ "id": "ggmtQf6q5FKE", "outputId": "9cbe2ec0-9be3-47de-ec3d-8da0b4800bcb" }, - "execution_count": null, "outputs": [ { - "output_type": "execute_result", "data": { - "text/plain": [ - "'No solution'" - ], "application/vnd.google.colaboratory.intrinsic+json": { "type": "string" - } + }, + "text/plain": [ + "'No solution'" + ] }, + "execution_count": 13, "metadata": {}, - "execution_count": 13 + "output_type": "execute_result" } + ], + "source": [ + "%%conjure\n", + "letting n be 5\n", + "letting perm be sequence( 1, 4, 2, 5, 3)\n", + "find result : bool\n", + "such that\n", + " result = and([ max(subs) - min(subs) + 1 != |subs| |\n", + " i : int(1..n-1), j : int(2..n),\n", + " i < j,\n", + " !(i = 1 /\\ j = n),\n", + " letting subs be [perm(k) | k : int(i..j)]]\n", + " )" ] } - ] -} \ No newline at end of file + ], + "metadata": { + "colab": { + "authorship_tag": "ABX9TyPeoxDmDrpY9z9gXZGQBH/P", + "include_colab_link": true, + "provenance": [] + }, + "kernelspec": { + "display_name": "Python 3", + "name": "python3" + }, + "language_info": { + "name": "python" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +}