{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "394ad00b",
   "metadata": {},
   "source": [
    "# Constraint *Count*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7fc4e2b2",
   "metadata": {},
   "source": [
    "The constraint *Count* imposes that the number of variables from a specified list of variables that take their values from a specified set (often, a single value) respects a numerical condition."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4a4bc46e",
   "metadata": {},
   "source": [
    "Below, we give several illustrations corresponding to representative use cases of the constraint *Count*. "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "dfe21ba1",
   "metadata": {},
   "source": [
    "## Case 1: AtLeast1"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "401820c3",
   "metadata": {},
   "source": [
    "The first case is when at least 1 variable from a specified list must take a specified value."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e9effd9d",
   "metadata": {},
   "source": [
    "To see how this constraint works, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "fb325926",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "15c0d15e",
   "metadata": {},
   "source": [
    "For our illustration, we introduce an array $x$ of 4 variables, each one with  {0,1,2}  as domain."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "576db332",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=4, dom=range(3))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4b65ff1c",
   "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": "5b9deb12",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Array of variable x:  [x[0], x[1], x[2], x[3]]\n",
      "Domain of any variable:  0..2\n"
     ]
    }
   ],
   "source": [
    "print(\"Array of variable x: \", x)\n",
    "print(\"Domain of any variable: \", x[0].dom)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "552fe6b0",
   "metadata": {},
   "source": [
    "We simply post a single constraint *Count*: at least 1 variable of $x$ must take the value 1."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "3ae9b1c8",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Count(x, value=1) >= 1\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ad46f5c8",
   "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": "3aea8bd7",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 0, 0, 1]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "51ff2f2f",
   "metadata": {},
   "source": [
    "One can infer that the number of solutions (supports) for this constraint is $3^4 - 2^4$. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "904b6532",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Last found solution:  [2, 1, 1, 1]\n",
      "Number of solutions:  65\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": "bb3b1492",
   "metadata": {},
   "source": [
    "## Case 2: AtMost1"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bcae42dc",
   "metadata": {},
   "source": [
    "The second case is when at most 1 variable from a specified list must take a specified value."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "770e4822",
   "metadata": {},
   "source": [
    "To start, we remove the last posted constraint by calling the function *unpost()*. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "da1d7b89",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e2e26bfe",
   "metadata": {},
   "source": [
    "We control that there are no more constraints."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "d755cfb8",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[]\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3d1b3ede",
   "metadata": {},
   "source": [
    "We post a single constraint *Count*: at most 1 variable of $x$ must take the value 0."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "328c30ff",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Count(x, value=0) <= 1\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3b167f95",
   "metadata": {},
   "source": [
    "We can call the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "b399659b",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 1, 1, 1]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3e661973",
   "metadata": {},
   "source": [
    "One can infer that the number of solutions (supports) for this constraint is $2^4  + 4 \\times 2^3=48$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "301422ca",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Last found solution:  [2, 2, 2, 1]\n",
      "Number of solutions:  48\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": "c45ccc79",
   "metadata": {},
   "source": [
    "## Case 3: ExactlyK"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "90050237",
   "metadata": {},
   "source": [
    "The third case is when exactly k variables from a specified list must take a specified value."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c0b1751b",
   "metadata": {},
   "source": [
    "To start, we remove the last posted constraint by calling the function *unpost()*. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "029235b4",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b902d91f",
   "metadata": {},
   "source": [
    "We post a single constraint *Count*: exactly 2 variables of $x$ must take the value 2."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "158a4ee2",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Count(x, value=2) == 2\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "df4c6aff",
   "metadata": {},
   "source": [
    "Interestingly, we can display the internal representation of the posted constraint; although a little bit technical, we can see that the information is correctly recorded (note that 'eq' stands for 'equal to')."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "a1e562b1",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "count(list:[x[0], x[1], x[2], x[3]], values:[2], condition:(eq,2))\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3db506ec",
   "metadata": {},
   "source": [
    "We can call the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "e8395541",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 0, 2, 2]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b95f2bc7",
   "metadata": {},
   "source": [
    "One can infer that the number of solutions (supports) for this constraint is ${4 \\choose 2} \\times 2^2=24$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "15654c0a",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Last found solution:  [1, 2, 2, 0]\n",
      "Number of solutions:  24\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": "2dbdb37b",
   "metadata": {},
   "source": [
    "## Case 4: Count Defined by a Variable"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1b82547c",
   "metadata": {},
   "source": [
    "The fouth case is when a variable is used to represent (count) the number of variables from a specified list that take a specified value."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "58fa911b",
   "metadata": {},
   "source": [
    "To start, we remove the last posted constraint by calling the function *unpost()*. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "d0c360bb",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bc905a2d",
   "metadata": {},
   "source": [
    "We introduce a variable, used for recording the \"counting\"."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "69362403",
   "metadata": {},
   "outputs": [],
   "source": [
    "y = Var(range(5))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0896e423",
   "metadata": {},
   "source": [
    "We post a single constraint Count: the number of variables of $x$ that take the value 1 is $y$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "id": "22b06b58",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Count(x, value=1) == y\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "98216a17",
   "metadata": {},
   "source": [
    "We can call the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "id": "15557a5a",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 0, 0, 0] 0\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x), value(y))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bf36bd36",
   "metadata": {},
   "source": [
    "For any tuple that can be built from $x$, which is $3^4$, the value of $y$ can be determined."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "id": "6010324f",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Last found solution:  [1, 2, 0, 0] 1\n",
      "Number of solutions:  81\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    print(\"Last found solution: \", values(x), value(y))\n",
    "    print(\"Number of solutions: \", n_solutions())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3c5cc3bb",
   "metadata": {},
   "source": [
    "## Case 5: Among"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "86778338",
   "metadata": {},
   "source": [
    "The fifth case is when exactly k variables from a specified list must take a specified value."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2a333ae2",
   "metadata": {},
   "source": [
    "First of all, we need to remove everything that has been introduced so far."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "id": "cb10230a",
   "metadata": {},
   "outputs": [],
   "source": [
    "clear()  # to clear previously posted variables and constraints"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "443e9ced",
   "metadata": {},
   "source": [
    "We re-introduce an array $x$ of 4 variables, each one with  {0,1,2}  as domain."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "id": "b19eeaf3",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=4, dom=range(3))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "de1dd58c",
   "metadata": {},
   "source": [
    "We post a single constraint Count: the number of variables of $x$ that take their values among $\\{0,2\\}$ must be equal to 3."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "id": "b69117d4",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Count(x, values=[1,2]) == 3\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e5338d5f",
   "metadata": {},
   "source": [
    "We can call the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "id": "fb5ff76d",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 1, 1, 1]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9da6f5f9",
   "metadata": {},
   "source": [
    "## Case 6: Count on Expressions"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "de020c9d",
   "metadata": {},
   "source": [
    "The sixth case is when we count the number of occurrences of a specified value over a list of expressions. "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "616bf43e",
   "metadata": {},
   "source": [
    "To start, we remove the last posted constraint by calling the function *unpost()*. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "id": "dc6768c3",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4a05e2f3",
   "metadata": {},
   "source": [
    "We post a single constraint Count: the number of expressions that take the value 3 is 2."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "id": "4e97c74f",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Count([x[0]+x[1], x[1]+x[2], x[2]+x[3]], value=3) == 2\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2849340a",
   "metadata": {},
   "source": [
    "By enumerating the solutions, one can observe that two expressions are always evaluated as the value 3."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "id": "2a607963",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 1, 2, 1]\n",
      "Solution 2: [0, 2, 1, 2]\n",
      "Solution 3: [1, 2, 1, 0]\n",
      "Solution 4: [1, 2, 1, 1]\n",
      "Solution 5: [1, 1, 2, 1]\n",
      "Solution 6: [2, 2, 1, 2]\n",
      "Solution 7: [2, 1, 2, 0]\n",
      "Solution 8: [2, 1, 2, 2]\n",
      "Solution 9: [1, 2, 2, 1]\n",
      "Solution 10: [2, 1, 1, 2]\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)}\")"
   ]
  }
 ],
 "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
}