{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "6e40ec58",
   "metadata": {
    "tags": [
     "CSP",
     "easy",
     "AllDifferent",
     "Sum",
     "Intension",
     "academic"
    ]
   },
   "source": [
    "# Problem *Crypto Puzzle*"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "51f8ac5e",
   "metadata": {},
   "source": [
    "In crypto-arithmetic problems, digits (values between 0 and 9) are represented by letters. Different letters stand for different digits, and different occurrences of the same letter denote the same digit.\n",
    "The problem is then represented as an arithmetic operation between words. The task is to find out which letter stands for which digit, so that the result of the given arithmetic operation is true.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b6ff05f4",
   "metadata": {},
   "source": [
    "Here are some examples of crypto puzzles:\n",
    "\n",
    "       no           cross         donald\n",
    "    +  no        +  roads       + gerald\n",
    "    = yes        = danger       = robert"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4a6a8872",
   "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": "ed4f0ed8",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pycsp3 import *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d54e583e",
   "metadata": {},
   "source": [
    "Then, we need some data. Here, we choose a specific crypto puzzle (donald+gerald=robert). Note that the  function *alphabet\\_positions()* returns a tuple composed of the positions in the Latin alphabet of all letters of a string passed as a parameter."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "7d344173",
   "metadata": {},
   "outputs": [],
   "source": [
    "words = [\"donald\", \"gerald\", \"robert\"]\n",
    "word1, word2, word3 = words\n",
    "letters = set(alphabet_positions(word1 + word2 + word3))\n",
    "n = len(word1)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0662b84f",
   "metadata": {},
   "source": [
    "We can check the value of these variables. In letters, we have the indexes of all involved characters in the three words."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "5f8daaa4",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Letters:  {0, 1, 3, 4, 6, 11, 13, 14, 17, 19}\n",
      "n:  6\n"
     ]
    }
   ],
   "source": [
    "print(\"Letters: \", letters)\n",
    "print(\"n: \", n)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f42a22ad",
   "metadata": {},
   "source": [
    "We assume that the two first words have the same length, while the third one may be longer by one letter.  "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "d0f8f9f8",
   "metadata": {},
   "outputs": [],
   "source": [
    "assert len(word2) == n and len(word3) in {n, n + 1}"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e2440db8",
   "metadata": {},
   "source": [
    "We start our CSP model with an array $x$ of variables; for simplicity, the array contains 26 squares (for the 26 possible letters) but only some of them are considered as relevant: those corresponding to an involved letter index. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "fea8d339",
   "metadata": {},
   "outputs": [],
   "source": [
    "# x[i] is the value assigned to the ith letter (if present) of the alphabet\n",
    "x = VarArray(size=26, dom=lambda i: range(10) if i in letters else None)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d949e622",
   "metadata": {},
   "source": [
    "By printing the content of $x$, we can clearly see which variables are created. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "77ae0812",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[x[0], x[1], None, x[3], x[4], None, x[6], None, None, None, None, x[11], None, x[13], x[14], None, None, x[17], None, x[19], None, None, None, None, None, None]\n"
     ]
    }
   ],
   "source": [
    "print(x)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "27f7693c",
   "metadata": {},
   "source": [
    "The domain of each variable is $\\{0,1,\\dots,9\\}$. For example:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "4aec1ffc",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "0..9\n"
     ]
    }
   ],
   "source": [
    "print(x[4].dom)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5fdd2f20",
   "metadata": {},
   "source": [
    "For simplicity, we build three auxiliary lists of variables corresponding to the letters of the three words. Note however that we do not build new variables in our model, as we simply copy the references of some of them."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "bf659680",
   "metadata": {},
   "outputs": [],
   "source": [
    "# auxiliary lists of variables associated with the three words\n",
    "x1, x2, x3 = [[x[i] for i in alphabet_positions(word)] for word in words]"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "eace5bb4",
   "metadata": {},
   "source": [
    "This gives:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "5c14cb6c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "x1: [x[3], x[14], x[13], x[0], x[11], x[3]] \n",
      "x2: [x[6], x[4], x[17], x[0], x[11], x[3]] \n",
      "x3: [x[17], x[14], x[1], x[4], x[17], x[19]]\n"
     ]
    }
   ],
   "source": [
    "print(f\"x1: {x1} \\nx2: {x2} \\nx3: {x3}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d56be225",
   "metadata": {},
   "source": [
    "Concerning the constraints, we first post a constraint *AllDifferent*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "ce723407",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    # all letters must be assigned different values\n",
    "    AllDifferent(x)\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7869f8e6",
   "metadata": {},
   "source": [
    "Then, we want to avoid to have the most significant letters assigned to 0. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "d5fc1d18",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    x1[0] != 0, \n",
    "    x2[0] != 0, \n",
    "    x3[0] != 0\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f0e0f5f7",
   "metadata": {},
   "source": [
    "If we are curious, we can print the intern representation of the constraints that have been posted. Athough a little bit technical, one can see that we have one constraint *AllDifferent* and three constraints *Intension* (note that 'ne' stands for 'not equal to')."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "2b04f74f",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "allDifferent(list:[x[0], x[1], x[3], x[4], x[6], x[11], x[13], x[14], x[17], x[19]])\n",
      "intension(function:ne(x[3],0))\n",
      "intension(function:ne(x[6],0))\n",
      "intension(function:ne(x[17],0))\n"
     ]
    }
   ],
   "source": [
    "print(posted())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e2cc6ed3",
   "metadata": {},
   "source": [
    "Interestingly, by calling the function *solve()*, we can check that the problem is satisfiable (SAT). We can also display the values of each word. Here, we call the function *values()* that collects the values assigned to a specified list of variables."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "73717a37",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "  [2, 7, 6, 0, 5, 2]\n",
      "+ [4, 3, 8, 0, 5, 2]\n",
      "= [8, 7, 1, 3, 8, 9]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\" \", values(x1))\n",
    "    print(\"+\", values(x2))\n",
    "    print(\"=\", values(x3))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7ae192a4",
   "metadata": {},
   "source": [
    "Of course, the sum is not valid. The missing constraint can be written by calling the function *Sum()*:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "4b8bbee2",
   "metadata": {},
   "outputs": [],
   "source": [
    "satisfy(\n",
    "    # ensuring the crypto-arithmetic sum\n",
    "    Sum((x1[-i-1] + x2[-i-1]) * 10 ** i for i in range(n))\n",
    "      == Sum(x3[-i-1] * 10 ** i for i in range(len(x3)))\n",
    ");"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "cccecb4e",
   "metadata": {},
   "source": [
    "Because this expression is rather complex, one may want to control it. This is made easier by developping the last posted constraint (i.e., printing its internal representation). One can see that it corresponds to a weighted sum under the condition \"= 0\" (note that 'eq' stands for 'equal to'). By calling *posted(-1)* we can get the constraint(s) that have been posted at the last call to *satisfy()*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "b1d02a14",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "sum(list:[add(x[3],x[3]), add(x[11],x[11]), add(x[0],x[0]), add(x[13],x[17]), add(x[14],x[4]), add(x[3],x[6]), x[19], x[17], x[4], x[1], x[14], x[17]], coeffs:[1, 10, 100, 1000, 10000, 100000, -1, -10, -100, -1000, -10000, -100000], condition:(eq,0))\n"
     ]
    }
   ],
   "source": [
    "print(posted(-1))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ee1dd49a",
   "metadata": {},
   "source": [
    "We can now obtain a valid solution."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "1c1ad115",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "  [5, 2, 6, 4, 8, 5]\n",
      "+ [1, 9, 7, 4, 8, 5]\n",
      "= [7, 2, 3, 9, 7, 0]\n"
     ]
    }
   ],
   "source": [
    "if solve() is SAT:\n",
    "    print(\" \", values(x1))\n",
    "    print(\"+\", values(x2))\n",
    "    print(\"=\", values(x3))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c834394c",
   "metadata": {},
   "source": [
    "By the way, does there exist several solutions? We can check it as follows."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "014b5c85",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Number of solutions:  1\n"
     ]
    }
   ],
   "source": [
    "if solve(sols=ALL) is SAT:\n",
    "    print(\"Number of solutions: \", n_solutions())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "dbd96b74",
   "metadata": {},
   "source": [
    "If you want to solve another puzzle, replace for example [\"donald\", \"gerald\", \"robert\"] by [\"no\", \"no\", \"yes\"] at the top of this page, and restart the jupyter kernel."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "41114caa",
   "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). "
   ]
  },
  {
   "cell_type": "raw",
   "id": "b909ef00",
   "metadata": {
    "raw_mimetype": "text/x-python"
   },
   "source": [
    "from pycsp3 import *\n",
    "\n",
    "word1, word2, word3 = words = [w.lower() for w in data]\n",
    "letters = set(alphabet_positions(word1 + word2 + word3))\n",
    "n = len(word1) \n",
    "\n",
    "assert len(word2) == n and len(word3) in {n, n + 1}\n",
    "\n",
    "# x[i] is the value assigned to the ith letter (if present) of the alphabet\n",
    "x = VarArray(size=26, dom=lambda i: range(10) if i in letters else None)\n",
    "\n",
    "# auxiliary lists of variables associated with the three words\n",
    "x1, x2, x3 = [[x[i] for i in alphabet_positions(word)] for word in words]\n",
    "\n",
    "satisfy(\n",
    "    # all letters must be assigned different values\n",
    "    AllDifferent(x),\n",
    "\n",
    "    # the most significant letter of each word cannot be equal to 0\n",
    "    [x1[0] != 0, x2[0] != 0, x3[0] != 0],\n",
    "\n",
    "    # ensuring the crypto-arithmetic sum\n",
    "    Sum((x1[-i-1] + x2[-i-1]) * 10 ** i for i in range(n))\n",
    "      == Sum(x3[-i-1] * 10 ** i for i in range(len(x3)))\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
}