{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "492d8080",
   "metadata": {},
   "source": [
    "# Constraint *Cardinality*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c8e22963",
   "metadata": {},
   "source": [
    "The constraint *Cardinality*, also called *GlobalCardinality* or *gcc* in the literature, ensures that the number of occurrences of each value in a specified set, taken by the variables of a specified list, is equal to a specified value (or variable), or belongs to a specified interval. A dictionay called *occurrences* is used to store that kind of information."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c70deab5",
   "metadata": {},
   "source": [
    "Below, we give several illustrations corresponding to representative use cases of the constraint *Cardinality*."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "24c0e8f9",
   "metadata": {},
   "source": [
    "## Case 1: Cardinality with Exact Numbers of Occurrences"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fc8fa939",
   "metadata": {},
   "source": [
    "We consider the case where we have a list of variables and a dictionay indicating for each value (key), the exact number of expected occurrences (value) with a constant. "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6ea3ff6d",
   "metadata": {},
   "source": [
    "To see how this constraint works, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "735ddc49",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b163f2f9",
   "metadata": {},
   "source": [
    "We introduce an array $x$ of $8$ variables, each one with {0,1,2,3} as domain."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "87480a73",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=8, dom=range(4))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "46a52815",
   "metadata": {},
   "source": [
    "We can display (the structure of) the array as well as the domain of the first variable."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "6fa10017",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Array of variable x:  [x[0], x[1], x[2], x[3], x[4], x[5], x[6], x[7]]\n",
      "Domain of any variable:  0..3\n"
     ]
    }
   ],
   "source": [
    "print(\"Array of variable x: \",x)\n",
    "print(\"Domain of any variable: \", x[0].dom)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e8751d68",
   "metadata": {},
   "source": [
    "We simply post a single constraint *Cardinality*: \n",
    "- the number of occurrences of the value 0 must be 1\n",
    "- the number of occurrences of the value 1 must be 2\n",
    "- the number of occurrences of the value 2 must be 3\n",
    "- the number of occurrences of the value 3 must be 2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "f8ae3710",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Cardinality(x, occurrences={0:1, 1:2, 2:3, 3:2})\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f5471df3",
   "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; 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": 5,
   "id": "4eb7fd0d",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 1, 1, 2, 2, 2, 3, 3]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8dd788d9",
   "metadata": {},
   "source": [
    "On can check that the number of solutions (supports) for our constraint is ${8 \\choose 1} \\times {7 \\choose 2} \\times {5 \\choose 2}$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "8dfd49f6",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Last found solution:  [2, 2, 0, 2, 1, 3, 3, 1]\n",
      "Number of solutions:  1680\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    print(\"Last found solution: \", values(x))\n",
    "    print(\"Number of solutions: \", n_solutions())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "25f1dcf7",
   "metadata": {},
   "source": [
    "## Case 2: Cardinality with Ranges of Occurrences"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "dce6d63b",
   "metadata": {},
   "source": [
    "We consider now the case where we have a list of variables and a dictionay indicating for each value (key), an interval of expected occurrences (value). "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "dac2e094",
   "metadata": {},
   "source": [
    "First of all, we need to remove everything that has been introduced so far."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "e9e392b7",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b9900f0d",
   "metadata": {},
   "source": [
    "We control that there are no more constraints."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "ffcb2dae",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[]\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "44b6b60c",
   "metadata": {},
   "source": [
    "We post a single constraint *Cardinality*:\n",
    "- the number of occurrences of the value 0 must be 1\n",
    "- the number of occurrences of the value 1 must be between 2 and 3\n",
    "- the number of occurrences of the value 2 must be between 2 and 3\n",
    "- the number of occurrences of the value 3 must be between 1 and 3"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "4a4eebc5",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Cardinality(x, occurrences={0:1, 1:range(2,4), 2:range(2,4), 3:range(1,4)})\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e4db2688",
   "metadata": {},
   "source": [
    "Interstingly, we can display the internal representation of the posted constraint; although a little bit technical, we can see that the information about occurrences is correct. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "241aa5f3",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "cardinality(list:[x[0], x[1], x[2], x[3], x[4], x[5], x[6], x[7]], values:[0, 1, 2, 3], occurs:[1, 2..3, 2..3, 1..3])\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8d2f78d0",
   "metadata": {},
   "source": [
    "We can run again the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "e1c4519b",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 1, 1, 1, 2, 2, 2, 3]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f2117f78",
   "metadata": {},
   "source": [
    "And we can enumerate the 15 first solutions (supports) for this constraint."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "a0041898",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 1, 1, 1, 2, 2, 2, 3]\n",
      "Solution 2: [0, 1, 1, 1, 2, 2, 3, 3]\n",
      "Solution 3: [0, 1, 1, 1, 2, 2, 3, 2]\n",
      "Solution 4: [0, 1, 1, 1, 2, 3, 3, 2]\n",
      "Solution 5: [0, 1, 1, 1, 2, 3, 2, 2]\n",
      "Solution 6: [0, 1, 1, 1, 2, 3, 2, 3]\n",
      "Solution 7: [0, 1, 1, 1, 3, 2, 2, 3]\n",
      "Solution 8: [0, 1, 1, 1, 3, 2, 2, 2]\n",
      "Solution 9: [0, 1, 1, 1, 3, 3, 2, 2]\n",
      "Solution 10: [0, 1, 1, 1, 3, 2, 3, 2]\n",
      "Solution 11: [0, 1, 1, 2, 3, 2, 3, 2]\n",
      "Solution 12: [0, 1, 1, 2, 3, 2, 1, 2]\n",
      "Solution 13: [0, 1, 1, 2, 3, 3, 1, 2]\n",
      "Solution 14: [0, 1, 1, 2, 3, 3, 2, 2]\n",
      "Solution 15: [0, 1, 1, 2, 3, 1, 2, 2]\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=15) is SAT:\n",
    "    for i in range(n_solutions()):\n",
    "        print(f\"Solution {i+1}: {values(x, sol=i)}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0376f091",
   "metadata": {},
   "source": [
    "## Case 3: Cardinality with a Variable Number of Occurrences"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "86e14502",
   "metadata": {},
   "source": [
    "We consider now the case where we have a list of variables and a dictionay indicating for each value (key), a number of expected occurrences represented by a variable. "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4752fb1b",
   "metadata": {},
   "source": [
    "To start, we remove the last posted constraint by calling the function *unpost()*. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "ebe29cc2",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8e31f61c",
   "metadata": {},
   "source": [
    "We control that there are no more constraints."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "66db3c00",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[]\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "72f90f3a",
   "metadata": {},
   "source": [
    "We introduce a second array of variables $y$ that will be used to store the number of occurrences of each value."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "1709af83",
   "metadata": {},
   "outputs": [],
   "source": [
    "y = VarArray(size=4, dom=range(9))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1fc5b216",
   "metadata": {},
   "source": [
    "We post a single constraint *Cardinality*:\n",
    "- the number of occurrences of the value 0 must be $y[0]$\n",
    "- the number of occurrences of the value 1 must be $y[1]$\n",
    "- the number of occurrences of the value 2 must be $y[2]$\n",
    "- the number of occurrences of the value 3 must be $y[3]$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "33d0db73",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Cardinality(x, occurrences={i:y[i] for i in range(4)})\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4bcfac39",
   "metadata": {},
   "source": [
    "We can display the internal representation of the posted constraint:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "f678a657",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "cardinality(list:[x[0], x[1], x[2], x[3], x[4], x[5], x[6], x[7]], values:[0, 1, 2, 3], occurs:[y[0], y[1], y[2], y[3]])\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "58ed7c18",
   "metadata": {},
   "source": [
    "We can run the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "d9499f6a",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 0, 0, 0, 0, 0, 0, 0]\n",
      "The number of occurrences of 0 is 8\n",
      "The number of occurrences of 1 is 0\n",
      "The number of occurrences of 2 is 0\n",
      "The number of occurrences of 3 is 0\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x))\n",
    "    for v in range(4):\n",
    "        print(f\"The number of occurrences of {v} is {value(y[v])}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "401268ea",
   "metadata": {},
   "source": [
    "One can anticipate that the number of solutions (supports) for this constraint is $4^8$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "id": "494cba32",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Last found solution:  [3, 3, 1, 1, 0, 3, 2, 2]\n",
      "Number of solutions:  65536\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    print(\"Last found solution: \", values(x))\n",
    "    print(\"Number of solutions: \", n_solutions())"
   ]
  }
 ],
 "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
}