{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "d15c1ba8",
   "metadata": {},
   "source": [
    "# Constraint *LexIncreasing*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "250c7191",
   "metadata": {},
   "source": [
    "The constraint *Increasing* can be naturally lifted to lists, by considering the so-called *lexicographic order*: it is then called *LexIncreasing* and ensures that the tuple formed by the values assigned to the variables of a first list is lexicographically less than (or equal to) the tuple formed by the values assigned to the variables of a second  list. "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fc52b0ab",
   "metadata": {},
   "source": [
    "Below, we give several illustrations corresponding to representative use cases of the constraint *LexIncreasing*."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d3ffe5ad",
   "metadata": {},
   "source": [
    "## Case 1: *LexIncreasing* on Two Lists"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d0fed56e",
   "metadata": {},
   "source": [
    "To see how this constraint works, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "4a115adc",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2d9eb8f7",
   "metadata": {},
   "source": [
    "For our illustration, we introduce two arrays $x$ and $y$ of 3 variables, each variable having {0,1}  as domain."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "81599d43",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=3, dom=range(2))\n",
    "y = VarArray(size=3, dom=range(2))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b9f81868",
   "metadata": {},
   "source": [
    "We can display (the structure of) the arrays as well as the domain of a variable."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "8854b6b9",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Array of variable x:  [x[0], x[1], x[2]]\n",
      "Array of variable y:  [y[0], y[1], y[2]]\n",
      "Domain of any variable:  0 1\n"
     ]
    }
   ],
   "source": [
    "print(\"Array of variable x: \", x)\n",
    "print(\"Array of variable y: \", y)\n",
    "print(\"Domain of any variable: \", x[0].dom)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d3d3cddc",
   "metadata": {},
   "source": [
    "We simply post a single constraint *LexIncreasing* that imposes $x \\leq_{lex} y$: "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "575f59e3",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    LexIncreasing(x,y)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "39db6a98",
   "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": "5f87ac19",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Values of x:  [0, 0, 0]\n",
      "Values of y:  [0, 0, 0]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Values of x: \", values(x))\n",
    "    print(\"Values of y: \", values(y))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a73edf66",
   "metadata": {},
   "source": [
    "Here, we obtain a rather trivial solution. To get all solutions when x is, for example equal to [0, 1, 0], we can write:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "65de62c6",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 1, 0] [0, 1, 0]\n",
      "Solution 2: [0, 1, 0] [0, 1, 1]\n",
      "Solution 3: [0, 1, 0] [1, 1, 1]\n",
      "Solution 4: [0, 1, 0] [1, 1, 0]\n",
      "Solution 5: [0, 1, 0] [1, 0, 0]\n",
      "Solution 6: [0, 1, 0] [1, 0, 1]\n"
     ]
    }
   ],
   "source": [
    "satisfy(\n",
    "    x == [0,1,0]\n",
    ")\n",
    "\n",
    "if solve(sols=ALL) 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": "718dced0",
   "metadata": {},
   "source": [
    "### Strict *LexIncreasing*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9583dd53",
   "metadata": {},
   "source": [
    "We now see how to impose a strict ordering."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d9e5dc5f",
   "metadata": {},
   "source": [
    "To start, we remove the posted constraints by calling the function *unpost()* with a parameter set to the constant ALL. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "b4740013",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost(ALL)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5b33e79d",
   "metadata": {},
   "source": [
    "We control that there are no more constraints."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "0b372923",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[]\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b0088844",
   "metadata": {},
   "source": [
    "We post a single constraint *LexIncreasing* that imposes $x <_{lex} y$ (this is a strict ordering):"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "7dc79fbf",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    LexIncreasing(x, y, strict=True)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ed88aa18",
   "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 'lt' stands for 'strictly less than')."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "10f751cf",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "lex(list:[[x[0], x[1], x[2]], [y[0], y[1], y[2]]], operator:lt)\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "33c3de08",
   "metadata": {},
   "source": [
    "We can enumerate the 8 first solutions as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "1e548e90",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 0, 0] [0, 0, 1]\n",
      "Solution 2: [0, 0, 0] [0, 1, 1]\n",
      "Solution 3: [0, 0, 0] [0, 1, 0]\n",
      "Solution 4: [0, 0, 0] [1, 1, 0]\n",
      "Solution 5: [0, 0, 0] [1, 0, 0]\n",
      "Solution 6: [0, 0, 0] [1, 0, 1]\n",
      "Solution 7: [0, 0, 0] [1, 1, 1]\n",
      "Solution 8: [0, 0, 1] [1, 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)} {values(y, sol=i)}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "58f83e54",
   "metadata": {},
   "source": [
    "## Case 2: *LexIncreasing* on $k$ Lists"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b266814a",
   "metadata": {},
   "source": [
    "Actually, we can impose a lexicographic order on a sequence of $k$ lists with $k \\ge 2$. We give an illustration for $k=3$."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9b839e37",
   "metadata": {},
   "source": [
    "We first remove all posted constraints. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "bd6208d0",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost(ALL)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f0b93f41",
   "metadata": {},
   "source": [
    "We introduce a third array $z$ of 3 variables."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "4d1d56fc",
   "metadata": {},
   "outputs": [],
   "source": [
    "z = VarArray(size=3, dom=range(2))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "07dbb740",
   "metadata": {},
   "source": [
    "We post a single constraint *LexIncreasing* that imposes $x <_{lex} y <_{lex} z$: "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "44f44888",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    LexIncreasing(x, y, z, strict=True)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "58b2d8ec",
   "metadata": {},
   "source": [
    "We dsiplay its internal representation."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "ee3785ed",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "lex(list:[[x[0], x[1], x[2]], [y[0], y[1], y[2]], [z[0], z[1], z[2]]], operator:lt)\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "33cfa627",
   "metadata": {},
   "source": [
    "We enumerate the 8 first solutions:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "94cb3a57",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 0, 0] [0, 0, 1] [0, 1, 0]\n",
      "Solution 2: [0, 0, 0] [0, 0, 1] [0, 1, 1]\n",
      "Solution 3: [0, 0, 0] [0, 0, 1] [1, 1, 1]\n",
      "Solution 4: [0, 0, 0] [0, 0, 1] [1, 1, 0]\n",
      "Solution 5: [0, 0, 0] [0, 0, 1] [1, 0, 0]\n",
      "Solution 6: [0, 0, 0] [0, 0, 1] [1, 0, 1]\n",
      "Solution 7: [0, 0, 0] [0, 1, 1] [1, 0, 1]\n",
      "Solution 8: [0, 0, 0] [0, 1, 0] [1, 0, 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)} {values(y, sol=i)} {values(z, sol=i)}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "69ddae0b",
   "metadata": {},
   "source": [
    "## Case 3: *LexIncreasing* on Matrices"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b10e788e",
   "metadata": {},
   "source": [
    "We are now interested in the matrix variant of *LexIncreasing*. It means that we impose a lexicographic order on the sequence of rows and also on the sequence of columns of a two-dimensional array of variables. "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "550bd20f",
   "metadata": {},
   "source": [
    "We first clear (remove) variables and constraints."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "71f7a432",
   "metadata": {},
   "outputs": [],
   "source": [
    "clear()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f9191d0c",
   "metadata": {},
   "source": [
    "Then, we introduce a two-dimensional array of variables $x$, each variable having {0,1} as domain."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "0d86ed06",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=[3,3], dom={0,1})"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "feeba03d",
   "metadata": {},
   "source": [
    "We can display the structure of the array:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "id": "47f7090d",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Array of variable x:  [\n",
      "  [x[0][0], x[0][1], x[0][2]]\n",
      "  [x[1][0], x[1][1], x[1][2]]\n",
      "  [x[2][0], x[2][1], x[2][2]]\n",
      "]\n"
     ]
    }
   ],
   "source": [
    "print(\"Array of variable x: \", x)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bbed8a94",
   "metadata": {},
   "source": [
    "We post a single matrix constraint *LexIncreasing* on $x$ that imposes:\n",
    "- $x[0] \\leq_{lex} x[1] \\leq_{lex} x[2]$ \n",
    "- $x[:,0] \\leq_{lex} x[:,1] \\leq_{lex} x[:,2]$ \n",
    "\n",
    "where $x[:j]$ denotes the jth column of $x$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "id": "ffc21629",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    LexIncreasing(x, matrix=True)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2c8b7e08",
   "metadata": {},
   "source": [
    "We enumerate the 3 first solutions:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "id": "457795e6",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [\n",
      "  [0, 0, 0]\n",
      "  [0, 0, 0]\n",
      "  [0, 0, 0]\n",
      "]\n",
      "Solution 2: [\n",
      "  [0, 0, 0]\n",
      "  [0, 0, 0]\n",
      "  [0, 0, 1]\n",
      "]\n",
      "Solution 3: [\n",
      "  [0, 0, 0]\n",
      "  [0, 0, 0]\n",
      "  [0, 1, 1]\n",
      "]\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=3) is SAT:\n",
    "    for i in range(n_solutions()):\n",
    "        print(f\"Solution {i+1}: {values(x, sol=i)}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8adb24fc",
   "metadata": {},
   "source": [
    "We can also impose a strict ordering:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "id": "32b84ec6",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [\n",
      "  [0, 0, 0]\n",
      "  [0, 0, 1]\n",
      "  [0, 1, 0]\n",
      "]\n",
      "Solution 2: [\n",
      "  [0, 0, 0]\n",
      "  [0, 0, 1]\n",
      "  [0, 1, 1]\n",
      "]\n",
      "Solution 3: [\n",
      "  [0, 0, 0]\n",
      "  [0, 1, 1]\n",
      "  [1, 0, 1]\n",
      "]\n"
     ]
    }
   ],
   "source": [
    "unpost()\n",
    "\n",
    "satisfy(\n",
    "    LexIncreasing(x, matrix=True, strict=True)\n",
    ");\n",
    "\n",
    "if solve(sols=3) 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
}