{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "8dc53b31",
   "metadata": {},
   "source": [
    "# Constraint *Increasing*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "02f81e83",
   "metadata": {},
   "source": [
    "The constraint *Increasing* ensures that the values assigned to the variables of a specified list are in increasing order."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1b47763e",
   "metadata": {},
   "source": [
    "Below, we give several illustrations corresponding to representative use cases of the constraint *Increasing*."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bdb4f5f6",
   "metadata": {},
   "source": [
    "## Case 1: *Increasing* on Variables"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0b7eecab",
   "metadata": {},
   "source": [
    "We consider the case where we have just a list of variables. If $r$ is the size of a list $x$ of variables, we have:\n",
    "> $x[i] \\leq x[i+1], \\forall i \\in 0..r-1$"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0331caa8",
   "metadata": {},
   "source": [
    "To see how this constraint works, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "de089fab",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "  \u001b[93mWarning: \u001b[0mUnknown option: -f\n",
      "\n"
     ]
    }
   ],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "340e1f1e",
   "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": "d6b18970",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=4, dom=range(4))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0c088b58",
   "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": "774866bc",
   "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": "94338770",
   "metadata": {},
   "source": [
    "We simply post a single constraint *Increasing* on $x$ imposing that assigned values must be in increasing order."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "9770179d",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Increasing(x)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "dba115ef",
   "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 to a specified list of variables."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "0c1df14d",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Values of x:  [0, 0, 0, 0]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Values of x: \", values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b81e43e4",
   "metadata": {},
   "source": [
    "We can enumerate the 8 first solutions as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "8bf880e1",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 0, 0, 0]\n",
      "Solution 2: [0, 0, 0, 1]\n",
      "Solution 3: [0, 0, 0, 2]\n",
      "Solution 4: [0, 0, 0, 3]\n",
      "Solution 5: [0, 0, 1, 3]\n",
      "Solution 6: [0, 0, 2, 3]\n",
      "Solution 7: [0, 0, 3, 3]\n",
      "Solution 8: [0, 0, 1, 1]\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=8) is SAT:\n",
    "    for i in range(n_solutions()):\n",
    "        print(f\"Solution {i+1}: {values(x, sol=i)}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0d58fc6b",
   "metadata": {},
   "source": [
    "### Strict *Increasing*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0f37c0e9",
   "metadata": {},
   "source": [
    "We now see how to impose a strict ordering."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6344b180",
   "metadata": {},
   "source": [
    "To start, we remove the last posted constraint by calling the function *unpost()*. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "ce25b9d1",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b244ab7d",
   "metadata": {},
   "source": [
    "We control that there are no more constraints."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "751dc647",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[]\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "dd1c1e21",
   "metadata": {},
   "source": [
    "We post a single constraint *Increasing* with a strict ordering imposed on $x$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "71f81c12",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Increasing(x, strict=True)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "53fd9590",
   "metadata": {},
   "source": [
    "We call the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "20bc8764",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Values of x:  [0, 1, 2, 3]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Values of x: \", values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "16e1af7a",
   "metadata": {},
   "source": [
    "## Case 2: *Increasing* with Lengths"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "32e58386",
   "metadata": {},
   "source": [
    "Now, we consider the case where some lengths (durations) are associated with the variables of the list (except for the last one). If $r$ is the size of a list $x$ of variables, and $d$ a list of $r-1$ integers, we have:\n",
    "> $x[i] + d[i] \\leq x[i+1], \\forall i \\in 0..r-1$"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e959f9b7",
   "metadata": {},
   "source": [
    "To start, we remove the last posted constraint by calling the function *unpost()*. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "de8fa121",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "481396c7",
   "metadata": {},
   "source": [
    "We post a single constraint *Increasing* with some arbitrary lengths associated with the three first variables"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "59785643",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    Increasing(x, lengths=[1,0,1])\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "22bd1406",
   "metadata": {},
   "source": [
    "We call the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "b8fbad5e",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Values of x:  [0, 1, 1, 2]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Values of x: \", values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7966d13f",
   "metadata": {},
   "source": [
    "We can enumerate all solutions:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "0abf33f0",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 1, 1, 2]\n",
      "Solution 2: [0, 1, 1, 3]\n",
      "Solution 3: [0, 1, 2, 3]\n",
      "Solution 4: [0, 2, 2, 3]\n",
      "Solution 5: [1, 2, 2, 3]\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
}