{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Constraint *AllDifferent*"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The constraint *AllDifferent* ensures that the elements (most the time, variables) from a specified list take different values. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Below, we give several illustrations corresponding to representative use cases of the constraint *AllDifferent*. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Case 1: AllDifferent on Variables"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The first, and usual, case is when a list of variables is specified."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To see how this constraint works, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "For our illustration, we introduce an array $x$ of 4 variables, each one with {0,1,2,3} as domain. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=4, dom=range(4))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can display (the structure of) the array as well as the domains of the four variables."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Array of variable x:  [x[0], x[1], x[2], x[3]]\n",
      "Domain of x[0]: 0..3\n",
      "Domain of x[1]: 0..3\n",
      "Domain of x[2]: 0..3\n",
      "Domain of x[3]: 0..3\n"
     ]
    }
   ],
   "source": [
    "print(\"Array of variable x: \",x)\n",
    "for i in range(4):\n",
    "    print(f\"Domain of {x[i]}: {x[i].dom}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We simply post a single constraint *AllDifferent* on the variables of $x$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    AllDifferent(x)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "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,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 1, 2, 3]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If ever we want to count the number of solutions, we can use the named parameter *sols*. Because here the number of variables (4) is equal to the number of values (4), the number of solutions is exactly the number of permutations (4!=24). Note how the named parameter *sol* of *values()* is used to indicate the index of a solution."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [0, 1, 2, 3]\n",
      "Solution 2: [0, 1, 3, 2]\n",
      "Solution 3: [0, 3, 1, 2]\n",
      "Solution 4: [0, 3, 2, 1]\n",
      "Solution 5: [0, 2, 1, 3]\n",
      "Solution 6: [0, 2, 3, 1]\n",
      "Solution 7: [1, 2, 3, 0]\n",
      "Solution 8: [1, 2, 0, 3]\n",
      "Solution 9: [3, 2, 1, 0]\n",
      "Solution 10: [3, 2, 0, 1]\n",
      "Solution 11: [3, 1, 0, 2]\n",
      "Solution 12: [2, 1, 0, 3]\n",
      "Solution 13: [2, 3, 0, 1]\n",
      "Solution 14: [1, 3, 0, 2]\n",
      "Solution 15: [1, 3, 2, 0]\n",
      "Solution 16: [1, 0, 2, 3]\n",
      "Solution 17: [1, 0, 3, 2]\n",
      "Solution 18: [2, 0, 3, 1]\n",
      "Solution 19: [2, 1, 3, 0]\n",
      "Solution 20: [3, 1, 2, 0]\n",
      "Solution 21: [2, 3, 1, 0]\n",
      "Solution 22: [2, 0, 1, 3]\n",
      "Solution 23: [3, 0, 1, 2]\n",
      "Solution 24: [3, 0, 2, 1]\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",
   "metadata": {},
   "source": [
    "Although this is not the most efficient way of doing that, an alternative is to iteratively add a constraint that forbids the last found solution and to call *solve()*. This way, after each solution, a new instance is generated and the solver is loaded (in the future, we plan to be able to let the solver alive). Hence, we can enumerate all solutions (supports) of the constraint as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution 1: [2, 1, 0, 3]\n",
      "Solution 2: [3, 1, 0, 2]\n",
      "Solution 3: [1, 3, 0, 2]\n",
      "Solution 4: [1, 2, 0, 3]\n",
      "Solution 5: [2, 3, 0, 1]\n",
      "Solution 6: [3, 2, 0, 1]\n",
      "Solution 7: [0, 3, 2, 1]\n",
      "Solution 8: [0, 2, 3, 1]\n",
      "Solution 9: [0, 2, 1, 3]\n",
      "Solution 10: [0, 3, 1, 2]\n",
      "Solution 11: [0, 1, 3, 2]\n",
      "Solution 12: [0, 1, 2, 3]\n",
      "Solution 13: [3, 1, 2, 0]\n",
      "Solution 14: [2, 1, 3, 0]\n",
      "Solution 15: [3, 2, 1, 0]\n",
      "Solution 16: [2, 3, 1, 0]\n",
      "Solution 17: [1, 2, 3, 0]\n",
      "Solution 18: [1, 3, 2, 0]\n",
      "Solution 19: [2, 0, 1, 3]\n",
      "Solution 20: [3, 0, 1, 2]\n",
      "Solution 21: [1, 0, 2, 3]\n",
      "Solution 22: [1, 0, 3, 2]\n",
      "Solution 23: [3, 0, 2, 1]\n",
      "Solution 24: [2, 0, 3, 1]\n"
     ]
    }
   ],
   "source": [
    "cnt = 0\n",
    "while solve(solver=CHOCO) is SAT:\n",
    "    cnt += 1\n",
    "    print(f\"Solution {cnt}: {values(x)}\")\n",
    "    satisfy(\n",
    "        x != values(x)\n",
    "    )"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Suppose now that we arbitrarily remove the value 3 from the domain of the two last variables. We can check that no more solution exists because the result is now UNSAT; one can observe in the previous enumeration of solutions that it is not possible to have 3 assigned to both $x[2]$ and $x[3]$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Result:  UNSAT\n"
     ]
    }
   ],
   "source": [
    "satisfy(\n",
    "    x[2] != 3,\n",
    "    x[3] != 3\n",
    ")\n",
    "\n",
    "print(\"Result: \", solve())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Case 2: AllDifferent on Expressions"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The second case is when a list of expressions (not single variables) is specified."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "First of all, we need to remove everything that has been introduced so far by calling the function *clear()*. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [],
   "source": [
    "clear()  # to clear previously posted variables and constraints"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "As earlier, we introduce an array $x$ of 4 variables, each one with $\\{0,1,2,3\\}$ as domain. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [],
   "source": [
    "x = VarArray(size=4, dom=range(4))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Then, we post a single constraint *AllDifferent* on some expressions linking variables of $x$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    AllDifferent(abs(x[1]-x[0]), abs(x[2]-x[1]), abs(x[3]-x[2]), abs(x[0]-x[3]))\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can display the internal representation of the constraint that we have just posted; note that dist(a,b) is equivalent to abs(a-b)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "allDifferent(list:[dist(x[1],x[0]), dist(x[2],x[1]), dist(x[3],x[2]), dist(x[0],x[3])])\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can run the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solution:  [0, 0, 1, 3]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\"Solution: \", values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On can check that the four expressions are different."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Case 3: AllDifferent with Exceptions"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "A variant, sometimes called *AllDifferentExcept* in the literature, enforces variables to take distinct values, except those that are assigned to some specified values (often, the single value 0). We use a named parameter called *excepting* for indicating the value(s) that must be ignored."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To start, we remove the last posted constraint by calling the function *unpost()*. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We control that there are no more constraints."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[]\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Then, we post a single constraint AllDifferent on the variables of $x$, while indicating that the value 0 must be ignored."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    AllDifferent(x, excepting=0)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "When solutions are enumerated, one can see that the special value 0 is ignored. Here, we enumerate the 20 first solutions."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "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, 2, 0]\n",
      "Solution 8: [0, 0, 1, 0]\n",
      "Solution 9: [0, 0, 3, 0]\n",
      "Solution 10: [0, 0, 3, 1]\n",
      "Solution 11: [0, 0, 2, 1]\n",
      "Solution 12: [0, 0, 1, 2]\n",
      "Solution 13: [0, 0, 3, 2]\n",
      "Solution 14: [0, 1, 3, 2]\n",
      "Solution 15: [0, 1, 0, 2]\n",
      "Solution 16: [0, 3, 0, 2]\n",
      "Solution 17: [0, 3, 1, 2]\n",
      "Solution 18: [0, 3, 1, 0]\n",
      "Solution 19: [0, 3, 0, 0]\n",
      "Solution 20: [0, 3, 2, 0]\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=20) is SAT:\n",
    "    for i in range(20):\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": 2
}