{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "b1db8c9a",
   "metadata": {},
   "source": [
    "# Posting constraints"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "514a5144",
   "metadata": {},
   "source": [
    "When constraints must be imposed on variables, we say that these constraints must be satisfied.\n",
    "To impose (post) them, we call the PyCSP$^3$ function *satisfy()*. Several constraints can be posted together, by using comprehension lists and/or several parameters (with commas used as a separator between parameters)."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e730a9ea",
   "metadata": {},
   "source": [
    "To illustrate how it works, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "6136b4c6",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2fc53a65",
   "metadata": {},
   "source": [
    "For our illustration, let us declare an array x of 4 variables, each one with {0,1,2,3} as domain. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "d81544e1",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=4, dom=range(4))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6576cba9",
   "metadata": {},
   "source": [
    "Let us suppose that we want that:\n",
    "- the distance between any two successive values (assigned to variables) of $x$ is greater than or equal to 2\n",
    "- all values of $x$ are different."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c3e4ca14",
   "metadata": {},
   "source": [
    "We can decide to post each constraint independently. This gives:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "7e33a047",
   "metadata": {},
   "outputs": [],
   "source": [
    "for i in range(3):\n",
    "    satisfy(abs(x[i] - x[i+1]) >= 2)\n",
    "satisfy(\n",
    "    AllDifferent(x)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "99e20909",
   "metadata": {},
   "source": [
    "We can display the internal representation of the 4 posted constraints; this way, although a little bit technical, we can see that the constraints are correctly built. Note that 'ge' stands for 'greater than or equal to'."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "91d952fd",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "intension(function:ge(dist(x[0],x[1]),2))\n",
      "intension(function:ge(dist(x[1],x[2]),2))\n",
      "intension(function:ge(dist(x[2],x[3]),2))\n",
      "allDifferent(list:[x[0], x[1], x[2], x[3]])\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "31f95b24",
   "metadata": {},
   "source": [
    "By calling the function *solve()*, we can check that the problem is satisfiable (SAT). Here, to enumerate all solutions, we use the constant *ALL* as value of the named parameter *sols*. Note also that we print the found solutions by calling the function *values()* that collects the values assigned to a specified list of variables, for a solution whose index is given by the value of the named parameter *sol*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "28e0faf9",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      " Solution 0: [1, 3, 0, 2]\n",
      " Solution 1: [2, 0, 3, 1]\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    for i in range(n_solutions()):\n",
    "        print(f\" Solution {i}: {values(x, sol=i)}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "55124773",
   "metadata": {},
   "source": [
    "We now discard all posted constraints:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "9d1ed6fb",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost(ALL)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "876c880f",
   "metadata": {},
   "source": [
    "We can check that there are no more constraints:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "ffdf301e",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[]\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "be04aac6",
   "metadata": {},
   "source": [
    "We show now that we can use a comprehension list (actually, a generator) to post the three binary constraints. This gives:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "61925425",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    abs(x[i] - x[i+1]) >= 2 for i in range(3)\n",
    ")\n",
    "satisfy(\n",
    "    AllDifferent(x)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e745895b",
   "metadata": {},
   "source": [
    "We check that the result is the same in term of posted constraints:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "17f014e4",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "intension(function:ge(dist(x[0],x[1]),2))\n",
      "intension(function:ge(dist(x[1],x[2]),2))\n",
      "intension(function:ge(dist(x[2],x[3]),2))\n",
      "allDifferent(list:[x[0], x[1], x[2], x[3]])\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "dc5f01f6",
   "metadata": {},
   "source": [
    "And of course, we obtain the two same solutions:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "e9156085",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      " Solution 0: [1, 3, 0, 2]\n",
      " Solution 1: [2, 0, 3, 1]\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    for i in range(n_solutions()):\n",
    "        print(f\" Solution {i}: {values(x, sol=i)}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "afecbe23",
   "metadata": {},
   "source": [
    "Again, we discard all posted constraints."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "575c019f",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost(ALL)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c2cc1e57",
   "metadata": {},
   "source": [
    "We show now that we can post all constraints with a single call to *satisfy()*:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "d9cc6dfb",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    [abs(x[i] - x[i+1]) >= 2 for i in range(3)],\n",
    "    AllDifferent(x)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "092545b8",
   "metadata": {},
   "source": [
    "We check that the result is the same in term of posted constraints:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "e84722d0",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "intension(function:ge(dist(x[0],x[1]),2))\n",
      "intension(function:ge(dist(x[1],x[2]),2))\n",
      "intension(function:ge(dist(x[2],x[3]),2))\n",
      "allDifferent(list:[x[0], x[1], x[2], x[3]])\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f01cd0e5",
   "metadata": {},
   "source": [
    "And we have the two same solutions:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "6a33370b",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      " Solution 0: [1, 3, 0, 2]\n",
      " Solution 1: [2, 0, 3, 1]\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    for i in range(n_solutions()):\n",
    "        print(f\" Solution {i}: {values(x, sol=i)}\")"
   ]
  }
 ],
 "metadata": {
  "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
}