{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "4ad64caa",
   "metadata": {
    "tags": [
     "CSP",
     "academic",
     "medium",
     "Intension",
     "ElementMatrix",
     "Element",
     "AllDifferentMatrix"
    ]
   },
   "source": [
    "# Problem *Quasigroup Existence*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "915c09bd",
   "metadata": {},
   "source": [
    " From [CSPLib (Problem 03)](https://www.csplib.org/Problems/prob003/): A quasigroup of order n is a $n \\times n$ multiplication table in which each element occurs once in every row and column (i.e., is a Latin square), while satisfying some specific properties. Hence, the result a*b of applying the multiplication operator * on a (left operand) and b (right operand) is given by the value in the table at row a and column b. Classical variants of quasigroup existence correspond to taking into account the following properties:\n",
    "- QG3: quasigroups for which $(a*b)*(b*a)=a$\n",
    "- QG4: quasigroups for which $(b*a)*(a*b)=a$\n",
    "- QG5: quasigroups for which $((b*a)*b)*b=a$\n",
    "- QG6: quasigroups for which $(a*b)*b=a*(a*b)$\n",
    "- QG7: quasigroups for which $(b*a)*b=a*(b*a)$\n",
    "\n",
    "For each of these problems, we may additionally demand that the quasigroup is idempotent. That is, $a*a=a$ for every element $a$. This is what we consider below."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bedf4050",
   "metadata": {},
   "source": [
    "To build a CSP (Constraint Satisfaction Problem) model, we need first to import the library PyCSP$^3$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "ca2ce71d",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "53f8ea5f",
   "metadata": {},
   "source": [
    "Then, we need some data. Actually, we just need an integer $n$. For example, the value 5."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "62c078a7",
   "metadata": {},
   "outputs": [],
   "source": [
    "n = 5"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a2ce4bf2",
   "metadata": {},
   "source": [
    "We start our CSP model by introducing an array $x$ of variables."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "a0db3a15",
   "metadata": {},
   "outputs": [],
   "source": [
    "# x[i][j] is the value at row i and column j of the quasi-group\n",
    "x = VarArray(size=[n, n], dom=range(n))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2409d6a8",
   "metadata": {},
   "source": [
    "We can display the structure of the array, as well as the domain of the first variable (note that all variables have the same domain)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "4c672247",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Array x:  [\n",
      "  [x[0][0], x[0][1], x[0][2], x[0][3], x[0][4]]\n",
      "  [x[1][0], x[1][1], x[1][2], x[1][3], x[1][4]]\n",
      "  [x[2][0], x[2][1], x[2][2], x[2][3], x[2][4]]\n",
      "  [x[3][0], x[3][1], x[3][2], x[3][3], x[3][4]]\n",
      "  [x[4][0], x[4][1], x[4][2], x[4][3], x[4][4]]\n",
      "]\n",
      "Domain of any variable:  0..4\n"
     ]
    }
   ],
   "source": [
    "print(\"Array x: \", x)\n",
    "print(\"Domain of any variable: \", x[0][0].dom)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9b7a3ef9",
   "metadata": {},
   "source": [
    "Concerning the constraints, we have to post first a constraint *AllDifferentMatrix* in order to impose a Latin square."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "7645da49",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "   # ensuring a Latin square\n",
    "   AllDifferent(x, matrix=True)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1adc3dca",
   "metadata": {},
   "source": [
    "Then, we post a group of unary constraints *Intension* to enforce idempotence."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "8338c10d",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "   # ensuring idempotence  tag(idempotence)\n",
    "   x[i][i] == i for i in range(n)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1ea42d71",
   "metadata": {},
   "source": [
    "We can display the internal representation of the posted constraints; this way, although a little bit technical, we can see that the arguments of the constraints are correct (note that 'eq' stands for 'equal to')."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "61a52f4e",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "allDifferent(matrix:(x[0][0],x[0][1],x[0][2],x[0][3],x[0][4])(x[1][0],x[1][1],x[1][2],x[1][3],x[1][4])(x[2][0],x[2][1],x[2][2],x[2][3],x[2][4])(x[3][0],x[3][1],x[3][2],x[3][3],x[3][4])(x[4][0],x[4][1],x[4][2],x[4][3],x[4][4]))\n",
      "intension(function:eq(x[0][0],0))\n",
      "intension(function:eq(x[1][1],1))\n",
      "intension(function:eq(x[2][2],2))\n",
      "intension(function:eq(x[3][3],3))\n",
      "intension(function:eq(x[4][4],4))\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a0ea7228",
   "metadata": {},
   "source": [
    "Interestingly, by calling the function *solve()*, we can check that the problem is satisfiable (SAT). We can also display the found solution. Here, we call the function *values()* that collects the values assigned to a specified list of variables."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "1d4cda67",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[\n",
      "  [0, 2, 1, 4, 3]\n",
      "  [3, 1, 4, 0, 2]\n",
      "  [4, 3, 2, 1, 0]\n",
      "  [2, 4, 0, 3, 1]\n",
      "  [1, 0, 3, 2, 4]\n",
      "]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6698d6ff",
   "metadata": {},
   "source": [
    "We can see that until now everything is on the right track."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "38b18995",
   "metadata": {},
   "source": [
    "We now introduce the three representative variants QG4, QG5 and QG7 for wich the existence of a quasigroup is guaranteed for $n =5$."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b784204a",
   "metadata": {},
   "source": [
    "## QG4"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5dfa2029",
   "metadata": {},
   "source": [
    "For the variant QG4, we have to post a group of constraints *ElementMatrix*:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "8a209e67",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    x[x[j][i], x[i][j]] == i for i in range(n) for j in range(n)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0dd64b01",
   "metadata": {},
   "source": [
    "For control, we can display the two last posted constraints:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "ce83b820",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "element(matrix:(x[0][0],x[0][1],x[0][2],x[0][3],x[0][4])(x[1][0],x[1][1],x[1][2],x[1][3],x[1][4])(x[2][0],x[2][1],x[2][2],x[2][3],x[2][4])(x[3][0],x[3][1],x[3][2],x[3][3],x[3][4])(x[4][0],x[4][1],x[4][2],x[4][3],x[4][4]), index:[x[3][4], x[4][3]], condition:(eq,4))\n",
      "element(matrix:(x[0][0],x[0][1],x[0][2],x[0][3],x[0][4])(x[1][0],x[1][1],x[1][2],x[1][3],x[1][4])(x[2][0],x[2][1],x[2][2],x[2][3],x[2][4])(x[3][0],x[3][1],x[3][2],x[3][3],x[3][4])(x[4][0],x[4][1],x[4][2],x[4][3],x[4][4]), index:[x[4][4], x[4][4]], condition:(eq,4))\n"
     ]
    }
   ],
   "source": [
    "print(posted()[-2:])"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "cfd4ba73",
   "metadata": {},
   "source": [
    "An we can run the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "a8bcf6b8",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[\n",
      "  [0, 2, 1, 4, 3]\n",
      "  [3, 1, 4, 0, 2]\n",
      "  [4, 3, 2, 1, 0]\n",
      "  [2, 4, 0, 3, 1]\n",
      "  [1, 0, 3, 2, 4]\n",
      "]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "30553fef",
   "metadata": {},
   "source": [
    "We can compute the number of solutions as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "5d395e44",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Number of solutions:  12\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    print(\"Number of solutions: \", n_solutions())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1b0e3b1c",
   "metadata": {},
   "source": [
    "## QG5"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "faeb0150",
   "metadata": {},
   "source": [
    "For the variant QG5, we have to post a group of complex constraints *Intension*. They will be partly decomposed by introducing auxiliary variables and constraints *Element*, in order to remain in the perimeter of XSCP$^3$-core. "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8bdaa11f",
   "metadata": {},
   "source": [
    "But first, we have to remove all constraints that have been posted at the last call to *satisfy()*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "f78e6e5b",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a10637c7",
   "metadata": {},
   "source": [
    "We can check that these constraints have been discarded."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "3f545842",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "allDifferent(matrix:x[][])\n",
      "instantiation(list:x[0][0] x[1][1] x[2][2] x[3][3] x[4][4], values:[0, 1, 2, 3, 4])\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "63fde999",
   "metadata": {},
   "source": [
    "We post the new group of constraints:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "af3a63a3",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    x[x[x[j,i],j],j] == i for i in range(n) for j in range(n)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2e6707dd",
   "metadata": {},
   "source": [
    "We run the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "a1f808d2",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[\n",
      "  [0, 2, 1, 4, 3]\n",
      "  [3, 1, 4, 0, 2]\n",
      "  [4, 3, 2, 1, 0]\n",
      "  [2, 4, 0, 3, 1]\n",
      "  [1, 0, 3, 2, 4]\n",
      "]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9ec97093",
   "metadata": {},
   "source": [
    "And we compute the number of solutions."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "d9076f26",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Number of solutions:  6\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    print(\"Number of solutions: \", n_solutions())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "174fdf06",
   "metadata": {},
   "source": [
    "## QG7"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4f4c03cc",
   "metadata": {},
   "source": [
    "For the variant QG7, we have to post a group of complex constraints *Intension*. They will be decomposed by introducing auxiliary variables and constraints *Element*, in order to remain in the perimeter of XSCP$^3$-core."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9d050137",
   "metadata": {},
   "source": [
    "But first, we have to remove all constraints that have been posted at the last call to *satisfy()*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "3a651f8e",
   "metadata": {},
   "outputs": [],
   "source": [
    "unpost()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "72069413",
   "metadata": {},
   "source": [
    "We post the new group of constraints:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "id": "d8676a96",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    x[x[j][i],j] == x[i,x[j][i]] for i in range(n) for j in range(n)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "158e9099",
   "metadata": {},
   "source": [
    "We run the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "id": "3d46c59f",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[\n",
      "  [0, 2, 1, 4, 3]\n",
      "  [3, 1, 4, 0, 2]\n",
      "  [4, 3, 2, 1, 0]\n",
      "  [2, 4, 0, 3, 1]\n",
      "  [1, 0, 3, 2, 4]\n",
      "]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(values(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "089ea099",
   "metadata": {},
   "source": [
    "And we compute the number of solutions."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "id": "9dc1b335",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Number of solutions:  12\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    print(\"Number of solutions: \", n_solutions())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "899962b9",
   "metadata": {},
   "source": [
    "Finally, we give below the model in one piece. Here the data is expected to be given by the user (in a command line). The user must also indicate the variant (with the option -variant on the command line)."
   ]
  },
  {
   "cell_type": "raw",
   "id": "e8278e33",
   "metadata": {
    "raw_mimetype": "text/x-python"
   },
   "source": [
    "from pycsp3 import *\n",
    "\n",
    "n = data or 8\n",
    "\n",
    "# x[i][j] is the value at row i and column j of the quasi-group\n",
    "x = VarArray(size=[n, n], dom=range(n))\n",
    "\n",
    "satisfy(\n",
    "    # ensuring a Latin square\n",
    "    AllDifferent(x, matrix=True),\n",
    "\n",
    "    # ensuring idempotence  tag(idempotence)\n",
    "    [x[i][i] == i for i in range(n)]\n",
    ")\n",
    "\n",
    "\n",
    "if variant(\"v3\"):\n",
    "    satisfy(\n",
    "        x[x[i][j], x[j][i]] == i for i in range(n) for j in range(n)\n",
    "    )\n",
    "elif variant(\"v4\"):\n",
    "    satisfy(\n",
    "        x[x[j][i], x[i][j]] == i for i in range(n) for j in range(n)\n",
    "    )\n",
    "elif variant(\"v5\"):\n",
    "    satisfy(\n",
    "        x[x[x[j][i], j], j] == i for i in range(n) for j in range(n)\n",
    "    )\n",
    "elif variant(\"v6\"):\n",
    "    satisfy(\n",
    "        x[x[i][j], j] == x[i, x[i][j]] for i in range(n) for j in range(n)\n",
    "    )\n",
    "elif variant(\"v7\"):\n",
    "    satisfy(\n",
    "        x[x[j][i], j] == x[i, x[j][i]] for i in range(n) for j in range(n)\n",
    "    )"
   ]
  }
 ],
 "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
}