{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "ead7f8c4",
   "metadata": {},
   "source": [
    "# Constraint *Precedence*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "de7b3fdc",
   "metadata": {},
   "source": [
    "The constraint *Precedence* ensures that if a variable $x$ of a specified list of variables is assigned the $i+1th$ value of a specified list $V$ of values, then another variable that precedes $x$ in the list of variables, is assigned the $ith$ value of $V$.\n",
    "In general, this constraint is useful for breaking value symmetries."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ad6fceed",
   "metadata": {},
   "source": [
    "Below, we illustrate two representative use cases of the constraint *Precedence*."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "386a2267",
   "metadata": {},
   "source": [
    "## Case 1: *Precedence* while Specifying Values"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "148939a0",
   "metadata": {},
   "source": [
    "In PyCSP$^3$, we must call the function *Precedence()* that allows us to pass the variables either in sequence (individually) or under the form of a list. \n",
    "A named parameter *values* allows to specify the values involved in the constraint.\n",
    "\n",
    "It is also possible to use an optional named parameter *covered*: when *True*, each value of the specified list must be assigned by at least one variable in the scope of the constraint (by default, the value if *False*)."
   ]
  },
  {
   "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}  as domain."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "1c85cdb9",
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=4, dom={0, 1, 2})"
   ]
  },
  {
   "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 1 2\n"
     ]
    }
   ],
   "source": [
    "print(\"Array of variable x: \", x)\n",
    "print(\"Domain of any variable: \", x[0].dom)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2f52f0ae",
   "metadata": {},
   "source": [
    "First, we simply post a single constraint *Precedence* involving the values 0 and 1. This means that whenever 1 is assigned by a variable of $x$, it is preceeded by 0."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "c71d5d09",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "     Precedence(x, values=[0,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 compute all solutions (supports) by setting the parameter *sols* to the constant *ALL*. We can also print the values assigned to the variables in the found solutions; we can call the function *values()* that collects the values assigned to a specified list of variables, while indicating the index of the solution with the parameter *sol*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "eef140e4",
   "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, 1, 2]\n",
      "Solution 5: [0, 0, 2, 2]\n",
      "Solution 6: [0, 0, 2, 0]\n",
      "Solution 7: [0, 0, 1, 0]\n",
      "Solution 8: [0, 0, 1, 1]\n",
      "Solution 9: [0, 0, 2, 1]\n",
      "Solution 10: [0, 1, 2, 1]\n",
      "Solution 11: [0, 2, 2, 1]\n",
      "Solution 12: [0, 2, 0, 1]\n",
      "Solution 13: [0, 2, 1, 1]\n",
      "Solution 14: [0, 1, 1, 1]\n",
      "Solution 15: [0, 1, 0, 1]\n",
      "Solution 16: [0, 1, 0, 0]\n",
      "Solution 17: [0, 1, 0, 2]\n",
      "Solution 18: [0, 1, 1, 2]\n",
      "Solution 19: [0, 1, 2, 2]\n",
      "Solution 20: [0, 1, 2, 0]\n",
      "Solution 21: [0, 1, 1, 0]\n",
      "Solution 22: [0, 2, 1, 0]\n",
      "Solution 23: [0, 2, 0, 0]\n",
      "Solution 24: [0, 2, 2, 0]\n",
      "Solution 25: [0, 2, 2, 2]\n",
      "Solution 26: [0, 2, 0, 2]\n",
      "Solution 27: [0, 2, 1, 2]\n",
      "Solution 28: [2, 0, 1, 2]\n",
      "Solution 29: [2, 0, 0, 2]\n",
      "Solution 30: [2, 0, 2, 2]\n",
      "Solution 31: [2, 2, 2, 2]\n",
      "Solution 32: [2, 2, 0, 2]\n",
      "Solution 33: [2, 2, 0, 0]\n",
      "Solution 34: [2, 2, 0, 1]\n",
      "Solution 35: [2, 2, 2, 0]\n",
      "Solution 36: [2, 0, 2, 0]\n",
      "Solution 37: [2, 0, 2, 1]\n",
      "Solution 38: [2, 0, 0, 1]\n",
      "Solution 39: [2, 0, 1, 1]\n",
      "Solution 40: [2, 0, 1, 0]\n",
      "Solution 41: [2, 0, 0, 0]\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": "149ae95e",
   "metadata": {},
   "source": [
    "Now, let us discard this constraint:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "936027a2",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "39f2752b",
   "metadata": {},
   "source": [
    "Let us check that there are no more constraints:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "0c33a0d7",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[]\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d7a837bf",
   "metadata": {},
   "source": [
    "This time, let us post a constraint *Precedence* while indicating three values:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "3e6d0202",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "     Precedence(x, values=[0,1,2])\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c74c4532",
   "metadata": {},
   "source": [
    "Let us display all solutions: "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "91d8688e",
   "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, 1, 1]\n",
      "Solution 4: [0, 0, 1, 0]\n",
      "Solution 5: [0, 0, 1, 2]\n",
      "Solution 6: [0, 1, 1, 2]\n",
      "Solution 7: [0, 1, 1, 0]\n",
      "Solution 8: [0, 1, 1, 1]\n",
      "Solution 9: [0, 1, 0, 1]\n",
      "Solution 10: [0, 1, 2, 1]\n",
      "Solution 11: [0, 1, 2, 0]\n",
      "Solution 12: [0, 1, 2, 2]\n",
      "Solution 13: [0, 1, 0, 2]\n",
      "Solution 14: [0, 1, 0, 0]\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": "218ed2a9",
   "metadata": {},
   "source": [
    "## Case 2: *Precedence* without Specifying Values"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f5442622",
   "metadata": {},
   "source": [
    "Let us start by discarding the last posted constraint:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "dad0437d",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "45eb64ca",
   "metadata": {},
   "source": [
    "Let us check that there are no more constraints:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "21af2780",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[]\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d4e2e06f",
   "metadata": {},
   "source": [
    "And let us post a constraint *Precedence* without indicating any values.\n",
    "This is equivalent to indicate the ordered list of values that can be collected over the domains of the variables involved in the constraint. Here, it is equivalent to [0,1,2]."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "50aa461c",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "     Precedence(x)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6ad4e483",
   "metadata": {},
   "source": [
    "Let us display all solutions: "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "2242db5e",
   "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, 1, 1]\n",
      "Solution 4: [0, 0, 1, 0]\n",
      "Solution 5: [0, 0, 1, 2]\n",
      "Solution 6: [0, 1, 1, 2]\n",
      "Solution 7: [0, 1, 1, 0]\n",
      "Solution 8: [0, 1, 1, 1]\n",
      "Solution 9: [0, 1, 0, 1]\n",
      "Solution 10: [0, 1, 2, 1]\n",
      "Solution 11: [0, 1, 2, 0]\n",
      "Solution 12: [0, 1, 2, 2]\n",
      "Solution 13: [0, 1, 0, 2]\n",
      "Solution 14: [0, 1, 0, 0]\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": "4807363a",
   "metadata": {},
   "source": [
    "We can observe thet this way of posting the constraint *Precedence* is indeed equivalent to the last previsouly post operation (for Case 1).  "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "eec30137",
   "metadata": {},
   "source": [
    "Since XCSP$^3$ Specifications 3.1, *Precedence* belongs to XCSP$^3$-core."
   ]
  }
 ],
 "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
}