{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "8f4deef8",
   "metadata": {},
   "source": [
    "# Constraint *Channel*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "05b84bb0",
   "metadata": {},
   "source": [
    "The constraint *Channel* is used to make some connections between variables (from correspondances between their assigned values). Actually, there are three variants of the constraint *Channel*."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a8240e4b",
   "metadata": {},
   "source": [
    "## Variant 1"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "eb84e216",
   "metadata": {},
   "source": [
    "We consider the variant 1 of the constraint *Channel*. It is defined on a single list $x$ of variables, and ensures that if the ith variable of the list is assigned the value $j$, then the jth variable of the same list must be assigned the value $i$. We have:\n",
    "> $x_i = j \\Rightarrow x_j=i$"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fa4712b5",
   "metadata": {},
   "source": [
    "To see how this constraint works, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "f5093871",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1be023fd",
   "metadata": {},
   "source": [
    "For our illustration, we introduce an array $x$ of $5$ variables."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "da9c6a1a",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=5, dom=range(5))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "61681e67",
   "metadata": {},
   "source": [
    "Now, we can post a single constraint *Channel*, as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "29e3e714",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Channel(x)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c9cf6729",
   "metadata": {},
   "source": [
    "By calling the function $solve()$, we can check that the problem (actually, the single constraint) is satisfiable (SAT). We can also display the values assigned to the variables in the found solution; we can call the function *values()* that collects the values assigned (in the last found solution) to a specified list of variables."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "cb61f995",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[0, 1, 2, 3, 4]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a2b4aca9",
   "metadata": {},
   "source": [
    "By the way, how many solutions (supports) does there exist for our constraint taken alone? The reader can try to prove that it is 26. We can check this by calling *solve()* with the named parameter *sols*. Note how the named parameter *sol* of *values()* is used to indicate the index of a solution."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "222871be",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 1, 2, 3, 4]\n",
      "Solution 2: [0, 1, 2, 4, 3]\n",
      "Solution 3: [0, 1, 4, 3, 2]\n",
      "Solution 4: [0, 1, 3, 2, 4]\n",
      "Solution 5: [0, 4, 3, 2, 1]\n",
      "Solution 6: [0, 4, 2, 3, 1]\n",
      "Solution 7: [0, 3, 2, 1, 4]\n",
      "Solution 8: [0, 3, 4, 1, 2]\n",
      "Solution 9: [0, 2, 1, 4, 3]\n",
      "Solution 10: [0, 2, 1, 3, 4]\n",
      "Solution 11: [1, 0, 2, 3, 4]\n",
      "Solution 12: [1, 0, 4, 3, 2]\n",
      "Solution 13: [2, 1, 0, 3, 4]\n",
      "Solution 14: [4, 1, 2, 3, 0]\n",
      "Solution 15: [2, 4, 0, 3, 1]\n",
      "Solution 16: [4, 2, 1, 3, 0]\n",
      "Solution 17: [3, 2, 1, 0, 4]\n",
      "Solution 18: [1, 0, 3, 2, 4]\n",
      "Solution 19: [3, 1, 2, 0, 4]\n",
      "Solution 20: [2, 3, 0, 1, 4]\n",
      "Solution 21: [4, 3, 2, 1, 0]\n",
      "Solution 22: [3, 1, 4, 0, 2]\n",
      "Solution 23: [3, 4, 2, 0, 1]\n",
      "Solution 24: [1, 0, 2, 4, 3]\n",
      "Solution 25: [2, 1, 0, 4, 3]\n",
      "Solution 26: [4, 1, 3, 2, 0]\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    for i in range(n_solutions()):\n",
    "        print(f\"Solution {i+1}: {values(x, sol=i)}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ddc43c38",
   "metadata": {},
   "source": [
    "## Variant 2"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5639f39f",
   "metadata": {},
   "source": [
    "We consider the variant 2 of the constraint *Channel*, sometimes called *Inverse* or *Assignment* in the literature: it is defined from two separate lists $x$ and $y$ (of the same size) of variables. \n",
    "It ensures that the value assigned to the ith variable of the first list gives the position of the variable of the second list that is assigned to $i$, and vice versa. We have:\n",
    "> $x_i = j \\Leftrightarrow y_j = i$."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3fc5b16c",
   "metadata": {},
   "source": [
    "First of all, we need to remove everything that has been introduced so far."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "0ac3a3a2",
   "metadata": {},
   "outputs": [],
   "source": [
    "clear()  # to clear previously posted variables and constraints"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2096da3b",
   "metadata": {},
   "source": [
    "For our illustration, we introduce two arrays $x$ and $y$ of $4$ variables."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "0a98ba61",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=4, dom=range(4))\n",
    "y = VarArray(size=4, dom=range(4))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "950c57ba",
   "metadata": {},
   "source": [
    "Now, we can post a single constraint *Channel* as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "33cf7978",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Channel(x, y)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "249cef30",
   "metadata": {},
   "source": [
    "By calling the function *solve()*, we can check that the problem (actually, the single constraint) is satisfiable (SAT). We can also display the values assigned to the variables in the found solution."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "066464f3",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[0, 1, 2, 3] [0, 1, 2, 3]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(values(x), values(y))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "71ae92a6",
   "metadata": {},
   "source": [
    "We can enumerate all solutions as follows: "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "a432f143",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 1, 2, 3], [0, 1, 2, 3]\n",
      "Solution 2: [0, 1, 3, 2], [0, 1, 3, 2]\n",
      "Solution 3: [0, 3, 1, 2], [0, 2, 3, 1]\n",
      "Solution 4: [0, 3, 2, 1], [0, 3, 2, 1]\n",
      "Solution 5: [0, 2, 3, 1], [0, 3, 1, 2]\n",
      "Solution 6: [0, 2, 1, 3], [0, 2, 1, 3]\n",
      "Solution 7: [1, 2, 0, 3], [2, 0, 1, 3]\n",
      "Solution 8: [1, 0, 2, 3], [1, 0, 2, 3]\n",
      "Solution 9: [2, 1, 0, 3], [2, 1, 0, 3]\n",
      "Solution 10: [2, 0, 1, 3], [1, 2, 0, 3]\n",
      "Solution 11: [3, 0, 1, 2], [1, 2, 3, 0]\n",
      "Solution 12: [3, 0, 2, 1], [1, 3, 2, 0]\n",
      "Solution 13: [2, 0, 3, 1], [1, 3, 0, 2]\n",
      "Solution 14: [1, 0, 3, 2], [1, 0, 3, 2]\n",
      "Solution 15: [1, 2, 3, 0], [3, 0, 1, 2]\n",
      "Solution 16: [2, 1, 3, 0], [3, 1, 0, 2]\n",
      "Solution 17: [3, 1, 0, 2], [2, 1, 3, 0]\n",
      "Solution 18: [3, 1, 2, 0], [3, 1, 2, 0]\n",
      "Solution 19: [1, 3, 2, 0], [3, 0, 2, 1]\n",
      "Solution 20: [2, 3, 1, 0], [3, 2, 0, 1]\n",
      "Solution 21: [3, 2, 1, 0], [3, 2, 1, 0]\n",
      "Solution 22: [1, 3, 0, 2], [2, 0, 3, 1]\n",
      "Solution 23: [2, 3, 0, 1], [2, 3, 0, 1]\n",
      "Solution 24: [3, 2, 0, 1], [2, 3, 1, 0]\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    for i in range(n_solutions()):\n",
    "        print(f\"Solution {i+1}: {values(x, sol=i)}, {values(y, sol=i)}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4dd14b9e",
   "metadata": {},
   "source": [
    "It is also possible to use this form of *Channel*, with two lists of different sizes.\n",
    "The constraint then imposes restrictions on all variables of the first list, but not on all variables of the second list. The syntax is the same, but the semantics is the following (note that the equivalence has been replaced by an implication):\n",
    ">  $x_i = j \\Rightarrow y_j = i$ "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "67cf625f",
   "metadata": {},
   "source": [
    "## Variant 3"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "69c76fbc",
   "metadata": {},
   "source": [
    "We consider the variant 3 of the constraint *Channel*: it is obtained by considering a list $x$ of 0/1 variables to be channeled with an integer variable $v$. This third form of constraint *Channel* ensures that the only variable of the list that is assigned to 1 is at an index (position) that corresponds to the value assigned to the stand-alone integer variable. We have:\n",
    ">  $x_i = 1 \\Leftrightarrow v = i$"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f91abe17",
   "metadata": {},
   "source": [
    "First of all, we need to remove everything that has been introduced so far."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "14c9880c",
   "metadata": {},
   "outputs": [],
   "source": [
    "clear()  # to clear previously posted variables and constraints"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "db269443",
   "metadata": {},
   "source": [
    "We introduce an array $x$ of 0/1 variables, and a stand-alone variable $v$ that will play the role of value."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "a7425f9a",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=6, dom={0,1})\n",
    "v = Var(range(6))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5d018e25",
   "metadata": {},
   "source": [
    "Now, we can post the constraint *Channel*:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "f380459c",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Channel(x,v)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "99259a44",
   "metadata": {},
   "source": [
    "We can call the function *solve()*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "6d69a433",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[0, 0, 0, 0, 0, 1] 5\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(values(x), value(v))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "838dd034",
   "metadata": {},
   "source": [
    "We can enumerate all solutions:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "18f7ec98",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 0, 0, 0, 0, 1]  5 \n",
      "Solution 2: [0, 0, 0, 0, 1, 0]  4 \n",
      "Solution 3: [0, 0, 0, 1, 0, 0]  3 \n",
      "Solution 4: [0, 0, 1, 0, 0, 0]  2 \n",
      "Solution 5: [0, 1, 0, 0, 0, 0]  1 \n",
      "Solution 6: [1, 0, 0, 0, 0, 0]  0 \n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    for k in range(n_solutions()):\n",
    "        print(f\"Solution {k+1}: {values(x, sol=k)}  {value(v, sol=k)} \")"
   ]
  }
 ],
 "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
}