{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "943b07ed",
   "metadata": {},
   "source": [
    "# Constraint *NValues*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "030ee6b0",
   "metadata": {},
   "source": [
    "The constraint *NValues* ensures that the number of distinct values taken by the variables of a specified list $x$ respects a numerical condition. For example, the number of distinct values in $x$ must be less than or equal to a constant."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "01eedc24",
   "metadata": {},
   "source": [
    "Below, we give several illustrations corresponding to representative use cases of the constraint *NValues*. "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e6aff0ee",
   "metadata": {},
   "source": [
    "## Case 1: Number of Distinct Values as a Constant"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "03517cf7",
   "metadata": {},
   "source": [
    "The first case is when the number of distinct values taken by a list of variables is constrained by a constant (limit)."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d29f6c67",
   "metadata": {},
   "source": [
    "To see how this constraint works, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "a1d145a2",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b0790af0",
   "metadata": {},
   "source": [
    "For our illustration, we introduce an array $x$ of 5 variables, each one with  {0,1,2,3}  as domain."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "8c23b6ca",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=5, dom=range(4))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "cf471726",
   "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": "b28ce67f",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Array of variable x:  [x[0], x[1], x[2], x[3], x[4]]\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": "c3d7d9eb",
   "metadata": {},
   "source": [
    "We simply post a single constraint *NValues*: the number of distinct values assigned to the variables of $x$ must be less than or equal to 2:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "f665145e",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    NValues(x) <= 2\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e3f591c5",
   "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": "bd414b9d",
   "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))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8f32a6a1",
   "metadata": {},
   "source": [
    "On can check that the number of solutions (supports) for our constraint is $4 + {4 \\choose 2} \\times 2 \\times ({5 \\choose 1} + {5 \\choose 2})$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "c6c452c8",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Last found solution:  [2, 0, 2, 2, 0]\n",
      "Number of solutions:  184\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": "e97a2c22",
   "metadata": {},
   "source": [
    "## Case 2: Number of Distinct Values as a Variable"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "539499ff",
   "metadata": {},
   "source": [
    "The second case is when the number of distinct values taken by a list of variables is constrained by a variable (limit)."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7a0c9844",
   "metadata": {},
   "source": [
    "To start, we remove the last posted constraint by calling the function *unpost()*. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "565d93dc",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8c222bc2",
   "metadata": {},
   "source": [
    "We control that there are no more constraints."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "beb1a062",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[]\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c6e9da91",
   "metadata": {},
   "source": [
    "We introduce a stand-alone variable $y$ that will be useful to \"compute\" the number of distinct values in $x$. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "68330002",
   "metadata": {},
   "outputs": [],
   "source": [
    "y = Var(range(1, 6))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bea26e22",
   "metadata": {},
   "source": [
    "We post a single constraint *NValues*:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "ac8c04ea",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    NValues(x) == y\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "866ca08d",
   "metadata": {},
   "source": [
    "And we run the solver to find a first solution."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "f5d6a9c1",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 0, 0, 0, 0] 1\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x), value(y))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "eecdc5d8",
   "metadata": {},
   "source": [
    "One can prove rather easily that the number of solutions is $4^5$. We can display the last ten solutions."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "fcedc338",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Number of solutions:  1024\n",
      "Solution 1024: x=[3, 0, 1, 3, 2]  y=4\n",
      "Solution 1023: x=[2, 0, 1, 3, 2]  y=4\n",
      "Solution 1022: x=[2, 0, 3, 3, 1]  y=4\n",
      "Solution 1021: x=[2, 0, 1, 3, 1]  y=4\n",
      "Solution 1020: x=[2, 0, 0, 3, 1]  y=4\n",
      "Solution 1019: x=[2, 3, 0, 3, 1]  y=4\n",
      "Solution 1018: x=[2, 3, 1, 3, 0]  y=4\n",
      "Solution 1017: x=[2, 0, 1, 3, 0]  y=4\n",
      "Solution 1016: x=[2, 1, 1, 3, 0]  y=4\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    print(\"Number of solutions: \", n_solutions())\n",
    "    for i in range(1, 10):\n",
    "        print(f\"Solution {n_solutions()-i+1}: x={values(x, sol=-i)}  y={value(y,sol=-i)}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9cdbe4ee",
   "metadata": {},
   "source": [
    "## Case 3: Number of Distinct Expressions"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6c6e0010",
   "metadata": {},
   "source": [
    "The third case is when the number of distinct values taken by a list of expressions is constrained by a constant."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "15f623e6",
   "metadata": {},
   "source": [
    "First of all, we need to remove everything that has been introduced so far."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "ea9fb10c",
   "metadata": {},
   "outputs": [],
   "source": [
    "clear()  # to clear previously posted variables and constraints"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "af731841",
   "metadata": {},
   "source": [
    "We introduce an array $x$ of 5 variables, each one with {0,1,2,3} as domain."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "c9319900",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=5, dom=range(4))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0ddfa4e0",
   "metadata": {},
   "source": [
    "We post a single constraint *NValues* on expressions:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "aedcba40",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    NValues(x[0]+x[1], x[1]+x[2], x[2]+x[3], x[3]+x[4]) > 2\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "401a7e2c",
   "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 'gt' stands for '(strictly) greater than')."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "74f502c7",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "nValues(list:[add(x[0],x[1]), add(x[1],x[2]), add(x[2],x[3]), add(x[3],x[4])], condition:(gt,2))\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "raw",
   "id": "8b5f5975",
   "metadata": {},
   "source": [
    "We can run the solver"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "bb2265bc",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 0, 0, 1, 1] 4\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x), value(y))"
   ]
  }
 ],
 "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
}