From 1c366417a60be96a5ef451dc897fd8347ba95f82 Mon Sep 17 00:00:00 2001 From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de> Date: Tue, 17 Jul 2018 13:48:46 +0200 Subject: [PATCH] update presentation --- notebooks/presentations/LPOP18.ipynb | 1685 ++++---------------------- 1 file changed, 224 insertions(+), 1461 deletions(-) diff --git a/notebooks/presentations/LPOP18.ipynb b/notebooks/presentations/LPOP18.ipynb index 2df8bad..87f6ef6 100644 --- a/notebooks/presentations/LPOP18.ipynb +++ b/notebooks/presentations/LPOP18.ipynb @@ -269,7 +269,7 @@ } }, "source": [ - "Tuples simply correspond to nested pairs:" + "**Tuples** simply correspond to nested pairs:" ] }, { @@ -299,7 +299,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Classical B also provides records:" + "Classical B also provides **records**, i.e., tuples with named fields:" ] }, { @@ -373,7 +373,7 @@ } }, "source": [ - "or via a predicate by using a set comprehension:" + "or via a predicate by using a **set comprehension**:" ] }, { @@ -456,7 +456,7 @@ } }, "source": [ - "Sets can be higher-order and contain other sets:" + "Sets can be **higher-order** and contain other sets:" ] }, { @@ -494,7 +494,7 @@ } }, "source": [ - "Relations are modelled as sets of pairs:" + "**Relations** are modelled as sets of pairs:" ] }, { @@ -611,7 +611,7 @@ } }, "source": [ - "Functions are relations which map every domain element to at most one value:" + "**Functions** are relations which map every domain element to at most one value:" ] }, { @@ -637,6 +637,36 @@ "{ thomas|->1, gordon|->2}" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Sequences** are just functions whose domain is 1..n for some n:" + ] + }, + { + "cell_type": "code", + "execution_count": 1, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\mathit{TRUE}$" + ], + "text/plain": [ + "TRUE" + ] + }, + "execution_count": 1, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "[4,5,6] = {1|->4, 2|->5, 3|->6}" + ] + }, { "cell_type": "markdown", "metadata": { @@ -1018,11 +1048,12 @@ } }, "source": [ - "### Substitutions ###\n", - "B also has a rich syntax for substitutions, aka statements.\n", + "### Substitutions (Statements) ###\n", + "B also has a rich syntax for **substitutions**, aka statements.\n", "For example ```x := x+1``` increments the value of x by 1.\n", + "Other constructs are WHILE loops and CASE statements.\n", "We will not talk about substitutions in the rest of this presentation.\n", - "The major differences between classical B and Event-B lie in the area of substitutions, machine composition and refinement." + "But B can provide a nice mixture of **functional programming**, **constraint programming** and **imperative programming**, with precise proof rules rooted in logic." ] }, { @@ -1083,134 +1114,16 @@ }, "source": [ "## Constraint Solving Applications ##\n", - "Constraint solving has many applications in formal methods in general and B in particular.\n", + "Constraint solving has many applications in formal methods in general and B in particular:\n", + "* Animation, in particular dealing with implict specifications to determine parameters\n", + "* Test-case generation\n", + "* Bounded Model Checking\n", + "* Disprover and prover\n", + "* Enabling analysis (determining implicit control flow)\n", + "and many more\n", "\n" ] }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "source": [ - "#### Animation ####\n", - "It is required to animate implicit specifications.\n", - "Take for example an event\n", - "```\n", - "train_catches_up = any t1,t2,x where t1:dom(train_position) & t2:dom(train_position) &\n", - " train_position(t1) < train_position(t2) &\n", - " x:1..(train_position(t2)-train_position(t1)-1) then\n", - " train_position(t1) := train_position(t1)+x end\n", - "```\n", - "To determine whether the event is enabled, and to obtain values for the parameters of the event in a given state of the model, we have to solve the following constraint:" - ] - }, - { - "cell_type": "code", - "execution_count": 30, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "$TRUE$\n", - "\n", - "**Solution:**\n", - "* $x = 1$\n", - "* $train_position = \\{(thomas\\mapsto100),(gordon\\mapsto2020)\\}$\n", - "* $t1 = thomas$\n", - "* $t2 = gordon$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tx = 1\n", - "\ttrain_position = {(thomas↦100),(gordon↦2020)}\n", - "\tt1 = thomas\n", - "\tt2 = gordon" - ] - }, - "execution_count": 30, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "train_position = {thomas|->100, gordon|->2020} &\n", - "t1:dom(train_position) & t2:dom(train_position) & train_position(t1) < train_position(t2) &\n", - "x:1..(train_position(t2)-train_position(t1)-1)" - ] - }, - { - "cell_type": "code", - "execution_count": 31, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "$FALSE$" - ], - "text/plain": [ - "FALSE" - ] - }, - "execution_count": 31, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "train_position = {thomas|->2019, gordon|->2020} &\n", - "t1:dom(train_position) & t2:dom(train_position) & train_position(t1) < train_position(t2) &\n", - "x:1..(train_position(t2)-train_position(t1)-1)" - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "source": [ - "Many other applications exist: generating **testcases**, finding counter examples using **bounded model checking** or other algorithms like IC3.\n", - "Other applications are analysing **proof obligations**.\n", - "Take the proof obligation for an event theorem t1 $/=$ t2:\n", - "```\n", - "train_position:Trains-->1..10000 & train_position(t1) < train_position(t2) |- t1 /= t2\n", - "```\n", - "We can find counter examples to it by negating the proof goal:" - ] - }, - { - "cell_type": "code", - "execution_count": 34, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "$FALSE$" - ], - "text/plain": [ - "FALSE" - ] - }, - "execution_count": 34, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "train_position:Trains-->1..10000 &\n", - "train_position(t1) < train_position(t2) & \n", - "not( t1 /= t2 )" - ] - }, { "cell_type": "markdown", "metadata": {}, @@ -1228,7 +1141,9 @@ "source": [ "### Modelling and Solving Problems in B ###\n", "\n", - "Obviously, we can also use constraint solving to solve puzzles or real-life problems.\n", + "Obviously, we can also use constraint solving in B to solve puzzles or real-life problems.\n", + "In other words, we use B as way to express constraint problems in almost pure mathematics.\n", + "\n", "#### Send More Money Puzzle ####\n", "We now try and solve the SEND+MORE=MONEY arithmetic puzzle in B, involving 8 distinct digits:" ] @@ -1477,406 +1392,230 @@ }, { "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "slide" - } - }, - "source": [ - "## How to solve (set) constraints in B ##\n", - "\n", - "We will now examine how one can perform constraint solving for B." - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "source": [ - "### Booleans ###\n", - "\n", - "If we have only booleans, constraint solving is equivalent to SAT solving.\n", - "Internally, ProB has an interpreter which does **not** translate to CNF (conjunctive normal form), but is otherwise similar to DPLL: deterministic propagations are carried out first (unit propagation) and there are heuristics to choose the next boolean variable to enumerate.\n", - "(We do not translate to CNF also because of well-definedness issues.)\n" - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "slide" - } - }, - "source": [ - "### Integers ###\n", - "\n", - "Let us take the integer constraint ```x*x=100``` which we saw earlier.\n", - "This constraint is actually more complicated than might appear at first sight: the constraint is not linear and the domain of x is not bounded. Indeed, B supports mathematical integers without any bit size restriction.\n", - "So, let us first look at some simpler constraints, where the domains of the variables are all bounded." - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, + "metadata": {}, "source": [ - "Let us look at the simple constraint ```X:0..3 & Y:0..3 & X+Y=2```.\n", - "As you can see there are three solutions for this constraint:\n" + "The well known n Queens problem can be solved as follows:" ] }, { "cell_type": "code", - "execution_count": 42, + "execution_count": 5, "metadata": {}, "outputs": [ { "data": { "text/markdown": [ - "$\\{(0\\mapsto2),(1\\mapsto1),(2\\mapsto0)\\}$" + "Execution time: 0.020736936 seconds" + ], + "text/plain": [ + "Execution time: 0.020736936 seconds" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/markdown": [ + "$\\mathit{TRUE}$\n", + "\n", + "**Solution:**\n", + "* $\\mathit{queens} = \\{(1\\mapsto 1),(2\\mapsto 5),(3\\mapsto 8),(4\\mapsto 6),(5\\mapsto 3),(6\\mapsto 7),(7\\mapsto 2),(8\\mapsto 4)\\}$\n", + "* $\\mathit{n} = 8$" ], "text/plain": [ - "{(0↦2),(1↦1),(2↦0)}" + "TRUE\n", + "\n", + "Solution:\n", + "\tqueens = {(1↦1),(2↦5),(3↦8),(4↦6),(5↦3),(6↦7),(7↦2),(8↦4)}\n", + "\tn = 8" ] }, - "execution_count": 42, + "execution_count": 5, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "{X,Y|X:0..3 & Y:0..3 & X+Y=2}" + ":time :solve prob n=8 &\n", + " queens : perm(1..n) &\n", + " ∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 => queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ - "We will now study how such constraints can be solved." - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "slide" - } - }, - "source": [ - "#### Solving constraints by translating to SAT ####\n", - "Given that we know the *domain* of X and Y in the constraint ``` X:0..3 & Y:0..3 & X+Y=2```, we can represent the integers by binary numbers and convert the constraint to a **SAT** problem.\n", - "The number 2 is ```10``` in binary and we can represent X and Y each by two bits X0,X1 and Y0,Y1.\n", - "We can translate the addition to a propositional logic formula:\n", + "### Mixing Functional Programming with Constraint Programming ###\n", "\n", - "Bit1 | Bit0\n", - "-----|-----\n", - " X1 | X0\n", - " + Y1 | Y0\n", - " |\n", - " Z1 | Z0\n", - " \n", - "Let us find one solution to this constraint, by encoding addition using an additional carry bit ```CARRY0```:" + "In B we can also define (higher-order) functions and mix those with logical predicates.\n" ] }, { "cell_type": "code", - "execution_count": 44, - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, + "execution_count": 7, + "metadata": {}, "outputs": [ { "data": { "text/markdown": [ - "$4$" + "$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\mathit{TRUE}$\n", + "\n", + "**Solution:**\n", + "* $\\mathit{r2} = \\{1,4,9,16,25,36,49,64,81,100\\}$\n", + "* $\\mathit{r3} = [4,9,25,49,121]$\n", + "* $\\mathit{r4} = 256$\n", + "* $\\mathit{sqrt} = 10$\n", + "* $\\mathit{f} = \\lambda \\mathit{x}\\qdot(\\mathit{x} \\in \\mathit{INTEGER}\\mid \\mathit{x} * \\mathit{x})$\n", + "* $\\mathit{r1} = 10000000000$" ], "text/plain": [ - "4" + "TRUE\n", + "\n", + "Solution:\n", + "\tr2 = {1,4,9,16,25,36,49,64,81,100}\n", + "\tr3 = [4,9,25,49,121]\n", + "\tr4 = 256\n", + "\tsqrt = 10\n", + "\tf = λx·(x ∈ INTEGER∣x ∗ x)\n", + "\tr1 = 10000000000" ] }, - "execution_count": 44, + "execution_count": 7, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "card({X0,X1,Y0,Y1,Z0,Z1,CARRY0 | ((X0=TRUE <=> Y0=TRUE) <=> Z0=FALSE) & \n", - " ((X0=TRUE & Y0=TRUE) <=> CARRY0=TRUE) & \n", - " (CARRY0=FALSE => ((X1=TRUE <=> Y1=TRUE) <=> Z1=FALSE)) & \n", - " (CARRY0=TRUE => ((X1=TRUE <=> Y1=TRUE) <=> Z1=TRUE)) &\n", - " Z0=FALSE & Z1=TRUE})" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "As you can see, we have found four solutions and not three! One solution is 3+3=2.\n", - "This is a typical issue when translating arithmetic to binary numbers: we have to prevent overflows, which we do below:" + "f = %x.(x:INTEGER|x*x) & // this is an infinite function\n", + "r1 = f(100000) &\n", + "r2 = f[1..10] &\n", + "r3 = ([2,3,5,7,11] ; f) & // relational composition ; corresponds to map\n", + "r4 = iterate(f,3)(2) & // we can apply the iteration or transitive closure operators\n", + "f(sqrt) = 100 // compute the square root of 100" ] }, { "cell_type": "code", - "execution_count": 45, - "metadata": { - "slideshow": { - "slide_type": "fragment" - } - }, + "execution_count": 8, + "metadata": {}, "outputs": [ { "data": { "text/markdown": [ - "|Nr|X0|X1|Y0|Y1|Z0|Z1|CARRY0|\n", - "|---|---|---|---|---|---|---|---|\n", - "|1|FALSE|FALSE|FALSE|TRUE|FALSE|TRUE|FALSE|\n", - "|2|FALSE|TRUE|FALSE|FALSE|FALSE|TRUE|FALSE|\n", - "|3|TRUE|FALSE|TRUE|FALSE|FALSE|TRUE|TRUE|\n" + "$\\newcommand{\\cprod}{\\mathbin\\times}\\newcommand{\\cprod}{\\mathbin\\times}\\mathit{TRUE}$\n", + "\n", + "**Solution:**\n", + "* $\\mathit{r2} = \\{1,2,3,4\\}$\n", + "* $\\mathit{r3} = [2,2,3,3,4]$\n", + "* $\\mathit{r4} = 2$\n", + "* $\\mathit{r5} = \\{2,4,10,100\\}$\n", + "* $\\mathit{sqr} = 9802$\n", + "* $\\mathit{f} = \\{\\mathit{x},\\mathit{y}\\mid \\mathit{x} \\in \\mathit{NATURAL} \\land \\mathit{y} \\cprod 2 \\geq \\mathit{x} \\land (\\mathit{y} - 1) \\cprod 2 < \\mathit{x}\\}$\n", + "* $\\mathit{r1} = 317$" ], "text/plain": [ - "Nr\tX0\tX1\tY0\tY1\tZ0\tZ1\tCARRY0\n", - "1\tFALSE\tFALSE\tFALSE\tTRUE\tFALSE\tTRUE\tFALSE\n", - "2\tFALSE\tTRUE\tFALSE\tFALSE\tFALSE\tTRUE\tFALSE\n", - "3\tTRUE\tFALSE\tTRUE\tFALSE\tFALSE\tTRUE\tTRUE\n" + "TRUE\n", + "\n", + "Solution:\n", + "\tr2 = {1,2,3,4}\n", + "\tr3 = [2,2,3,3,4]\n", + "\tr4 = 2\n", + "\tr5 = {2,4,10,100}\n", + "\tsqr = 9802\n", + "\tf = {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}\n", + "\tr1 = 317" ] }, - "execution_count": 45, + "execution_count": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ - ":table ({X0,X1,Y0,Y1,Z0,Z1,CARRY0 | ((X0=TRUE <=> Y0=TRUE) <=> Z0=FALSE) & \n", - " ((X0=TRUE & Y0=TRUE) <=> CARRY0=TRUE) & \n", - " (CARRY0=FALSE => ((X1=TRUE <=> Y1=TRUE) <=> Z1=FALSE)) & \n", - " (CARRY0=TRUE => ((X1=TRUE <=> Y1=TRUE) <=> Z1=TRUE)) &\n", - " (CARRY0=TRUE => (X1=FALSE & Y1=FALSE)) & // no overflow\n", - " (CARRY0=FALSE => (X1=FALSE or Y1=FALSE)) & // no overflow\n", - " Z0=FALSE & Z1=TRUE})" + "f = {x,y|x:NATURAL & y**2 >= x & (y-1)**2 <x } & // integer square root function\n", + "r1 = f(100000) &\n", + "r2 = f[1..10] &\n", + "r3 = ([2,3,5,7,11] ; f) &\n", + "r4 = iterate(f,3)(2) &\n", + "f(sqr) = 100 &\n", + "r5 = closure1(f)[{10000}]" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { - "slide_type": "subslide" + "slide_type": "slide" } }, "source": [ - "In ProB, we can use **Kodkod** backend to achieve such a translation to SAT.\n", - "- Kodkod (https://github.com/emina/kodkod) is the API to the **Alloy** (http://alloytools.org) constraint analyzer and takes relational logic predicates and translates them to SAT.\n", - "- The SAT problem can be solved by any SAT solver (Sat4J, minisat, glucose,...).\n", - "- ProB translates parts of B to the Kodkod API and translates the results back to B values.\n", - "- Prior to the translation, ProB performs an interval analysis to determine possible ranges for the integer decision variables.\n", - "\n", - "The details were presented at FM'2012 (Plagge, L.).\n", + "## How to solve (set) constraints in B ##\n", "\n", - "" + "We will now examine how one can perform constraint solving for B.\n", + "ProB has three main solving backends\n", + "* the default solver using CLP(FD) and Prolog co-routines\n", + "* a SAT-based solver, using the Kodkod API of Alloy\n", + "* an SMT-based solver, using Z3 or CVC4\n" ] }, { "cell_type": "code", - "execution_count": 46, - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "outputs": [ - { - "data": { - "text/markdown": [ - "$TRUE$\n", - "\n", - "**Solution:**\n", - "* $x = 2$\n", - "* $y = 0$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tx = 2\n", - "\ty = 0" - ] - }, - "execution_count": 46, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - ":solve kodkod x:0..2 & y:0..2 & x+y=2" - ] - }, - { - "cell_type": "markdown", + "execution_count": 14, "metadata": {}, - "source": [ - "We can find all solutions and check that we find exactly the three expected solutions:" - ] - }, - { - "cell_type": "code", - "execution_count": 47, - "metadata": { - "slideshow": { - "slide_type": "fragment" - } - }, "outputs": [ { "data": { "text/markdown": [ - "$TRUE$\n", - "\n", - "**Solution:**\n", - "* $res = \\{(0\\mapsto2),(1\\mapsto1),(2\\mapsto0)\\}$" + "Execution time: 0.036815957 seconds" ], "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tres = {(0↦2),(1↦1),(2↦0)}" + "Execution time: 0.036815957 seconds" ] }, - "execution_count": 47, "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - ":solve kodkod {x,y|x:0..2 & y:0..2 & x+y=2}=res" - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "slide" - } - }, - "source": [ - "#### Translation to SMTLib ####\n", - "At iFM'2016 we (Krings, L.) presented a translation to SMTLib format to use either the **Z3** or **CVC4** SMT solver.\n", - "Compared to the Kodkod backend, no translation to SAT is performed, SMTLib supports **integer** predicates and integer operators in the language.\n", - "\n", - "\n" - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "source": [ - "Here is ProB's SMTLib/Z3 API calls for the constraint ``` X:0..3 & Y:0..3 & X+Y=2```:\n", - "- mk_var(integer,x) $\\rightarrow$ 2\n", - "- mk_var(integer,y) $\\rightarrow$ 3\n", - "- mk_int_const(0) $\\rightarrow$ 4\n", - "- mk_op(greater_equal,2,4) $\\rightarrow$ 5\n", - "- mk_int_const(2) $\\rightarrow$ 6\n", - "- mk_op(greater_equal,6,2) $\\rightarrow$ 7\n", - "- mk_int_const(0) $\\rightarrow$ 8\n", - "- mk_op(greater_equal,3,8) $\\rightarrow$ 9\n", - "- mk_int_const(2) $\\rightarrow$ 10\n", - "- mk_op(greater_equal,10,3) $\\rightarrow$ 11\n", - "- mk_op(add,2,3) $\\rightarrow$ 12\n", - "- mk_int_const(2) $\\rightarrow$ 13\n", - "- mk_op(equal,12,13) $\\rightarrow$ 14\n", - "- mk_op_arglist(conjunct,[5,7,9,11,14]) $\\rightarrow$ 15" - ] - }, - { - "cell_type": "code", - "execution_count": 48, - "metadata": {}, - "outputs": [ + "output_type": "display_data" + }, { "data": { "text/markdown": [ - "$TRUE$\n", + "$\\mathit{TRUE}$\n", "\n", "**Solution:**\n", - "* $x = 0$\n", - "* $y = 2$" + "* $\\mathit{queens} = \\{(1\\mapsto 1),(2\\mapsto 3),(3\\mapsto 5),(4\\mapsto 14),(5\\mapsto 17),(6\\mapsto 4),(7\\mapsto 16),(8\\mapsto 7),(9\\mapsto 12),(10\\mapsto 18),(11\\mapsto 15),(12\\mapsto 19),(13\\mapsto 6),(14\\mapsto 10),(15\\mapsto 20),(16\\mapsto 11),(17\\mapsto 8),(18\\mapsto 2),(19\\mapsto 13),(20\\mapsto 9)\\}$\n", + "* $\\mathit{n} = 20$" ], "text/plain": [ "TRUE\n", "\n", "Solution:\n", - "\tx = 0\n", - "\ty = 2" + "\tqueens = {(1↦1),(2↦3),(3↦5),(4↦14),(5↦17),(6↦4),(7↦16),(8↦7),(9↦12),(10↦18),(11↦15),(12↦19),(13↦6),(14↦10),(15↦20),(16↦11),(17↦8),(18↦2),(19↦13),(20↦9)}\n", + "\tn = 20" ] }, - "execution_count": 48, + "execution_count": 14, "metadata": {}, "output_type": "execute_result" } ], "source": [ - ":solve z3 x:0..2 & y:0..2 & x+y=2" - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "slide" - } - }, - "source": [ - "#### ProB's CLP(FD) Solver ####\n", - "ProB's default solver makes use of constraint logic programming.\n", - "For arithmetic, it builts on top of CLP(FD), the finite domain library of SICStus Prolog.\n", - "In CLP(FD):\n", - "- every integer variable is associated with a domain of possible values, typically an interval\n", - "- when adding a new constraints, the domains of the involved variables are updated, or more precisely narrowed down.\n", - "- at some point we need to chose variables for enumeration; typically ProB chooses the value with the smallest domain.\n", - "\n", - "Let us use a slightly adapted constraint ```x:0..9 & y:0..9 & x+y=2``` to illustrate how constraint processing works:\n", - "\n", - "- x:0..9 $\\leadsto$ x:0..9, y:$-\\infty$..$\\infty$\n", - "- y:0..9 $\\leadsto$ x:0..9, y:0..9\n", - "- x+y=2 $\\leadsto$ x:0..2, y:0..2\n", - "- Enumerate (label) variable x\n", - " - x=0 $\\leadsto$ x:0..0, y:2..2\n", - " - x=1 $\\leadsto$ x:1..1, y:1..1\n", - " - x=2 $\\leadsto$ x:2..2, y:0..0" - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "source": [ - "Let us now examine the three approaches for the KISS-PASSION puzzle:" + ":time :solve prob n=20 &\n", + " queens : perm(1..n) &\n", + " ∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 => queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2))" ] }, { "cell_type": "code", - "execution_count": 34, + "execution_count": 18, "metadata": {}, "outputs": [ { "data": { "text/markdown": [ - "Execution time: 0.213287097 seconds" + "Execution time: 1.417787341 seconds" ], "text/plain": [ - "Execution time: 0.213287097 seconds" + "Execution time: 1.417787341 seconds" ] }, "metadata": {}, @@ -1888,46 +1627,32 @@ "$\\mathit{TRUE}$\n", "\n", "**Solution:**\n", - "* $\\mathit{P} = 4$\n", - "* $\\mathit{A} = 1$\n", - "* $\\mathit{S} = 3$\n", - "* $\\mathit{I} = 0$\n", - "* $\\mathit{K} = 2$\n", - "* $\\mathit{N} = 9$\n", - "* $\\mathit{O} = 8$" + "* $\\mathit{queens} = \\{(3\\mapsto 4),(5\\mapsto 10),(6\\mapsto 3),(7\\mapsto 5),(9\\mapsto 1),(10\\mapsto 6),(11\\mapsto 2),(12\\mapsto 12),(13\\mapsto 8),(1\\mapsto 7),(2\\mapsto 9),(4\\mapsto 13),(8\\mapsto 11)\\}$\n", + "* $\\mathit{n} = 13$" ], "text/plain": [ "TRUE\n", "\n", "Solution:\n", - "\tP = 4\n", - "\tA = 1\n", - "\tS = 3\n", - "\tI = 0\n", - "\tK = 2\n", - "\tN = 9\n", - "\tO = 8" + "\tqueens = {(3↦4),(5↦10),(6↦3),(7↦5),(9↦1),(10↦6),(11↦2),(12↦12),(13↦8),(1↦7),(2↦9),(4↦13),(8↦11)}\n", + "\tn = 13" ] }, - "execution_count": 34, + "execution_count": 18, "metadata": {}, "output_type": "execute_result" } ], "source": [ - ":time :solve prob {K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & \n", - "(1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) = \n", - "1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7" + ":time :solve kodkod n=13 &\n", + " queens : 1..n >-> 1..n &\n", + " ∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 => queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2))" ] }, { "cell_type": "code", - "execution_count": 35, - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, + "execution_count": 11, + "metadata": {}, "outputs": [ { "ename": "CommandExecutionException", @@ -1939,26 +1664,9 @@ } ], "source": [ - ":time :solve z3 {K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7" - ] - }, - { - "cell_type": "code", - "execution_count": 36, - "metadata": {}, - "outputs": [ - { - "ename": "ProBError", - "evalue": "ProB reported Errors\nProB returned error messages:\nWarning: Kodkod SAT Solver Timeout for Problem Id: 0", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProB reported Errors\u001b[0m", - "\u001b[1m\u001b[31mWarning: Kodkod SAT Solver Timeout for Problem Id: 0\u001b[0m" - ] - } - ], - "source": [ - ":time :solve kodkod {K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7" + ":time :solve z3 n=8 &\n", + " queens : perm(1..n) &\n", + " ∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 => queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2))" ] }, { @@ -2243,89 +1951,7 @@ "### Translation to SAT ###\n", "The Kodkod/Alloy backend translates sets bit vectors. The size of the vector is the number of possible elements.\n", "\n", - "Take for example the following constraint:" - ] - }, - { - "cell_type": "code", - "execution_count": 60, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "$TRUE$\n", - "\n", - "**Solution:**\n", - "* $x = \\{1\\}$\n", - "* $y = \\{1,2\\}$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tx = {1}\n", - "\ty = {1,2}" - ] - }, - "execution_count": 60, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2 & 1:x & x ⊂ y" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "| Element | x | y | x ∪ y |\n", - "| ------------- |-------------| -----| -----|\n", - "| 1 | x1 | y1 | x1 or y1\n", - "| 2 | x2 | y2 | x2 or y2 |" - ] - }, - { - "cell_type": "code", - "execution_count": 55, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "|x1|x2|y1|y2|\n", - "|---|---|---|---|\n", - "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n" - ], - "text/plain": [ - "x1\tx2\ty1\ty2\n", - "TRUE\tFALSE\tTRUE\tTRUE\n" - ] - }, - "execution_count": 55, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - ":table {x1,x2,y1,y2 | {x1,x2,y1,y2} <: BOOL &\n", - " (x1=TRUE or y1=TRUE) & (x2=TRUE or y2=TRUE) & // x ∪ y = 1..2\n", - " x1=TRUE & // 1:x \n", - " (x1=TRUE => y1=TRUE) & (x2=TRUE => y2=TRUE) & (x1/=y1 or x2/=y2) //x ⊂ y\n", - " }" - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "source": [ - "This translation to SAT is exactly what the Kodkod backend does:" + "Take for example the following constraint, the sets x and y are translated to bit vectors of size 2 and set union is simple bitwise or:" ] }, { @@ -2579,135 +2205,32 @@ ] }, { - "cell_type": "code", - "execution_count": 69, + "cell_type": "markdown", "metadata": { "slideshow": { - "slide_type": "fragment" + "slide_type": "subslide" } }, + "source": [ + "Let us look at another relatively simple example which poses problems:" + ] + }, + { + "cell_type": "code", + "execution_count": 71, + "metadata": {}, "outputs": [ { - "data": { - "text/markdown": [ - "$TRUE$\n", - "\n", - "**Solution:**\n", - "* $x = \\emptyset$\n", - "* $y = \\{1,2\\}$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tx = ∅\n", - "\ty = {1,2}" - ] - }, - "execution_count": 69, - "metadata": {}, - "output_type": "execute_result" + "ename": "CommandExecutionException", + "evalue": ":solve: Computation not completed: no solution found (but one might exist)", + "output_type": "error", + "traceback": [ + "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m" + ] } ], "source": [ - "∀ smt_tmp28.(smt_tmp28 ∈ x ⇒ smt_tmp28 ≥ 1 & 2 ≥ smt_tmp28) & // x ⊆ 1..2\n", - "∀ smt_tmp29.(smt_tmp29 ∈ y ⇒ smt_tmp29 ≥ 1 & 2 ≥ smt_tmp29) & // y ⊆ 1..2\n", - "x ∪ y = {1,2}" - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "source": [ - "This in turn gets translated to SMTLib (calls to the Z3 API):\n", - "- mk_var(set(integer),x) $\\rightarrow$ 2\n", - "- mk_var(set(integer),y) $\\rightarrow$ 3\n", - "- mk_bounded_var(integer,_smt_tmp28) $\\rightarrow$ 4\n", - "- mk_op(member,4,2) $\\rightarrow$ 5\n", - "- mk_int_const(1) $\\rightarrow$ 6\n", - "- mk_op(greater_equal,4,6) $\\rightarrow$ 7\n", - "- mk_int_const(2) $\\rightarrow$ 8\n", - "- mk_op(greater_equal,8,4) $\\rightarrow$ 9\n", - "- mk_op_arglist(conjunct,[7,9]) $\\rightarrow$ 10\n", - "- mk_op(implication,5,10) $\\rightarrow$ 11\n", - "- mk_quantifier(forall,[4],11) $\\rightarrow$ 12\n", - "- mk_bounded_var(integer,_smt_tmp29) $\\rightarrow$ 13\n", - "- mk_op(member,13,3) $\\rightarrow$ 14\n", - "- mk_int_const(1) $\\rightarrow$ 15\n", - "- mk_op(greater_equal) $\\rightarrow$ 13,15,16\n", - "- mk_int_const(2) $\\rightarrow$ 17\n", - "- mk_op(greater_equal,17,13) $\\rightarrow$ 18\n", - "- mk_op_arglist(conjunct,[16,18]) $\\rightarrow$ 19\n", - "- mk_op(implication,14,19) $\\rightarrow$ 20\n", - "- mk_quantifier(forall,[13],20) $\\rightarrow$ 21\n", - "- mk_op(union,2,3) $\\rightarrow$ 22\n", - "- mk_int_const(1) $\\rightarrow$ 23\n", - "- mk_int_const(2) $\\rightarrow$ 24\n", - "- mk_set([23,24]) $\\rightarrow$ 25\n", - "- mk_op(equal,22,25) $\\rightarrow$ 26\n", - "- mk_op_arglist(conjunct,[12,21,26]) $\\rightarrow$ 27" - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "source": [ - "This can be solved by Z3 but not by CVC4. Already the slightly more complicated example from above (or the other examples) cannot be solved:" - ] - }, - { - "cell_type": "code", - "execution_count": 56, - "metadata": {}, - "outputs": [ - { - "ename": "CommandExecutionException", - "evalue": ":solve: Computation not completed: no solution found (but one might exist)", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m" - ] - } - ], - "source": [ - ":solve z3 x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2 & 1∈x & x ⊂ y" - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "source": [ - "Let us look at another relatively simple example which poses problems:" - ] - }, - { - "cell_type": "code", - "execution_count": 71, - "metadata": {}, - "outputs": [ - { - "ename": "CommandExecutionException", - "evalue": ":solve: Computation not completed: no solution found (but one might exist)", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m" - ] - } - ], - "source": [ - ":solve z3 f = {1|->3, 2|->6} & r = f~[{6}]" + ":solve z3 f = {1|->3, 2|->6} & r = f~[{6}]" ] }, { @@ -2965,52 +2488,6 @@ "{x|x∈0..2**10 & x mod 100 = 0}" ] }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "source": [ - "A lot of operators and predicates have optimised versions for the AVL tree represenation, e.g.," - ] - }, - { - "cell_type": "code", - "execution_count": 63, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "$\\mathit{TRUE}$\n", - "\n", - "**Solution:**\n", - "* $\\mathit{mn} = 0$\n", - "* $\\mathit{s} = \\{0,100,200,300,400,500,600,700,800,900,1000\\}$\n", - "* $\\mathit{mx} = 1000$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tmn = 0\n", - "\ts = {0,100,200,300,400,500,600,700,800,900,1000}\n", - "\tmx = 1000" - ] - }, - "execution_count": 63, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "s = {x|x∈0..2**10 & x mod 100 = 0} &\n", - "mx = max(s) &\n", - "mn = min(s)" - ] - }, { "cell_type": "markdown", "metadata": { @@ -3085,91 +2562,6 @@ "inf = {x|x>1000} & 1024 : inf & not(1000:inf) & res = (900..1100) ∩ inf" ] }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "source": [ - "For the following set, ProB tries to expand it and then an enumeration warning occurs (also called a **virtual timeout**, ProB realises that no matter what time budget it would be given a timeout would occur).\n", - "The set is then kept symbolic and can again be used in various ways." - ] - }, - { - "cell_type": "code", - "execution_count": 39, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "$\\newcommand{\\binter}{\\mathbin{\\mkern1mu\\cap\\mkern1mu}}\\mathit{TRUE}$\n", - "\n", - "**Solution:**\n", - "* $\\mathit{inf} = \\{\\mathit{x}\\mid \\mathit{x} > 1000 \\land \\mathit{x} \\mathit{mod} 25 = 0\\}$\n", - "* $\\mathit{res} = ((900 \\ldots 1100) \\binter \\{\\mathit{x}\\mid \\mathit{x} > 1000 \\land \\mathit{x} \\mathit{mod} 25 = 0\\})$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tinf = {x∣x > 1000 ∧ x mod 25 = 0}\n", - "\tres = ((900 ‥ 1100) ∩ {x∣x > 1000 ∧ x mod 25 = 0})" - ] - }, - "execution_count": 39, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "inf = {x|x>1000 & x mod 25 = 0} & 1025 ∈ inf & not(1000∈inf) & res = (900..1100) ∩ inf" - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "source": [ - "The virtual timeout message can be removed (and performance improved) by adding the symbolic pragma:" - ] - }, - { - "cell_type": "code", - "execution_count": 7, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "$\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\binter}{\\mathbin{\\mkern1mu\\cap\\mkern1mu}}\\mathit{TRUE}$\n", - "\n", - "**Solution:**\n", - "* $\\mathit{inf} = \\{\\mathit{x}\\mid \\mathit{x} > 1000 \\land \\mathit{x} \\mathit{mod} 25 = 0\\}$\n", - "* $\\mathit{res} = ((900 \\upto 1100) \\binter \\{\\mathit{x}\\mid \\mathit{x} > 1000 \\land \\mathit{x} \\mathit{mod} 25 = 0\\})$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tinf = {x∣x > 1000 ∧ x mod 25 = 0}\n", - "\tres = ((900 ‥ 1100) ∩ {x∣x > 1000 ∧ x mod 25 = 0})" - ] - }, - "execution_count": 7, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "inf = /*@symbolic*/ {x|x>1000 & x mod 25 = 0} & 1025 ∈ inf & not(1000∈inf) & res = (900..1100) ∩ inf" - ] - }, { "cell_type": "markdown", "metadata": { @@ -3239,108 +2631,7 @@ } }, "source": [ - "Note that Kodkod translation and SMT translation not very effective for the above.\n", - "The Kodkod translation can deal with a simpler version of the above:" - ] - }, - { - "cell_type": "code", - "execution_count": 84, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "Execution time: 2.542529935 seconds" - ], - "text/plain": [ - "Execution time: 2.542529935 seconds" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/markdown": [ - "$TRUE$\n", - "\n", - "**Solution:**\n", - "* $vec = \\{(3\\mapsto4),(5\\mapsto16),(6\\mapsto32),(7\\mapsto64),(1\\mapsto1),(2\\mapsto2),(4\\mapsto8),(8\\mapsto128)\\}$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tvec = {(3↦4),(5↦16),(6↦32),(7↦64),(1↦1),(2↦2),(4↦8),(8↦128)}" - ] - }, - "execution_count": 84, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - ":time :solve kodkod vec: 1..8 --> 0..199 & vec(1) : {1,10} & !x.(x:2..8 => vec(x) = vec(x-1)*2)" - ] - }, - { - "cell_type": "code", - "execution_count": 85, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "Execution time: 0.016755497 seconds" - ], - "text/plain": [ - "Execution time: 0.016755497 seconds" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/markdown": [ - "$TRUE$\n", - "\n", - "**Solution:**\n", - "* $vec = \\{(1\\mapsto1),(2\\mapsto2),(3\\mapsto4),(4\\mapsto8),(5\\mapsto16),(6\\mapsto32),(7\\mapsto64),(8\\mapsto128)\\}$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tvec = {(1↦1),(2↦2),(3↦4),(4↦8),(5↦16),(6↦32),(7↦64),(8↦128)}" - ] - }, - "execution_count": 85, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - ":time :solve prob vec: 1..8 --> 0..199 & vec(1) : {1,10} & !x.(x:2..8 => vec(x) = vec(x-1)*2)" - ] - }, - { - "cell_type": "code", - "execution_count": 86, - "metadata": {}, - "outputs": [ - { - "ename": "CommandExecutionException", - "evalue": ":time: :solve: Computation not completed: time out", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:time: :solve: Computation not completed: time out\u001b[0m" - ] - } - ], - "source": [ - ":time :solve z3 vec: 1..8 --> 0..199 & vec(1) : {1,10} & !x.(x:2..8 => vec(x) = vec(x-1)*2)" + "Note that Kodkod translation and SMT translation not very effective for the above." ] }, { @@ -3419,275 +2710,11 @@ "Here is a simple verison of the above" ] }, - { - "cell_type": "code", - "execution_count": 2, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "Execution time: 0.122529996 seconds" - ], - "text/plain": [ - "Execution time: 0.122529996 seconds" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/markdown": [ - "$\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\mathit{TRUE}$\n", - "\n", - "**Solution:**\n", - "* $\\mathit{xy} = \\exists 201\\in\\{1,2,\\ldots,299,300\\}$\n", - "* $\\mathit{x} = (1 \\upto 100)$\n", - "* $\\mathit{y} = (200 \\upto 300)$\n", - "* $\\mathit{n} = 100$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\txy = ∃201∈{1,2,…,299,300}\n", - "\tx = (1 ‥ 100)\n", - "\ty = (200 ‥ 300)\n", - "\tn = 100" - ] - }, - "execution_count": 2, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - ":time :solve prob x = 1..n & y = 2*n..3*n & n = 100 & xy = x \\/ y" - ] - }, - { - "cell_type": "code", - "execution_count": 89, - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "outputs": [ - { - "ename": "CommandExecutionException", - "evalue": ":solve: Computation not completed: time out", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:solve: Computation not completed: time out\u001b[0m" - ] - } - ], - "source": [ - ":solve z3 x = 1..n & y = 2*n..3*n & n = 100 & xy = x \\/ y" - ] - }, - { - "cell_type": "code", - "execution_count": 3, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "Execution time: 2.035079877 seconds" - ], - "text/plain": [ - "Execution time: 2.035079877 seconds" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/markdown": [ - "$\\mathit{TRUE}$\n", - "\n", - "**Solution:**\n", - "* $\\mathit{xy} = \\{3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,200,201,202,203,204,205,206,\\ldots\\}$\n", - "* $\\mathit{x} = \\{3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,1,2,4,8,16,32,64\\}$\n", - "* $\\mathit{y} = \\{200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,256\\}$\n", - "* $\\mathit{n} = 100$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\txy = {3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,200,201,202,203,204,205,206,…}\n", - "\tx = {3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,1,2,4,8,16,32,64}\n", - "\ty = {200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,256}\n", - "\tn = 100" - ] - }, - "execution_count": 3, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - ":time :solve kodkod x = 1..n & y = 2*n..3*n & n = 100 & xy = x \\/ y" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "In the appendix there are more examples which analyse the performance for such examples." - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "source": [ - "ProB employs the *Andorra* principle: deterministic computations are done first.\n", - "As there are multiple set representations, there are actually two kinds of deterministic computations:\n", - "- deterministic computations that generate an efficient representation, e.g., an AVL set representation\n", - "- and other deterministic computations\n", - "\n", - "The ProB solver has a **WAITFLAG store** where choice points and enumerations are registered with a given priority.\n", - "- Priority 0 means that an efficient representation can be generated\n", - "- Priority 1 is a deterministic computation not guaranteed to produce an efficient representation\n", - "- Priority k is a choice point/enumeration which may generate k possible values\n", - "\n", - "At each solving step one waitflag is activated, the one with the lowest priority.\n", - "CLP(FD) variables are also registered in the WAITFLAG store and are enumerated before a waitflag of the same priority is activated. For tie breaking one typically uses the **most attached constraints first** (ffc) heuristic.\n", - "\n", - "#### Example ####\n", - "Let us examine how ```x = 1..n & y = 2*n..3*n & n = 100 & xy = x \\/ y``` is solved.\n", - "- all constraints are registered\n", - "- in phase 0 ```n=100``` is run\n", - "- this means that ```1..n``` can be efficiently computed\n", - "- this means that ```x = 1..n``` triggers in phase 0\n", - "- then ```2*n``` and ```3*n``` can be computed, followed by ```2*n..3*n```\n", - "- this means that ```y = 2*n..3*n``` triggers in phase 0\n", - "- again, this means that ```x \\/ y``` can be efficiently computed\n", - "- finally ```xy = x \\/ y``` can be executed in phase 0\n", - "\n", - "No enumeration was required. In this case ProB's constraint solver works similar to a topological sorting algorithm.\n" - ] - }, { "cell_type": "markdown", - "metadata": {}, - "source": [ - "#### Dealing with unbounded enumeration ####\n", - "\n", - "Note: if an unbounded enumeration is encountered, the solver registers an **enumeration warning** in the current scope (every quantification / comprehension set results in a new inner scope). Depending on the kind of scope (existential/universal) and on whether a solution is found, the warning gets translated into an **UNKNOWN** result." - ] - }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "subslide" - } - }, - "source": [ - "### Functional Programming ###\n", - "\n", - "Some functions are automatically detected as infinite by ProB, are kept symbolic but can be applied in several ways:\n" - ] - }, - { - "cell_type": "code", - "execution_count": 64, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\mathit{TRUE}$\n", - "\n", - "**Solution:**\n", - "* $\\mathit{r2} = \\{1,4,9,16,25,36,49,64,81,100\\}$\n", - "* $\\mathit{r3} = [4,9,25,49,121]$\n", - "* $\\mathit{r4} = 256$\n", - "* $\\mathit{sqrt} = 10$\n", - "* $\\mathit{f} = \\lambda \\mathit{x}\\qdot(\\mathit{x} \\in \\mathit{INTEGER}\\mid \\mathit{x} * \\mathit{x})$\n", - "* $\\mathit{r1} = 10000000000$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tr2 = {1,4,9,16,25,36,49,64,81,100}\n", - "\tr3 = [4,9,25,49,121]\n", - "\tr4 = 256\n", - "\tsqrt = 10\n", - "\tf = λx·(x ∈ INTEGER∣x ∗ x)\n", - "\tr1 = 10000000000" - ] - }, - "execution_count": 64, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "f = %x.(x:INTEGER|x*x) &\n", - "r1 = f(100000) &\n", - "r2 = f[1..10] &\n", - "r3 = ([2,3,5,7,11] ; f) &\n", - "r4 = iterate(f,3)(2) &\n", - "f(sqrt) = 100" - ] - }, - { - "cell_type": "code", - "execution_count": 2, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "$\\newcommand{\\cprod}{\\mathbin\\times}\\newcommand{\\cprod}{\\mathbin\\times}\\mathit{TRUE}$\n", - "\n", - "**Solution:**\n", - "* $\\mathit{r2} = \\{1,2,3,4\\}$\n", - "* $\\mathit{r3} = [2,2,3,3,4]$\n", - "* $\\mathit{r4} = 2$\n", - "* $\\mathit{r5} = \\{2,4,10,100\\}$\n", - "* $\\mathit{sqr} = 9802$\n", - "* $\\mathit{f} = \\{\\mathit{x},\\mathit{y}\\mid \\mathit{x} \\in \\mathit{NATURAL} \\land \\mathit{y} \\cprod 2 \\geq \\mathit{x} \\land (\\mathit{y} - 1) \\cprod 2 < \\mathit{x}\\}$\n", - "* $\\mathit{r1} = 317$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tr2 = {1,2,3,4}\n", - "\tr3 = [2,2,3,3,4]\n", - "\tr4 = 2\n", - "\tr5 = {2,4,10,100}\n", - "\tsqr = 9802\n", - "\tf = {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}\n", - "\tr1 = 317" - ] - }, - "execution_count": 2, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "f = {x,y|x:NATURAL & y**2 >= x & (y-1)**2 <x } & // integer square root function\n", - "r1 = f(100000) &\n", - "r2 = f[1..10] &\n", - "r3 = ([2,3,5,7,11] ; f) &\n", - "r4 = iterate(f,3)(2) &\n", - "f(sqr) = 100 &\n", - "r5 = closure1(f)[{10000}]" + "metadata": {}, + "source": [ + "In the appendix there are more examples which analyse the performance for such examples." ] }, { @@ -3698,50 +2725,40 @@ } }, "source": [ - "### Reification ###\n", + "ProB employs the *Andorra* principle: deterministic computations are done first.\n", + "As there are multiple set representations, there are actually two kinds of deterministic computations:\n", + "- deterministic computations that generate an efficient representation, e.g., an AVL set representation\n", + "- and other deterministic computations\n", "\n", - "Reification is linking the truth value of a constraint with a boolean variable.\n", - "ProB's kernel provides support for reifying a considerable number of constraints (but not yet all!).\n", - "Reification is important for efficiency, to avoid choice points and is important to link various solvers of ProB (set, arithmetic, boolean,...).\n", - "" - ] - }, - { - "cell_type": "code", - "execution_count": 93, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "$TRUE$\n", - "\n", - "**Solution:**\n", - "* $x = 125$\n", - "* $ReifVar = TRUE$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tx = 125\n", - "\tReifVar = TRUE" - ] - }, - "execution_count": 93, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "(x>100 <=> (ReifVar=TRUE)) & (x<125 <=> (ReifVar=FALSE)) & x<200" + "The ProB solver has a **WAITFLAG store** where choice points and enumerations are registered with a given priority.\n", + "- Priority 0 means that an efficient representation can be generated\n", + "- Priority 1 is a deterministic computation not guaranteed to produce an efficient representation\n", + "- Priority k is a choice point/enumeration which may generate k possible values\n", + "\n", + "At each solving step one waitflag is activated, the one with the lowest priority.\n", + "CLP(FD) variables are also registered in the WAITFLAG store and are enumerated before a waitflag of the same priority is activated. For tie breaking one typically uses the **most attached constraints first** (ffc) heuristic.\n", + "\n", + "#### Example ####\n", + "Let us examine how ```x = 1..n & y = 2*n..3*n & n = 100 & xy = x \\/ y``` is solved.\n", + "- all constraints are registered\n", + "- in phase 0 ```n=100``` is run\n", + "- this means that ```1..n``` can be efficiently computed\n", + "- this means that ```x = 1..n``` triggers in phase 0\n", + "- then ```2*n``` and ```3*n``` can be computed, followed by ```2*n..3*n```\n", + "- this means that ```y = 2*n..3*n``` triggers in phase 0\n", + "- again, this means that ```x \\/ y``` can be efficiently computed\n", + "- finally ```xy = x \\/ y``` can be executed in phase 0\n", + "\n", + "No enumeration was required. In this case ProB's constraint solver works similar to a topological sorting algorithm.\n" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ - "" + "#### Dealing with unbounded enumeration ####\n", + "\n", + "Note: if an unbounded enumeration is encountered, the solver registers an **enumeration warning** in the current scope (every quantification / comprehension set results in a new inner scope). Depending on the kind of scope (existential/universal) and on whether a solution is found, the warning gets translated into an **UNKNOWN** result." ] }, { @@ -4041,206 +3058,6 @@ ":solve prob s1 = {2,3,5,7,11} & s2 = {4,8,16,32} & c = s1*s2 & r=c~[{8}]" ] }, - { - "cell_type": "markdown", - "metadata": { - "slideshow": { - "slide_type": "slide" - } - }, - "source": [ - "### Benchmark Puzzles ####\n", - "\n", - "#### N-Queens ####\n" - ] - }, - { - "cell_type": "code", - "execution_count": 124, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "Execution time: 0.060237608 seconds" - ], - "text/plain": [ - "Execution time: 0.060237608 seconds" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/markdown": [ - "$TRUE$\n", - "\n", - "**Solution:**\n", - "* $queens = \\{(1\\mapsto4),(2\\mapsto2),(3\\mapsto7),(4\\mapsto3),(5\\mapsto6),(6\\mapsto8),(7\\mapsto5),(8\\mapsto1)\\}$\n", - "* $n = 8$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tqueens = {(1↦4),(2↦2),(3↦7),(4↦3),(5↦6),(6↦8),(7↦5),(8↦1)}\n", - "\tn = 8" - ] - }, - "execution_count": 124, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - ":time :solve prob n=8 &\n", - " queens : 1..n >-> 1..n &\n", - " !(q1,q2).(q1:1..n & q2:2..n & q2>q1 => queens(q1)+(q2-q1) /= queens(q2) & queens(q1)+(q1-q2) /= queens(q2))" - ] - }, - { - "cell_type": "code", - "execution_count": 125, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "Execution time: 0.393750784 seconds" - ], - "text/plain": [ - "Execution time: 0.393750784 seconds" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/markdown": [ - "$TRUE$\n", - "\n", - "**Solution:**\n", - "* $queens = \\{(1\\mapsto4),(2\\mapsto7),(3\\mapsto5),(4\\mapsto2),(5\\mapsto6),(6\\mapsto1),(7\\mapsto3),(8\\mapsto8)\\}$\n", - "* $n = 8$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tqueens = {(1↦4),(2↦7),(3↦5),(4↦2),(5↦6),(6↦1),(7↦3),(8↦8)}\n", - "\tn = 8" - ] - }, - "execution_count": 125, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - ":time :solve z3 n=8 &\n", - " queens : 1..n >-> 1..n &\n", - " !(q1,q2).(q1:1..n & q2:2..n & q2>q1 => queens(q1)+(q2-q1) /= queens(q2) & queens(q1)+(q1-q2) /= queens(q2))" - ] - }, - { - "cell_type": "code", - "execution_count": 126, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "Execution time: 0.467670114 seconds" - ], - "text/plain": [ - "Execution time: 0.467670114 seconds" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/markdown": [ - "$TRUE$\n", - "\n", - "**Solution:**\n", - "* $queens = \\{(3\\mapsto2),(5\\mapsto5),(6\\mapsto1),(7\\mapsto8),(1\\mapsto3),(2\\mapsto6),(4\\mapsto7),(8\\mapsto4)\\}$\n", - "* $n = 8$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tqueens = {(3↦2),(5↦5),(6↦1),(7↦8),(1↦3),(2↦6),(4↦7),(8↦4)}\n", - "\tn = 8" - ] - }, - "execution_count": 126, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - ":time :solve kodkod n=8 &\n", - " queens : 1..n >-> 1..n &\n", - " !(q1,q2).(q1:1..n & q2:2..n & q2>q1 => queens(q1)+(q2-q1) /= queens(q2) & queens(q1)+(q1-q2) /= queens(q2))" - ] - }, - { - "cell_type": "code", - "execution_count": 128, - "metadata": {}, - "outputs": [ - { - "ename": "CommandExecutionException", - "evalue": ":time: :solve: Computation not completed: time out", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:time: :solve: Computation not completed: time out\u001b[0m" - ] - } - ], - "source": [ - ":time :solve z3 n=3 & bshp <: (1..n)*(1..n) & \n", - " !(i,j).({i,j}<:1..n => ( (i,j): bshp => (!k.(k:(i+1)..n => (k,j+k-i) /: bshp & (k,j-k+i) /: bshp )) )) &\n", - " card(bshp) = 3" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "Solving takes about 150 seconds; Kodkod translation currently does not work due to card and preventing overflows." - ] - }, - { - "cell_type": "code", - "execution_count": 129, - "metadata": {}, - "outputs": [ - { - "data": { - "text/latex": [ - "$\\mathit{n} = 3 \\wedge \\mathit{bshp} \\subseteq (1 .. \\mathit{n}) \\times (1 .. \\mathit{n}) \\wedge \\forall (\\mathit{i},\\mathit{j})\\cdot (\\{\\mathit{i},\\mathit{j}\\} \\subseteq 1 .. \\mathit{n} \\mathbin\\Rightarrow (\\mathit{i} \\mapsto \\mathit{j} \\in \\mathit{bshp} \\mathbin\\Rightarrow \\forall \\mathit{k}\\cdot (\\mathit{k} \\in \\mathit{i} + 1 .. \\mathit{n} \\mathbin\\Rightarrow (\\mathit{k} \\mapsto (\\mathit{j} + \\mathit{k}) - \\mathit{i}) \\not\\in \\mathit{bshp} \\wedge (\\mathit{k} \\mapsto (\\mathit{j} - \\mathit{k}) + \\mathit{i}) \\not\\in \\mathit{bshp}))) \\wedge \\mathit{card}(\\mathit{bshp}) = 3$" - ], - "text/plain": [ - "n = 3 ∧ bshp ⊆ (1 ‥ n) × (1 ‥ n) ∧ ∀(i,j)·({i,j} ⊆ 1 ‥ n ⇒ (i ↦ j ∈ bshp ⇒ ∀k·(k ∈ i + 1 ‥ n ⇒ (k ↦ (j + k) - i) ∉ bshp ∧ (k ↦ (j - k) + i) ∉ bshp))) ∧ card(bshp) = 3" - ] - }, - "execution_count": 129, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - ":prettyprint n=3 & bshp <: (1..n)*(1..n) & \n", - " !(i,j).({i,j}<:1..n => ( (i,j): bshp => (!k.(k:(i+1)..n => (k,j+k-i) /: bshp & (k,j-k+i) /: bshp )) )) &\n", - " card(bshp) = 3" - ] - }, { "cell_type": "markdown", "metadata": { @@ -4422,60 +3239,6 @@ " res = SIGNAL \\ nxt[SIGNAL]" ] }, - { - "cell_type": "code", - "execution_count": 6, - "metadata": {}, - "outputs": [ - { - "data": { - "text/latex": [ - "$\\mathit{x} = \\mathbb N \\wedge \\mathit{y} = NAT$" - ], - "text/plain": [ - "x = ℕ ∧ y = NAT" - ] - }, - "execution_count": 6, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - ":prettyprint x=NATURAL & y=NAT" - ] - }, - { - "cell_type": "code", - "execution_count": 4, - "metadata": {}, - "outputs": [ - { - "data": { - "text/markdown": [ - "$\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\mathit{TRUE}$\n", - "\n", - "**Solution:**\n", - "* $\\mathit{x} = \\mathit{NATURAL}$\n", - "* $\\mathit{y} = (0 \\upto 3)$" - ], - "text/plain": [ - "TRUE\n", - "\n", - "Solution:\n", - "\tx = NATURAL\n", - "\ty = (0 ‥ 3)" - ] - }, - "execution_count": 4, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "x=NATURAL & y=NAT" - ] - }, { "cell_type": "code", "execution_count": null, -- GitLab