{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "f054b5b3",
   "metadata": {},
   "source": [
    "# Sudoku simplifié\n",
    "\n",
    "![Grille de sudoku 3x3](sudoku-simple.png)\n",
    "\n",
    "Remplir chaque case avec un chiffre parmi $\\{1,2,3\\}$\n",
    "\n",
    "Et, de telle sorte que chaque chiffre apparaisse une unique fois:\n",
    "- dans chaque ligne,\n",
    "- dans chaque colonne,\n",
    "- et dans chaque zone colorée\n",
    "\n",
    "## Réduction à SAT\n",
    "\n",
    "À partir d'une grille $G$ comme ci-dessus, on veut calculer une formule $\\varphi_G$ telle que **$\\varphi_G$ est satisfaite uniquement par les remplissages corrects de la grille**.\n",
    "\n",
    "On pourra alors utiliser un solveur SAT sur $\\varphi_G$ pour déterminer si elle est satisfiable, et pour obtenir un remplissage correct de $G$ cas échéant.\n",
    "\n",
    "## Modélisation en logique propositionnelle\n",
    "\n",
    "On cherche à calculer une **fonction** de remplissage qui associe une valeur parmi $\\{1, 2, 3\\}$ à chaque case de la grille. Cette fonction associe à chaque case $(i,j)$ la valeur $f(i,j)$.\n",
    "\n",
    "Nos variables propositionnelles vont donc encoder la proposition \"la case $(i,j)$ contient la valeur $k$\", pour toute case et pour toiute valeur. Nous aurons des variables $p_{i,j,k}$ pour $i, j, k \\in \\{1,2,3\\}$.\n",
    "- lorsque $p_{i,j,k}=1$, alors \"la case $(i,j)$ contient la valeur $k$\"\n",
    "- inversement, $p_{i,j,k}=0$ signifie que \"la case $(i,j)$ ne contient pas la valeur $k$\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "d123efa2",
   "metadata": {},
   "outputs": [],
   "source": [
    "# Accès au solver z3\n",
    "from z3 import Bool,Solver,Not,Or,And,Implies,sat\n",
    "\n",
    "# Intervalles des indices\n",
    "lines = range(1, 3 + 1)\n",
    "columns = range(1, 3 + 1)\n",
    "values = range(1, 3 + 1)\n",
    "\n",
    "# Définition des variables propositionnelles\n",
    "def name(i: int, j: int , k: int) -> str:\n",
    "    \"\"\" Return variable p_i,j,k name \"\"\"\n",
    "    return f\"p_{i}_{j}_{k}\"\n",
    "\n",
    "vars = {(i,j,k): Bool(name(i,j,k)) for i in lines for j in columns for k in values}\n",
    "\n",
    "# print(vars)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c88d3ca7",
   "metadata": {},
   "source": [
    "## Objet modélisé\n",
    "\n",
    "Les variables propositionnelles $p_{i,j,k}$ avec $i,j,k \\in \\{1,2,3\\}$ représentent-elles une fonction de remplissage? Expliquer."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f044fbbe",
   "metadata": {},
   "source": [
    "Non:\n",
    "- si $p_{111}$ et $p_{112}$ sont vraies, alors la case (1,1) contient à la fois 1 et 2\n",
    "- si $p_{111}=0$ et $p_{112}=0$ et $p_{113}=0$, alors la case (1,1) ne contient aucune valeur"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "dd9a5161",
   "metadata": {},
   "source": [
    "## Formalisation des contraintes\n",
    "\n",
    "Écrire une formule de logique propositionnelle qui exprime: \"s’il y a $1$ en case $(1,1)$, il n’y a pas $1$ en case $(1,2)$, ni en case $(1,3)$\""
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d585edbd",
   "metadata": {},
   "source": [
    "- FAUX: $p_{111} \\land \\lnot p_{121} \\land \\lnot p_{131}$\n",
    "- OK: $p_{111} \\implies (\\lnot p_{121} \\land \\lnot p_{131})$\n",
    "- DE MANIERE EQUIVALENTE: $(p_{111} \\implies \\lnot p_{121}) \\land (p_{111} \\implies \\lnot p_{131})$"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "308c4354",
   "metadata": {},
   "source": [
    "### Contrainte générique\n",
    "\n",
    "Généraliser la formule précédente à: \"s’il y a la valeur $k$ en case $(i,j)$, alors il n’y a pas la valeur $k$ dans les cases de l’ensemble $C$\". On notera $\\varphi_{i,j,k,C}$ la formule correspondante.\n",
    "\n",
    "On écrira $\\bigwedge_{(x,y) \\in C} \\ldots$ pour quantifier sur toutes les cases de $C$ (c’est à dire pour écrire: \"pour toute case $(x,y)$ de $C$ ...\")."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "40ab9b47",
   "metadata": {},
   "source": [
    "$\\bigwedge_{(x,y) \\in C} (p_{ijk} \\implies \\lnot p_{xyk})$\n",
    "\n",
    "Exemple, pour $(i,j) = (1,1)$, $k=1$ et $C=\\{(1,2), (1,3)\\}$ on a: $(p_{111} \\implies \\lnot p_{121}) \\land (p_{111} \\implies \\lnot p_{131})$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "020d3f45",
   "metadata": {},
   "outputs": [],
   "source": [
    "def takeValue(i, j, k, C):\n",
    "    \"\"\" Retourne une formule Z3 qui est vraie ssi quand (i,j) la valeur k, alors aucune cellule de C n'a la valeur k \"\"\"\n",
    "    l = [Implies(vars[(i,j,k)], Not(vars[(x,y,k)])) for (x,y) in C]\n",
    "    return And(l)\n",
    "\n",
    "# print(takeValue(1, 1, 1, [(1, 2), (1, 3)]))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4d599f67",
   "metadata": {},
   "source": [
    "### Unicité d'une valeur\n",
    "\n",
    "Écrire une formule $\\varphi_{k, C}$ qui exprime: \"la valeur $k$ apparaît au\n",
    "plus une fois dans l’ensemble de cases $C$\", en utilisant $\\varphi_{i,j,k,C}$."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1576e0ef",
   "metadata": {},
   "source": [
    "$\\bigwedge_{(i,j) \\in C} \\varphi_{i,j,k,C \\setminus (i,j)}$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "68e064e3",
   "metadata": {},
   "outputs": [],
   "source": [
    "def uniqueValue(k, C):\n",
    "    \"\"\" Retourne une formule Z3 qui est vraie si et seulement si au plus une case de C a la valeur k \"\"\"\n",
    "    l = [ takeValue(i, j, k, C - {(i, j)}) for (i, j) in C]\n",
    "    return And(l)\n",
    "\n",
    "# print(uniqueValue(1, {(1, 1), (1, 2), (1, 3)}))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "580e8142",
   "metadata": {},
   "source": [
    "### Unicité de toutes les valeurs\n",
    "\n",
    "Écrire une formule $\\varphi_{C}$ qui exprime: \"chaque valeur\n",
    "$k \\in \\{1,2,3\\}$ apparaît au plus une fois dans l’ensemble de cases\n",
    "$C$\"."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "03227546",
   "metadata": {},
   "source": [
    "$\\varphi_{1,C} \\land \\varphi_{2, C} \\land \\varphi_{3,C}$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "7a72c7ad",
   "metadata": {},
   "outputs": [],
   "source": [
    "def uniqueAllValues(C):\n",
    "    \"\"\" Retourne une formule Z3 qui est vraie si et seulement si chaque valeur de {1,2,3} apparaît au plus une fois dans C \"\"\"\n",
    "    l = [ uniqueValue(k, C) for k in values ]\n",
    "    return And(l)\n",
    "\n",
    "# print(uniqueAllValues({(1, 2), (1, 1), (1, 3)}))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "32e41ab8",
   "metadata": {},
   "source": [
    "### Unicité par blocs\n",
    "\n",
    "Écrire une formule $\\varphi_U$ qui exprime les contraintes d’unicité sur les lignes, les colonnes et les blocs de la grille en utilisant $\\varphi_C$.\n",
    "\n",
    "On notera L1, L2 et L3 les ensembles de cases correspondant aux lignes, C1, C2 et C3 ceux correspondant aux colonnes, et B1, B2 et B3 ceux correspondant aux blocs colorés."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "dd89c9df",
   "metadata": {},
   "source": [
    "$\\varphi_{L1} \\land \\varphi_{L2} \\land \\varphi_{L3} \\land \\varphi_{C1} \\land \\varphi_{C2} \\land \\varphi_{C3} \\land \\varphi_{B1} \\land \\varphi_{B2} \\land \\varphi_{B3}$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "1d265077",
   "metadata": {},
   "outputs": [],
   "source": [
    "# Définition des blocs\n",
    "\n",
    "L1 = {(1,1), (1,2), (1,3)}\n",
    "L2 = {(2,1), (2,2), (2,3)}\n",
    "L3 = {(3,1), (3,2), (3,3)}\n",
    "\n",
    "C1 = {(1,1), (2,1), (3,1)}\n",
    "C2 = {(1,2), (2,2), (3,2)}\n",
    "C3 = {(1,3), (2,3), (3,3)}\n",
    "\n",
    "B1 = L1\n",
    "B2 = {(1,2), (1,3), (2,3)}\n",
    "B3 = {(2,2), (3,2), (3,3)}\n",
    "\n",
    "# Contraintes d'unicité\n",
    "\n",
    "def unique():\n",
    "    \"\"\" Retourne une formule Z3 qui est vraie si et seulement si toutes les contraintes d'unicité sont respectées \"\"\"\n",
    "    l = [ uniqueAllValues(C) for C in [L1, L2, L3, C1, C2, C3, B1, B2, B3] ]\n",
    "    return And(l)\n",
    "\n",
    "# print(unique())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ac8e769d",
   "metadata": {},
   "source": [
    "### Problème de modélisation\n",
    "\n",
    "Pourquoi une valuation qui satisfait $\\varphi_U$ ne correspond-elle pas toujours à un remplissage valide de la grille?"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d9f3fe1a",
   "metadata": {},
   "source": [
    "Parce qu'on ne modélise pas une fonction de remplissage: une case peut avoir plus d'une valeur ou aucune valeur (cf. \"Objet modélisé\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5b11d7ff",
   "metadata": {},
   "source": [
    "Quelle formule $\\varphi_R$ faut-il adjoindre à $\\varphi_U$ pour résoudre ce problème?"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9ac46977",
   "metadata": {},
   "source": [
    "On doit exprimer que chaque case de la grille contient au moins une valeur:\n",
    "\n",
    "$\\bigwedge_{(i,j) \\in Grille} (p_{ij1} \\lor p_{ij2} \\lor p_{ij3})$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "150727c6",
   "metadata": {},
   "outputs": [],
   "source": [
    "# NB: du fait des contraintes d'unicité, il suffit de dire que chaque case \n",
    "# contient au moins une valeur\n",
    "\n",
    "def at_least_one_value(i, j):\n",
    "    \"\"\" Retourne une formule Z3 qui est vraie si et seulement si la case (i, j) possède au moins une valeur dans {1, 2, 3} \"\"\"\n",
    "    return Or([vars[(i, j, k)] for k in values])\n",
    "\n",
    "def consistent_valuation():\n",
    "    \"\"\" Retourne une formule Z3 qui est vraie si et seulement si le remplissage attribue une et une seule valeur à chaque case de la grille \"\"\"\n",
    "    return And([at_least_one_value(i, j) for i in lines for j in columns])\n",
    "\n",
    "print(consistent_valuation())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "cad886d4",
   "metadata": {},
   "source": [
    "### Valeurs initiales\n",
    "\n",
    "On fixe usuellement la valeur de certaines cases, comme la case `(2,1)` dans la grille précédente. Comment modéliser ces valeurs fixées?"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "70b038a3",
   "metadata": {},
   "source": [
    "On doit spécifier que les propositions correspondantes sont vraies, ici: $p_{2,1,3}$\n",
    "\n",
    "D'une façon, générale, la formule $\\varphi_I$ est la conjonction des variables propositionnelles correspondant aux cases initialement remplies. Par exemple, si nous avons initialement $1$ en $(1,1)$ et $2$ en $(1,2)$, la formule $\\varphi_I$ est: $p_{111} \\land p_{122}$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "d0e0bc62",
   "metadata": {},
   "outputs": [],
   "source": [
    "def initial_values():\n",
    "    \"\"\" Retourne une formule qui est vraie ssi la solution respecte les valeurs initiales de la grille \"\"\"\n",
    "    return vars[2, 1, 3]"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d9ab1676",
   "metadata": {},
   "source": [
    "### Obtenir une solution\n",
    "\n",
    "À partir des formules précédentes, définir la formule $\\varphi_G$ qui est vraie si et seulement si la grille a un remplissage valide."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "230f4cc9",
   "metadata": {},
   "source": [
    "$\\varphi_G$ est la conjonction de $\\varphi_U \\land \\varphi_R \\land \\varphi_I$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "41c4d5e2",
   "metadata": {},
   "outputs": [],
   "source": [
    "# Formula PhiG\n",
    "phiG = And(unique(), consistent_valuation(), initial_values())\n",
    "\n",
    "def print_model(m):\n",
    "    \"\"\" Prints the model `m` which is assumed to be a dictionary from variables to True/False \"\"\"\n",
    "    for i in lines:\n",
    "        for j in columns:\n",
    "            val = [k for k in values if m[vars[(i,j,k)]]]\n",
    "            print(f\"({i}, {j}) -> {val}\")\n",
    "\n",
    "# Solve the game and print a model is any\n",
    "solver = Solver()\n",
    "solver.add(phiG)\n",
    "\n",
    "if not solver.check() == sat:\n",
    "    print(\"La grille n'a pas de solution\")\n",
    "else:\n",
    "    print(\"La grille a une solution\")\n",
    "    print_model(solver.model())\n",
    "                "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7439c4be",
   "metadata": {},
   "source": [
    "### Unicité de la solution?\n",
    "\n",
    "Supposons qu’un algorithme fournit un remplissage valide r de G à partir de $\\varphi_G$. Comment utiliser cet algorithme pour vérifier si r est l’unique solution de G?"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "43eb9fec",
   "metadata": {},
   "source": [
    "À partir de $r$, on peut définir une **formule caractéristique** $\\varphi_r$, qui est vraie uniquement pour la valuation $r$.\n",
    "\n",
    "Exemple la formule caractéristique de $p=1$, $q=0$ et $r=1$ est: $p \\land \\lnot q \\land r$\n",
    "\n",
    "On demande au solveur de résoudre $\\varphi_G \\land \\lnot \\varphi_r$, c'est à dire de fournir une valuation qui satisfait à la fois $\\varphi_G$ (donc une solution de la grille), et qui ne satisfait pas $\\varphi_r$ (donc qui n'est pas $r$)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "b3b50a7c",
   "metadata": {},
   "outputs": [],
   "source": [
    "def formula_from_model(m):\n",
    "    \"\"\" Retourne la formule caractéristique de `m` qui est supposé associer à chaque variable une valeur True/False \"\"\"\n",
    "    f = True\n",
    "    for i in lines:\n",
    "        for j in columns:\n",
    "            for k in values:\n",
    "                l = vars[(i,j,k)]\n",
    "                if m[l] == False:\n",
    "                    l = Not(l)\n",
    "                f = And(f, l)\n",
    "    return f\n",
    "\n",
    "def print_satisfying_valuations(f):\n",
    "    \"\"\" Enumère et affiche toutes les valuations qui satisfont la formule f \"\"\"\n",
    "    s = Solver()\n",
    "    s.add(f)\n",
    "    while s.check() == sat:\n",
    "        print(\"--- modèle:\")\n",
    "        m = s.model()\n",
    "        print_model(m)\n",
    "        s.add(Not(formula_from_model(m)))\n",
    "    print(\"No more model\")\n",
    "\n",
    "print_satisfying_valuations(phiG)"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "pyvenv-3.14 (3.14.7)",
   "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.14.7"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}