{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "ead7f8c4",
   "metadata": {},
   "source": [
    "# Constraint *Maximum*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "de7b3fdc",
   "metadata": {},
   "source": [
    "The constraint *Maximum* ensures that the maximal value among those assigned to the variables of a specified list $x$ respects a numerical condition."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "148939a0",
   "metadata": {},
   "source": [
    "In PyCSP$^3$, we must call the function *Maximum()* that allows us to pass the variables either in sequence (individually) or under the form of a list. The object obtained when calling *Maximum()* must be restricted by a condition (typically, defined by a relational operator and a limit)."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "379e4006",
   "metadata": {},
   "source": [
    "Below, we give several illustrations corresponding to representative use cases of the constraint *Maximum*."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0e26f53c",
   "metadata": {},
   "source": [
    "## Case 1: Maximum Greater Than a Constant"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "aae266c1",
   "metadata": {},
   "source": [
    "We consider the case where we have a list of variables whose maximum must be greater than a constant."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "09d815cc",
   "metadata": {},
   "source": [
    "To see how this constraint works, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "ee65f363",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6fd481eb",
   "metadata": {},
   "source": [
    "For our illustration, we introduce an array $x$ of 4 variables, each variable having {0,1,2,3}  as domain."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "1c85cdb9",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=4, dom=range(4))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d4b8032d",
   "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": "f7b6e0c9",
   "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..3\n"
     ]
    }
   ],
   "source": [
    "print(\"Array of variable x: \", x)\n",
    "print(\"Domain of any variable: \", x[0].dom)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2f52f0ae",
   "metadata": {},
   "source": [
    "We simply post a single constraint *Maximum* imposing that the maximal value among those assigned to the variables of $x$ is strictly greater than 1."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "c71d5d09",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Maximum(x) > 1\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "450f4d23",
   "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": "f2cba76c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Values of x:  [0, 0, 0, 2]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Values of x: \", values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "38b23a1f",
   "metadata": {},
   "source": [
    "On this simple constraint, one can infer that the number of solutions (supports) is 240, out of $4^4 = 256$ possible tuples."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "eef140e4",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Last solution:  [2, 1, 0, 1]\n",
      "Number of solutions:  240\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    print(\"Last solution: \", values(x))\n",
    "    print(\"Number of solutions: \", n_solutions())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f5676f8e",
   "metadata": {},
   "source": [
    "## Case 2: Maximum Equal to a Variable"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "21f95988",
   "metadata": {},
   "source": [
    "Now, we consider the case where we have a list of variables whose maximum must be equal to a variable."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "43b73cdd",
   "metadata": {},
   "source": [
    "First of all, we need to remove everything that has been introduced so far."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "c6430262",
   "metadata": {},
   "outputs": [],
   "source": [
    "clear()  # to clear previously posted variables and constraints"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2059bb98",
   "metadata": {},
   "source": [
    "Then, we introduce an array $x$ of 4 variables and a stand-alone variable $y$, each variable having {0,1,2}  as domain."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "e2ce572d",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=4, dom=range(3))\n",
    "y = Var(range(3))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "42db16e5",
   "metadata": {},
   "source": [
    "We simply post a single constraint *Maximum* imposing that the maximal value among those assigned to the variables of $x$ is equal to the value assigned to $y$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "448cf9d6",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Maximum(x) == y\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "149ae95e",
   "metadata": {},
   "source": [
    "We can run the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "e94f613f",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Values of x:  [0, 0, 0, 0]\n",
      "Value of y:  0\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Values of x: \", values(x))\n",
    "    print(\"Value of y: \", value(y))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8443bbc1",
   "metadata": {},
   "source": [
    "Note that there are exactly 81 solutions (5-tuples called supports) for this constraint, among the $3^5=243$ possible tuples (corresponding to the Cartesian product of the domains)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "936027a2",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Last solution:  [1, 1, 1, 1]   1\n",
      "Number of solutions:  81\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    print(\"Last solution: \", values(x), \" \", value(y))\n",
    "    print(\"Number of solutions: \", n_solutions())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "51a5a795",
   "metadata": {},
   "source": [
    "Let us now arbitrarily set the value of $y$ to 1."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "f7d079d5",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    y == 1\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "39f2752b",
   "metadata": {},
   "source": [
    "We can display all solutions as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "0c33a0d7",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 0, 0, 1] 1\n",
      "Solution 2: [0, 0, 1, 1] 1\n",
      "Solution 3: [0, 0, 1, 0] 1\n",
      "Solution 4: [0, 1, 1, 0] 1\n",
      "Solution 5: [0, 1, 0, 0] 1\n",
      "Solution 6: [0, 1, 0, 1] 1\n",
      "Solution 7: [0, 1, 1, 1] 1\n",
      "Solution 8: [1, 1, 1, 1] 1\n",
      "Solution 9: [1, 1, 1, 0] 1\n",
      "Solution 10: [1, 1, 0, 0] 1\n",
      "Solution 11: [1, 1, 0, 1] 1\n",
      "Solution 12: [1, 0, 0, 1] 1\n",
      "Solution 13: [1, 0, 0, 0] 1\n",
      "Solution 14: [1, 0, 1, 0] 1\n",
      "Solution 15: [1, 0, 1, 1] 1\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)} {value(y, sol=i)}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d7a837bf",
   "metadata": {},
   "source": [
    "Although this is not the most efficient way of doing that (at each call to the function solve(), a new instance is generated and the solver is loaded; so, in the future, we plan to be able to let the solver alive), we can also enumerate all solutions (supports) of the constraint as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "44acf403",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 0, 0, 1]  1\n",
      "Solution 2: [1, 0, 0, 0]  1\n",
      "Solution 3: [1, 0, 0, 1]  1\n",
      "Solution 4: [0, 1, 0, 0]  1\n",
      "Solution 5: [0, 1, 0, 1]  1\n",
      "Solution 6: [1, 1, 0, 0]  1\n",
      "Solution 7: [1, 1, 0, 1]  1\n",
      "Solution 8: [0, 0, 1, 0]  1\n",
      "Solution 9: [0, 1, 1, 0]  1\n",
      "Solution 10: [0, 0, 1, 1]  1\n",
      "Solution 11: [0, 1, 1, 1]  1\n",
      "Solution 12: [1, 0, 1, 0]  1\n",
      "Solution 13: [1, 1, 1, 0]  1\n",
      "Solution 14: [1, 0, 1, 1]  1\n",
      "Solution 15: [1, 1, 1, 1]  1\n"
     ]
    }
   ],
   "source": [
    "cnt = 0\n",
    "while solve(solver=CHOCO) is SAT:\n",
    "    cnt += 1\n",
    "    print(f\"Solution {cnt}: {values(x)}  {value(y)}\")\n",
    "    satisfy(\n",
    "        x != values(x)\n",
    "    )"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5f1369b4",
   "metadata": {},
   "source": [
    "## Case 3: Maximum of Expressions"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f737d8dc",
   "metadata": {},
   "source": [
    "Finally, we consider the case where we have a list of expressions whose maximum must be greater than a constant."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c68b0f92",
   "metadata": {},
   "source": [
    "First of all, we need to remove everything that has been introduced so far."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "947d525d",
   "metadata": {},
   "outputs": [],
   "source": [
    "clear()  # to clear previously posted variables and constraints"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "01da63f3",
   "metadata": {},
   "source": [
    "Then, we introduce an array $x$ of 4 variables, each variable having {0,1,2,3}  as domain."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "ae421e07",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=4, dom=range(4))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b811ff45",
   "metadata": {},
   "source": [
    "We post a single constraint *Maximum* imposing that the maximal value among the specified expressions is greater than or equal to 3."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "ba2a475b",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Maximum(x[0]+x[1], x[1]+x[2], x[2]+x[3]) >= 5\n",
    ");"
   ]
  },
  {
   "cell_type": "raw",
   "id": "a3e7b6bb",
   "metadata": {},
   "source": [
    "We can run the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "89c6b4da",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Values of x:  [0, 0, 2, 3]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Values of x: \", values(x))"
   ]
  }
 ],
 "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
}