{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "f2bc1bc8",
   "metadata": {},
   "source": [
    "# Constraint *Sum*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "25fd6b4c",
   "metadata": {},
   "source": [
    "The constraint *Sum* is one of the most important constraint. \n",
    "This constraint involves variables (and possibly coefficients), and is subject to a numerical condition. For example, a sum of variables in a list must be equal to a constant.\n",
    "Note that a form of *Sum*, sometimes called *subset-sum* or *Knapsack* involves the operator $\\mathtt{in}$, and ensures that the computed sum belongs to a specified interval."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1ad65f52",
   "metadata": {},
   "source": [
    "Below, we give several illustrations corresponding to representative use cases of the constraint *Sum*."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "df86a502",
   "metadata": {},
   "source": [
    "## Case 1: Simple Sum"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e3706a59",
   "metadata": {},
   "source": [
    "A basic form of the constraint *Sum* simply involves a list $x$ of variables."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "519ad2fd",
   "metadata": {},
   "source": [
    "To see how this constraint works, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "0225644a",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fcd65b0e",
   "metadata": {},
   "source": [
    "For our illustration, we introduce an array $x$ of 5 variables, each one with {1,2,3} as domain. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "28f3dc06",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=5, dom=range(1, 4))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e61f78dd",
   "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": "f05948e5",
   "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:  1..3\n"
     ]
    }
   ],
   "source": [
    "print(\"Array of variable x: \", x)\n",
    "print(\"Domain of any variable: \", x[0].dom)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1d827746",
   "metadata": {},
   "source": [
    "We simply post a single constraint *Sum*: the sum of the values assigned to the variables of $x$ must be equal to 10:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "77c7bba4",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Sum(x) == 12\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c700c1b6",
   "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": "475bbd00",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [1, 2, 3, 3, 3]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "80a04037",
   "metadata": {},
   "source": [
    "If ever we want to count the number of solutions, we can set the value ALL to the named parameter *sols*. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "ed0c709a",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Number of solutions:  30\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    print(\"Number of solutions: \", n_solutions())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "aed5a09a",
   "metadata": {},
   "source": [
    "Suppose now that we arbitrarily assign $x[0]$ to 1."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "ae0b3bac",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    x[0] == 1\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "95ec73be",
   "metadata": {},
   "source": [
    "The number of solutions is drastically reduced. Note how the named parameter *sol* of *values()* is used to indicate the index of a solution."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "f1d2739c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [1, 2, 3, 3, 3]\n",
      "Solution 2: [1, 3, 3, 2, 3]\n",
      "Solution 3: [1, 3, 2, 3, 3]\n",
      "Solution 4: [1, 3, 3, 3, 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)}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a88c6e26",
   "metadata": {},
   "source": [
    "And one can logically think that additionally arbitrarily assigning $x[1]$ to 1 makes the problem instance unsatisfiable."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "23e8a364",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    x[1] == 1\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f8c3fb95",
   "metadata": {},
   "source": [
    "We can check that no more solution exists because the result is now UNSAT."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "e8b80cbb",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Result:  UNSAT\n"
     ]
    }
   ],
   "source": [
    "print(\"Result: \", solve())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "97b665bd",
   "metadata": {},
   "source": [
    "## Case 2: Weighted Sum"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a803c84a",
   "metadata": {},
   "source": [
    "It is rather frequent to have variables accompanied with coefficients when performing a sum (we say that we deal with a weighted sum)."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d01be5a6",
   "metadata": {},
   "source": [
    "First of all, we need to remove everything that has been introduced so far."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "6884b45e",
   "metadata": {},
   "outputs": [],
   "source": [
    "clear()  # to clear previously posted variables and constraints"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "81241a2d",
   "metadata": {},
   "source": [
    "As earlier, we introduce an array $x$ of 5 variables, each one with {1,2,3} as domain. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "1240d6ea",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=5, dom=range(1, 4))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d1f2dfca",
   "metadata": {},
   "source": [
    "and we put some arbitrary coefficients in a list."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "4f2dff52",
   "metadata": {},
   "outputs": [],
   "source": [
    "c = [3, 2, 1, 4, 2]"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "eb571244",
   "metadata": {},
   "source": [
    "We can post a weighted constraint *Sum*: the weighted sum of the values assigned to the variables of $x$ must be strictly greater than 28:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "683788b2",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Sum(x[i] * c[i] for i in range(5)) > 28\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c9cce817",
   "metadata": {},
   "source": [
    "We can display the internal representation of the posted constraint; although a little bit technical, we can see that the weighted sum has been recognized (note that 'gt' stands for '(strictly) greater than')."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "aabd0a1a",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "sum(list:[x[0], x[1], x[2], x[3], x[4]], coeffs:[3, 2, 1, 4, 2], condition:(gt,28))\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6d00e4ba",
   "metadata": {},
   "source": [
    "We enumerate the 15 first solutions as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "5b07cb33",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [1, 3, 2, 3, 3]\n",
      "Solution 2: [1, 3, 3, 3, 3]\n",
      "Solution 3: [2, 3, 3, 3, 3]\n",
      "Solution 4: [2, 3, 3, 3, 1]\n",
      "Solution 5: [2, 3, 3, 3, 2]\n",
      "Solution 6: [2, 3, 1, 3, 2]\n",
      "Solution 7: [2, 3, 2, 3, 2]\n",
      "Solution 8: [2, 3, 2, 3, 3]\n",
      "Solution 9: [2, 3, 1, 3, 3]\n",
      "Solution 10: [2, 2, 1, 3, 3]\n",
      "Solution 11: [2, 2, 2, 3, 3]\n",
      "Solution 12: [2, 2, 3, 3, 3]\n",
      "Solution 13: [2, 1, 3, 3, 3]\n",
      "Solution 14: [2, 2, 3, 3, 2]\n",
      "Solution 15: [3, 2, 3, 3, 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": "950e0ce7",
   "metadata": {},
   "source": [
    "The curious reader can see the value 1 is never present in any solution fo the variable $x[3]$. Technically, this means that this value can be deleted by a filtering algorithm associated with the constraint *Sum*. "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bbcbab08",
   "metadata": {},
   "source": [
    "### Weighted Sum by Dot Product"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "cf7a9672",
   "metadata": {},
   "source": [
    "Now, we are going to post the same constraint, but this time by using a dot product notation."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "268f1ebc",
   "metadata": {},
   "source": [
    "We start by deleting the currently posted constraint by calling the function *unpost()* that discards the last call to *satisfy()*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "b371763f",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b72b194a",
   "metadata": {},
   "source": [
    "We control that there are no more constraints."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "932a5484",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[]\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b28aabd3",
   "metadata": {},
   "source": [
    "We can use a dot notation to post the constraint:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "id": "b8245287",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    x * c  > 28\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ecd8c01f",
   "metadata": {},
   "source": [
    "We check that everything is fine."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "id": "29b7303c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "sum(list:[x[0], x[1], x[2], x[3], x[4]], coeffs:[3, 2, 1, 4, 2], condition:(gt,28))\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "20d448a2",
   "metadata": {},
   "source": [
    "We still have 44 solutions."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "id": "9d8e64d4",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Number of solutions:  44\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    print(\"Number of solutions: \", n_solutions())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5ba1df83",
   "metadata": {},
   "source": [
    "Importantly, if we write $c * x$ instead of $x * c$, an error occurs. This is because it is not possible to use in this context the operator $*$ on lists of integers in Python. We need to transform the list of integers into a more specific list with the function cp_array(). So it would be correct to write:"
   ]
  },
  {
   "cell_type": "raw",
   "id": "b7291b1f",
   "metadata": {
    "raw_mimetype": "text/x-python"
   },
   "source": [
    "satisfy(\n",
    "    cp_array(c) * x  > 28\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5c56f459",
   "metadata": {},
   "source": [
    "However, most of the times, we directy use arrays (or sub-arrays) coming from the data of the model, loaded from a file, and they have the right type of list, and so, it is very rare to need to call cp_array() explicitly."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2bd8b719",
   "metadata": {},
   "source": [
    "## Case 3: Sum of Expressions"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2eada615",
   "metadata": {},
   "source": [
    "Sometimes, sums are built from general expressions. We give an illustration below."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "790035ec",
   "metadata": {},
   "source": [
    "First of all, we need to remove everything that has been introduced so far."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "id": "4ee7a08a",
   "metadata": {},
   "outputs": [],
   "source": [
    "clear()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e040365d",
   "metadata": {},
   "source": [
    "Then, we introduce an array $x$ of 4 variables, each one with {0,1,2,3} as domain. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "id": "2b2442f9",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=4, dom=range(4))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bdaf5005",
   "metadata": {},
   "source": [
    "Although there exist other ways of expressing this, let us suppose that we want to guarantee that the number of variables in $x$ with a value greater than or equal to 1 is at least 3. We can write:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "id": "aca04df2",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Sum(x[i] >= 2 for i in range(4))  >= 3\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2b735d39",
   "metadata": {},
   "source": [
    "We can enumerate the first 10 solutions satisfying that constraint:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "id": "350a35ee",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 2, 2, 2]\n",
      "Solution 2: [0, 2, 2, 3]\n",
      "Solution 3: [0, 2, 3, 3]\n",
      "Solution 4: [0, 2, 3, 2]\n",
      "Solution 5: [0, 3, 3, 2]\n",
      "Solution 6: [0, 3, 3, 3]\n",
      "Solution 7: [0, 3, 2, 3]\n",
      "Solution 8: [0, 3, 2, 2]\n",
      "Solution 9: [1, 3, 2, 2]\n",
      "Solution 10: [1, 3, 2, 3]\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=10) is SAT:\n",
    "    for i in range(n_solutions()):\n",
    "        print(f\"Solution {i+1}: {values(x, sol=i)}\")"
   ]
  }
 ],
 "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
}