{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "597d3e8b",
   "metadata": {
    "tags": [
     "Count"
    ]
   },
   "source": [
    "# Constraint *NoOverlap*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a5fb1313",
   "metadata": {},
   "source": [
    "The one dimensional form of constraint *NoOverlap*, also called *Disjunctive* in the literature ensures that some objects (e.g., tasks), defined by their origins (e.g., starting times) and lengths (e.g., durations), must not overlap."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d8cfd8e9",
   "metadata": {},
   "source": [
    "The k-dimensional form of constraint *NoOverlap*, also called *diffn*, ensures that, given a set of $k$-dimensional boxes; for any pair of such boxes, there exists at least one dimension where one box is after the other, i.e., the boxes do not overlap."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "444aa44d",
   "metadata": {},
   "source": [
    "In PyCSP$^3$, we must call the function *NoOverlap()* that requires either two named parameters called *origins* and *lengths* or, equivalently, a named parameter called *tasks*. It is also posible to use an optional parameter called *zero_ignored*. "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b261c74c",
   "metadata": {},
   "source": [
    "Below, we give several illustrations corresponding to representative use cases of the constraint *NoOverlap*."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "47c49891",
   "metadata": {},
   "source": [
    "## Case 1: NoOverlap with  Fixed Lengths"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "698e48b8",
   "metadata": {},
   "source": [
    "The first case if about the one dimensional form with lengths given by constants (integers)."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4a3b18a2",
   "metadata": {},
   "source": [
    "The arguments given to *origins* and *lengths* when calling the function *NoOverlap()* are expected to be lists of the same length; *origins* must be given a list of variables whereas * must be given a list of integers.  "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "570a1c4a",
   "metadata": {},
   "source": [
    "To see how this constraint works, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "27f4bdcf",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ac420acc",
   "metadata": {},
   "source": [
    "For our illustration, we introduce an array $x$ of 4 variables, each one with {0,1,2,3,4,5,6,7,8,9} as domain. We can imagine that $x$ represents the starting times of 4 tasks. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "f60dc3d5",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=4, dom=range(10))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d37439a8",
   "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": "10a92ad7",
   "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..9\n"
     ]
    }
   ],
   "source": [
    "print(\"Array of variable x: \", x)\n",
    "print(\"Domain of any variable: \", x[0].dom)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0e13dd15",
   "metadata": {},
   "source": [
    "Then, for the durations, we introduce an array $t$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "887d2c51",
   "metadata": {},
   "outputs": [],
   "source": [
    "t = [3,5,2,4]"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "10e54985",
   "metadata": {},
   "source": [
    "We simply post a single constraint *NoOverlap* from $x$ and $t$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "e0bb2cc2",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    NoOverlap(origins=x, lengths=t)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2179bd1f",
   "metadata": {},
   "source": [
    "Interestingly, we can display the internal representation of the posted constraints; we can see that the information is correctly recorded."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "ce0b87bf",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "noOverlap(origins:[x[0], x[1], x[2], x[3]], lengths:[3, 5, 2, 4])\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e51ec15c",
   "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": 7,
   "id": "3675e390",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Task 0 starts at 0 and lasts 3 unit(s) of time\n",
      "Task 1 starts at 9 and lasts 5 unit(s) of time\n",
      "Task 2 starts at 3 and lasts 2 unit(s) of time\n",
      "Task 3 starts at 5 and lasts 4 unit(s) of time\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    for i in range(4):\n",
    "        print(f\"Task {i} starts at {value(x[i])} and lasts {t[i]} unit(s) of time\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1f91c69f",
   "metadata": {},
   "source": [
    "One can enumerate the 30 solutions as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "3d0c3764",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 9, 3, 5]\n",
      "Solution 2: [0, 9, 7, 3]\n",
      "Solution 3: [4, 9, 7, 0]\n",
      "Solution 4: [6, 9, 4, 0]\n",
      "Solution 5: [6, 9, 0, 2]\n",
      "Solution 6: [2, 9, 0, 5]\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": "049317e5",
   "metadata": {},
   "source": [
    "An alternative for posting the constraint is to use the named parameter *tasks* as follows. The reader can check it."
   ]
  },
  {
   "cell_type": "raw",
   "id": "096294b5",
   "metadata": {
    "raw_mimetype": "text/x-python"
   },
   "source": [
    "satisfy(\n",
    "    NoOverlap(tasks=[(x[i],t[i]) for i in range(4)])\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "78e0e133",
   "metadata": {},
   "source": [
    "## Case 2: NoOverlap with  Variable Lengths"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "711a10d8",
   "metadata": {},
   "source": [
    "The second case if about the one dimensional form with lengths given by variables."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "90650fff",
   "metadata": {},
   "source": [
    "The arguments given to *origins* and *lengths* when calling the function *NoOverlap()* are expected to be lists of the same length; *origins* and *lengths* must be given a list of variables. "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e6b09308",
   "metadata": {},
   "source": [
    "To start, we remove the last posted constraint by calling the function *unpost()*. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "c0d54968",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e02ad8c7",
   "metadata": {},
   "source": [
    "We control that there are no more constraints."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "786d79ef",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[]\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6c1e5927",
   "metadata": {},
   "source": [
    "In addition to the array $x$, we introduce an array $y$ of 4 variables, each one with {3,4,5} as domain; the variables of $x$ will represent the durations of the 4 tasks. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "055d21fc",
   "metadata": {},
   "outputs": [],
   "source": [
    "y = VarArray(size=4, dom=range(3,6))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8e109323",
   "metadata": {},
   "source": [
    "We post a single constraint *NoOverlap* from $x$ and $y$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "8cbfc551",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    NoOverlap(origins=x, lengths=y)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ad97d9ac",
   "metadata": {},
   "source": [
    "We can call the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "90c9f829",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Task 0 starts at 0 and lasts 3 unit(s) of time\n",
      "Task 1 starts at 3 and lasts 3 unit(s) of time\n",
      "Task 2 starts at 6 and lasts 3 unit(s) of time\n",
      "Task 3 starts at 9 and lasts 3 unit(s) of time\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    for i in range(4):\n",
    "        print(f\"Task {i} starts at {value(x[i])} and lasts {value(y[i])} unit(s) of time\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "056e9552",
   "metadata": {},
   "source": [
    "We can enumerate the 20 first solutions."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "61e9adcf",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 3, 6, 9] [3, 3, 3, 3]\n",
      "Solution 2: [0, 3, 6, 9] [3, 3, 3, 4]\n",
      "Solution 3: [0, 3, 6, 9] [3, 3, 3, 5]\n",
      "Solution 4: [0, 3, 9, 6] [3, 3, 3, 3]\n",
      "Solution 5: [0, 3, 9, 6] [3, 3, 4, 3]\n",
      "Solution 6: [0, 3, 9, 6] [3, 3, 5, 3]\n",
      "Solution 7: [0, 9, 3, 6] [3, 3, 3, 3]\n",
      "Solution 8: [0, 9, 3, 6] [3, 4, 3, 3]\n",
      "Solution 9: [0, 9, 3, 6] [3, 5, 3, 3]\n",
      "Solution 10: [0, 9, 6, 3] [3, 5, 3, 3]\n",
      "Solution 11: [0, 9, 6, 3] [3, 3, 3, 3]\n",
      "Solution 12: [0, 9, 6, 3] [3, 4, 3, 3]\n",
      "Solution 13: [0, 6, 9, 3] [3, 3, 3, 3]\n",
      "Solution 14: [0, 6, 9, 3] [3, 3, 4, 3]\n",
      "Solution 15: [0, 6, 9, 3] [3, 3, 5, 3]\n",
      "Solution 16: [0, 6, 3, 9] [3, 3, 3, 3]\n",
      "Solution 17: [0, 6, 3, 9] [3, 3, 3, 4]\n",
      "Solution 18: [0, 6, 3, 9] [3, 3, 3, 5]\n",
      "Solution 19: [6, 0, 3, 9] [3, 3, 3, 5]\n",
      "Solution 20: [6, 0, 3, 9] [3, 3, 3, 3]\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=20) is SAT:\n",
    "    for i in range(n_solutions()):\n",
    "        print(f\"Solution {i+1}: {values(x, sol=i)} {values(y, sol=i)}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "295145a2",
   "metadata": {},
   "source": [
    "## Case 3: Multi-dimensional NoOverlap with  Fixed Lengths"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ac6acbb1",
   "metadata": {},
   "source": [
    "The third case if about the two-dimensional form with lengths given by constants (integers)."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4f5111ad",
   "metadata": {},
   "source": [
    "The arguments given to *origins* and *lengths* when calling the function *NoOverlap()* are expected to be two-dimensional lists of the same length; *origins* and *lengths* must be given a list of pairs (i.e., lists or tuples of length 2) of variables. "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8c886aac",
   "metadata": {},
   "source": [
    "First of all, we need to remove everything that has been introduced so far."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "fa31ea28",
   "metadata": {},
   "outputs": [],
   "source": [
    "clear()  # to clear previously posted variables and constraints"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d5822f27",
   "metadata": {},
   "source": [
    "We introduce a two-dimensional array $t$ of $4 \\times 2$ variables, each one with {0,1,2,3,4,5} as domain. For each task of index $i$, $t[i][0]$ and $t[i][1]$ can represent the origin (starting place) along two axes (of indexes 0 and 1). "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "46096a2c",
   "metadata": {},
   "outputs": [],
   "source": [
    "t = VarArray(size=[4,2], dom=range(5))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "94d44fdf",
   "metadata": {},
   "source": [
    "We can display the structure of the array $t$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "3b40bbf1",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[\n",
      "  [t[0][0], t[0][1]]\n",
      "  [t[1][0], t[1][1]]\n",
      "  [t[2][0], t[2][1]]\n",
      "  [t[3][0], t[3][1]]\n",
      "]\n"
     ]
    }
   ],
   "source": [
    "print(t)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f4ff1a32",
   "metadata": {},
   "source": [
    "We introduce a two-dimensional array $d$ of $4 \\times 2$ integers."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "d4514807",
   "metadata": {},
   "outputs": [],
   "source": [
    "d = [[5,4], [2,3], [3,2], [3,4]] "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9c770543",
   "metadata": {},
   "source": [
    "We simply post a single two-dimensional constraint *NoOverlap* from $t$ and $d$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "id": "9a80ee10",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    NoOverlap(origins=t, lengths=d)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4c3bb904",
   "metadata": {},
   "source": [
    "We can run the solver. The interested reader can check that there is no overlapping between the boxes (rectangles)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "id": "f518979a",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[\n",
      "  [3, 4]\n",
      "  [0, 0]\n",
      "  [0, 3]\n",
      "  [3, 0]\n",
      "]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(values(t))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "21ef9137",
   "metadata": {},
   "source": [
    "One can compute the number of solutions (supports) for that constraint."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "id": "08bd44e8",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "1007\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    print(n_solutions())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "54458223",
   "metadata": {},
   "source": [
    "## Case 4: Multi-dimensional NoOverlap with  Variable Lengths"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1775da9f",
   "metadata": {},
   "source": [
    "The fourth case if about the two-dimensional form with lengths given by variables."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c5a596e2",
   "metadata": {},
   "source": [
    "To start, we remove the last posted constraint by calling the function *unpost()*. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "id": "d961d4ed",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7dc38556",
   "metadata": {},
   "source": [
    "In addition to the array $t$, we introduce an array $y$ of $4 \\times 2$ variables, each one with {3,4,5} as domain; the variables of $y$ will represent the durations over the two dimensions of the 4 tasks. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "id": "ce4dc555",
   "metadata": {},
   "outputs": [],
   "source": [
    "y = VarArray(size=[4,2], dom=range(3,6))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "334647bb",
   "metadata": {},
   "source": [
    "We post the constraint:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "id": "5aaa8441",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    NoOverlap(origins=t, lengths=y)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ae6e3b3f",
   "metadata": {},
   "source": [
    "We display the first found solution (support):"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "id": "dedb476f",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[\n",
      "  [0, 0]\n",
      "  [0, 3]\n",
      "  [3, 0]\n",
      "  [3, 3]\n",
      "] [\n",
      "  [3, 3]\n",
      "  [3, 3]\n",
      "  [3, 3]\n",
      "  [3, 3]\n",
      "]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(values(t), values(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
}