{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "0ed0eb0e",
   "metadata": {},
   "source": [
    "# Puzzle logique\n",
    "\n",
    "## Énoncés\n",
    "\n",
    "1. Si le train arrive en retard et s’il n’y a pas de taxis à la gare,\n",
    "alors l’invité arrive en retard.\n",
    "2. L’invité n’est pas en retard.\n",
    "3. Le train est arrivé en retard.\n",
    "\n",
    "**Comment déduire qu’il y avait des taxis à la gare?**\n",
    "\n",
    "## Modélisation du problème en logique propositionnelle\n",
    "\n",
    "### Variables propositionnelles\n",
    "\n",
    "- `p`: \"le train arrive en retard\",\n",
    "- `q`: \"il y a des taxis à la gare\"\n",
    "- `r`: \"l’invité est en retard\"\n",
    "\n",
    "### Formalisation des énoncés\n",
    "\n",
    "1. Si le train arrive en retard et s’il n’y a pas de taxis à la gare,\n",
    "alors l’invité arrive en retard: $p \\land \\lnot q \\implies r$\n",
    "2. L’invité n’est pas en retard : $\\lnot r$\n",
    "3. Le train est arrivé en retard : $p$\n",
    "\n",
    "### Réduction à SAT\n",
    "\n",
    "Toute valuation qui satisfait les trois formules:\n",
    "\n",
    "$$(p \\land \\lnot q \\implies r) \\land (\\lnot r) \\land (p)$$\n",
    "\n",
    "est une solution à l'énigme"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "f84353b0",
   "metadata": {},
   "outputs": [],
   "source": [
    "# This is the Z3 library for SAT solving\n",
    "from z3 import Solver, Bool, Or, And, Not, Implies\n",
    "\n",
    "# Déclaration des variables\n",
    "p = Bool(\"p\")\n",
    "q = Bool(\"q\")\n",
    "r = Bool(\"r\")\n",
    "\n",
    "# Solver and constraints\n",
    "solver = Solver()\n",
    "solver.add(Implies(And(p, Not(q)), r)) # p /\\ ~q => r\n",
    "solver.add(Not(r))                     # ~r\n",
    "solver.add(p)                          # p\n",
    "\n",
    "# Check\n",
    "r = solver.check().r\n",
    "if r == 1:\n",
    "    print(solver.model())\n",
    "else:\n",
    "    print(\"Pas de solution\")"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "defaultInterpreterPath: 3.14.7.final.0",
   "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
}