{ "cells": [ { "cell_type": "markdown", "id": "0de480a5", "metadata": {}, "source": [ "# Constraint *Intension*" ] }, { "cell_type": "markdown", "id": "5529d065", "metadata": {}, "source": [ "A constraint *Intension* corresponds to a Boolean expression that may involve variables, constants and various (arithmetic, relational and logical) operators.\n", "For example, the constraint $x+y = z$ corresponds to an equation, which is an expression evaluated to false or true according to the values assigned to the variables $x$, $y$ and $z$." ] }, { "cell_type": "markdown", "id": "7c6d7836", "metadata": {}, "source": [ "**Remark.** Note that for equality, we need to use '==' in Python (the operator '=' used for assignment cannot be redefined), and so, the previous constraint must be written $x+y == z$ in PyCSP$^3$." ] }, { "cell_type": "markdown", "id": "6528c6ec", "metadata": {}, "source": [ "**Remark.** Note that the integer values $0$ and $1$ are respectively equivalent to the Boolean values false and true. This allows us to combine Boolean expressions with arithmetic operators (for example, addition) without requiring any type conversions.\n", "For example, it is valid to write $(x < 5) + (y < z) == 1$ for stating that exactly one of the Boolean expressions $x<5$ and $y\n", " \n", " \n", " \n", "\n", "\n", "\n", "\n", "\n", " Arithmetic operators$+$addition$-$subtraction$*$multiplication // integer division % remainder ** power \n", " \n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", " Relational Operators$<$Less than$<=$Less than or equal$>=$Greater than or equal$>$Greater than$!=$Different from$==$Equal to \n", "\n", " \n", " \n", "\n", "\n", "\n", "\n", " Set Operators in membership not in non membership \n", " \n", "\n", "\n", "\n", "\n", " \n", "\n", " Logical Operators$\\sim$logical not | logical or \\ logical and ^ logical xor \n", " \n", " \n", " \n", "\n", "\n", " \n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", " Functions abs() absolute value of the argument min() minimum value of 2 or more arguments max() maximum value of 2 or more arguments dist() distance between the 2 arguments conjunction() conjunction of 2 or more arguments disjunction() disjunction of 2 or more arguments imply() implication between 2 arguments iff() equivalence between 2 or more arguments ift() ift(b,u,v) returns u if b is true, v otherwise \n", " \n", " \n", "\n", "\n", "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " Expressions Observations x + y < 10 equivalent to 10 > x + y x*2 - 10*y + 5 == 100 we need to use `==' in Python abs(z[0] - z[1]) >= 2 equivalent to dist(z[0], z[1]) >= 2 (x == y) | (y == 0) parentheses are required disjunction(x < 2, y < 4, x > y) equivalent to (x < 2) | (y < 4) | (x > y) imply(x == 0, y > 0) equivalent to (x = 0) | (y > 0) iff(x > 0, y > 0) equivalent to (x > 0) == (y > 0) (x == 0) ^ (y ==1) use of the logical xor operator ift(x == 0, 5, 10) the value is 5 if x is 0 else 10 \n", "\n" ] }, { "cell_type": "markdown", "id": "d5a05107", "metadata": {}, "source": [ "Below, we give several illustrations corresponding to representative use cases of the constraint *Intension*. " ] }, { "cell_type": "markdown", "id": "a69e2a0b", "metadata": {}, "source": [ "## Case 1: Simple Arithmetic Constraint" ] }, { "cell_type": "markdown", "id": "7f2062b3", "metadata": {}, "source": [ "The first case is a constraint *Intension* that corersponds to a simple arithmetic constraint." ] }, { "cell_type": "markdown", "id": "42bef244", "metadata": {}, "source": [ "To see how this constraint works, we need first to import the library PyCSP$^3$:" ] }, { "cell_type": "code", "execution_count": 1, "id": "80671ce1", "metadata": {}, "outputs": [], "source": [ "from pycsp3 import *" ] }, { "cell_type": "markdown", "id": "69b0453a", "metadata": {}, "source": [ "For our illustration, we introduce two stand-alone variables$x$and$y$, each one with$0..9$as domain" ] }, { "cell_type": "code", "execution_count": 2, "id": "363e8a70", "metadata": {}, "outputs": [], "source": [ "x = Var(range(10))\n", "y = Var(range(10))" ] }, { "cell_type": "markdown", "id": "fa0f358a", "metadata": {}, "source": [ "We simply post a single constraint *Intension* imposing that the sum of the values assigned to the variables$x$and$y$is strictly less than 10." ] }, { "cell_type": "code", "execution_count": 3, "id": "25482081", "metadata": {}, "outputs": [], "source": [ "satisfy(\n", " x + y < 10\n", ");" ] }, { "cell_type": "markdown", "id": "9d34d011", "metadata": {}, "source": [ "We can display the internal representation of the posted constraint; although a little bit technical, we can see that the constraint is correctly recorded (note that 'lt' stands for '(strictly) less than')." ] }, { "cell_type": "code", "execution_count": 4, "id": "dbe27d5b", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "intension(function:lt(add(x,y),10))\n" ] } ], "source": [ "print(posted())" ] }, { "cell_type": "markdown", "id": "1da7c0d2", "metadata": {}, "source": [ "By calling the function solve(), we can check that the problem (actually, the single constraint) is satisfiable (SAT). We can also print the values assigned to the variables in the found solution by calling the function *value()*." ] }, { "cell_type": "code", "execution_count": 5, "id": "5aad8683", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Values of x and y: 0 0\n" ] } ], "source": [ "if solve() is SAT:\n", " print(\"Values of x and y: \", value(x), value(y))" ] }, { "cell_type": "markdown", "id": "eb98722e", "metadata": {}, "source": [ "On can anticipate that the number of solutions (supports) for this constraint is$\\sum_{i=1}^{10} i = 55$" ] }, { "cell_type": "code", "execution_count": 6, "id": "de7de0a1", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Number of solutions: 55\n" ] } ], "source": [ "if solve(sols=ALL) is SAT:\n", " print(\"Number of solutions: \", n_solutions())" ] }, { "cell_type": "markdown", "id": "40d46221", "metadata": {}, "source": [ "## Case 2: Another Arithmetic Constraint" ] }, { "cell_type": "markdown", "id": "1944e25c", "metadata": {}, "source": [ "To test another constraint, we remove the one that has just been posted by calling the function *unpost()*." ] }, { "cell_type": "code", "execution_count": 7, "id": "1b71085e", "metadata": {}, "outputs": [], "source": [ "unpost()" ] }, { "cell_type": "markdown", "id": "67f09867", "metadata": {}, "source": [ "We control that there are no more constraints." ] }, { "cell_type": "code", "execution_count": 8, "id": "9a41c801", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "[]\n" ] } ], "source": [ "print(posted())" ] }, { "cell_type": "markdown", "id": "87daafda", "metadata": {}, "source": [ "We now post a single constraint *Intension* imposing that the distance between the values assigned to the variables$x$and$y$is strictly less than 10." ] }, { "cell_type": "code", "execution_count": 9, "id": "68d0b1fd", "metadata": {}, "outputs": [], "source": [ "satisfy(\n", " abs(x - y) >= 7\n", ");" ] }, { "cell_type": "markdown", "id": "f1a4bb72", "metadata": {}, "source": [ "We can enumerate all solutions (supports) of this constraint as follows:" ] }, { "cell_type": "code", "execution_count": 10, "id": "1e7edb70", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Solution 1: 0 7\n", "Solution 2: 0 8\n", "Solution 3: 0 9\n", "Solution 4: 1 9\n", "Solution 5: 2 9\n", "Solution 6: 7 0\n", "Solution 7: 8 0\n", "Solution 8: 9 0\n", "Solution 9: 9 1\n", "Solution 10: 8 1\n", "Solution 11: 9 2\n", "Solution 12: 1 8\n" ] } ], "source": [ "if solve(sols=ALL) is SAT:\n", " for i in range(n_solutions()):\n", " print(f\"Solution {i+1}: {value(x, sol=i)} {value(y, sol=i)}\")" ] }, { "cell_type": "markdown", "id": "45e84e2e", "metadata": {}, "source": [ "## Case 3: A Logical Combination" ] }, { "cell_type": "markdown", "id": "0e6700af", "metadata": {}, "source": [ "The third case is about a constraint *Intension* involving a logical operator." ] }, { "cell_type": "markdown", "id": "6403da3f", "metadata": {}, "source": [ "First, we need to remove the one that has just been posted by calling the function *unpost()*." ] }, { "cell_type": "code", "execution_count": 11, "id": "a0741907", "metadata": {}, "outputs": [], "source": [ "unpost()" ] }, { "cell_type": "markdown", "id": "c179708e", "metadata": {}, "source": [ "We now post a single constraint *Intension* imposing that either the value assigned to$x$is strictly less than 2 or the value assigned to$y\$ is equal to 4." ] }, { "cell_type": "markdown", "id": "0f6b61ac", "metadata": {}, "source": [ "If we post this inadequate form of constraint *Intension*, we obtain a warning." ] }, { "cell_type": "code", "execution_count": 12, "id": "23da2438", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "\n", " \u001b[93mWarning: \u001b[0mA node is evaluated as a Boolean (technically, __bool__ is called)\n", "\tIt is likely a problem with the use of logical operators\n", "\tFor example, you must write (x[0] == x[1]) | (x[0] == x[2]) instead of (x[0] == x[1]) or (x[0] == x[2])\n", "\tSee also the end of section about constraint Intension in chapter 'Twenty popular constraints' of the guide\n", "\n" ] } ], "source": [ "satisfy(\n", " x < 2 or y == 4\n", ");" ] }, { "cell_type": "markdown", "id": "ad96bb78", "metadata": {}, "source": [ "By displaying the internal representation of the constraint, one can clearly see that there is a problem." ] }, { "cell_type": "code", "execution_count": 13, "id": "ed2514a5", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "intension(function:lt(x,2))\n" ] } ], "source": [ "print(posted())" ] }, { "cell_type": "markdown", "id": "63e4987b", "metadata": {}, "source": [ "The problem is that **we cannot use the keywords or, and and not**, when writing constraints *Intension*. This is because we cannot redefine these keywords. Instead, **we have to use the operators \\|, & and ~**." ] }, { "cell_type": "markdown", "id": "03e25f69", "metadata": {}, "source": [ "Let us discard this flawed expression." ] }, { "cell_type": "code", "execution_count": 14, "id": "ff538241", "metadata": {}, "outputs": [], "source": [ "unpost()" ] }, { "cell_type": "markdown", "id": "20b569ce", "metadata": {}, "source": [ "Imagine now that we write the expression as follows:" ] }, { "cell_type": "raw", "id": "33be1801", "metadata": { "raw_mimetype": "text/x-python" }, "source": [ "satisfy(\n", " x < 2 | y == 4\n", ");" ] }, { "cell_type": "markdown", "id": "7465a166", "metadata": {}, "source": [ "An error occurs because an int and a Variable cannot be combined by the operator \\|." ] }, { "cell_type": "markdown", "id": "a6cc3bc6", "metadata": {}, "source": [ "And if we try this equivalent expression, we obtain a warning." ] }, { "cell_type": "code", "execution_count": 15, "id": "13414402", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "\n", " \u001b[93mWarning: \u001b[0mA node is evaluated as a Boolean (technically, __bool__ is called)\n", "\tIt is likely a problem with the use of logical operators\n", "\tFor example, you must write (x[0] == x[1]) | (x[0] == x[2]) instead of (x[0] == x[1]) or (x[0] == x[2])\n", "\tSee also the end of section about constraint Intension in chapter 'Twenty popular constraints' of the guide\n", "\n" ] } ], "source": [ "satisfy(\n", " 2 > x | y == 4\n", ");" ] }, { "cell_type": "markdown", "id": "c17369b5", "metadata": {}, "source": [ "By displaying the internal representation of the constraint, one can clearly see that there is again a problem." ] }, { "cell_type": "code", "execution_count": 16, "id": "8fd47f6f", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "intension(function:eq(or(x,y),4))\n" ] } ], "source": [ "print(posted())" ] }, { "cell_type": "markdown", "id": "09f0c844", "metadata": {}, "source": [ "The problem is that we need to surround subexpressions with brackets. " ] }, { "cell_type": "markdown", "id": "b2b8721b", "metadata": {}, "source": [ "Let us discard this flawed expression." ] }, { "cell_type": "code", "execution_count": 17, "id": "a18e3c1b", "metadata": {}, "outputs": [], "source": [ "unpost()" ] }, { "cell_type": "markdown", "id": "991b8bb4", "metadata": {}, "source": [ "And, now let us write:" ] }, { "cell_type": "code", "execution_count": 18, "id": "b0b8297a", "metadata": {}, "outputs": [], "source": [ "satisfy(\n", " (x < 2) | (y == 4)\n", ");" ] }, { "cell_type": "markdown", "id": "4d7a6be1", "metadata": {}, "source": [ "Let us print the posted constraint, to control it." ] }, { "cell_type": "code", "execution_count": 19, "id": "097105f1", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "intension(function:or(lt(x,2),eq(y,4)))\n" ] } ], "source": [ "print(posted())" ] }, { "cell_type": "markdown", "id": "e0443dda", "metadata": {}, "source": [ "That looks correct. So let us run the solver:" ] }, { "cell_type": "code", "execution_count": 20, "id": "936187c2", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Values of x and y: 0 0\n" ] } ], "source": [ "if solve() is SAT:\n", " print(\"Values of x and y: \", value(x), value(y))" ] }, { "cell_type": "markdown", "id": "aa45fe90", "metadata": {}, "source": [ "To be convinced that everything is ok, let us enumerate all solutions." ] }, { "cell_type": "code", "execution_count": 21, "id": "b9c1f201", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Solution 1: 0 0\n", "Solution 2: 0 1\n", "Solution 3: 0 2\n", "Solution 4: 0 3\n", "Solution 5: 0 5\n", "Solution 6: 0 6\n", "Solution 7: 0 7\n", "Solution 8: 0 8\n", "Solution 9: 0 9\n", "Solution 10: 0 4\n", "Solution 11: 1 4\n", "Solution 12: 2 4\n", "Solution 13: 3 4\n", "Solution 14: 4 4\n", "Solution 15: 5 4\n", "Solution 16: 6 4\n", "Solution 17: 7 4\n", "Solution 18: 8 4\n", "Solution 19: 9 4\n", "Solution 20: 1 0\n", "Solution 21: 1 1\n", "Solution 22: 1 2\n", "Solution 23: 1 3\n", "Solution 24: 1 5\n", "Solution 25: 1 6\n", "Solution 26: 1 7\n", "Solution 27: 1 8\n", "Solution 28: 1 9\n" ] } ], "source": [ "if solve(sols=ALL) is SAT:\n", " for i in range(n_solutions()):\n", " print(f\"Solution {i+1}: {value(x, sol=i)} {value(y, sol=i)}\")" ] } ], "metadata": { "celltoolbar": "Raw Cell Format", "kernelspec": { "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, "language_info": { "codemirror_mode": { "name": "ipython", "version": 3 }, "file_extension": ".py", "mimetype": "text/x-python", "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.7.12" } }, "nbformat": 4, "nbformat_minor": 5 }