walkSAT.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<table>\n",
    "    <tr>\n",
    "        <td><img src=\"./img/Macc.png\" width=\"auto\"/></td>\n",
    "        <td>\n",
    "            <table><tr>\n",
    "            <h1 style=\"color:blue;text-align:center\">Lógica para Ciencias de la Computación</h1></td>\n",
    "            </tr></table>   \n",
    "        <td>&nbsp;</td>\n",
    "        <td>\n",
    "            <table><tr>\n",
    "            <tp><p style=\"font-size:150%;text-align:center\">Taller</p></tp>\n",
    "            <tp><p style=\"font-size:150%;text-align:center\">Algoritmo WalkSAT</p></tp>\n",
    "            </tr></table>\n",
    "        </td>\n",
    "    </tr>\n",
    "</table>\n",
    "\n",
    "---"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Objetivo <a class=\"anchor\" id=\"inicio\"></a>\n",
    "\n",
    "En clase hemos visto el algoritmo walkSAT para encontrar un modelo $I$ para una fórmula $S$ en forma clausal. En este notebook implementaremos este algoritmo en Python.\n",
    "\n",
    "Desarrollaremos la explicación mediante las siguientes secciones."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Secciones\n",
    "\n",
    "1. [Funciones auxiliares](#aux)\n",
    "2. [Walksat](#walk)\n",
    "3. [Comparación de tiempos](#comp)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Funciones auxiliares <a class=\"anchor\" id=\"aux\"></a>\n",
    "\n",
    "([Volver al inicio](#inicio))\n",
    "\n",
    "Para poder implementar el algoritmo walkSAT requerimos algunas funciones auxiliares:\n",
    "\n",
    "* `complemento()`: Sea $\\ell$ un literal. Se define \n",
    "\n",
    "`complemento`$(\\ell)=\\begin{cases}\n",
    "\\overline{p},&\\mbox { si }\\ell=p\\mbox{ para algún }p\\\\ \n",
    "p,&\\mbox{ si }\\ell=\\overline{p}\\mbox{ para algún }p\\\\\n",
    "\\end{cases}$\n",
    "\n",
    "* `interpretacion_aleatoria(letrasp)`: Devuelve una interpretación seleccionando aleatoriamente el valor True o False para cada letra proposicional en `letrasp`. \n",
    "\n",
    "* `flip_literal`$(I, \\ell)$: Modifica el valor de verdad asignado por la interpretación $I$ al literal $\\ell$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "from random import *\n",
    "from copy import deepcopy\n",
    "\n",
    "def complemento(l):\n",
    "    if '-' in l:\n",
    "        return l[1:]\n",
    "    else:\n",
    "        return '-' + l\n",
    "\n",
    "def interpretacion_aleatoria(letrasp):\n",
    "    I = {p:randint(0,1)==1 for p in letrasp}\n",
    "    return I\n",
    "\n",
    "def flip_literal(I, l):\n",
    "    p = l[-1]\n",
    "    valor = False if I[p] else True\n",
    "    Ip = deepcopy(I)\n",
    "    Ip[p] = valor\n",
    "    return Ip"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'p': True, 'q': True, 'r': True}"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "letrasp = ['p', 'q', 'r']\n",
    "I = interpretacion_aleatoria(letrasp)\n",
    "I"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'p': False, 'q': True, 'r': True}"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "I = flip_literal(I, 'p')\n",
    "I"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Para manejar la información sobre las letras proposicionales y las cláusulas de la fórmula que vayamos a trabajar, hemos definido una clase `WalkSatEstado` de la siguiente manera:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "class WalkSatEstado():\n",
    "    \n",
    "    def __init__(self, S):\n",
    "        self.S = S\n",
    "        self.letrasp = list(set([l[-1] for C in self.S for l in C]))\n",
    "        self.I = interpretacion_aleatoria(self.letrasp)\n",
    "        self.I_lits = set([p for p in self.letrasp if self.I[p]] + ['-'+p for p in self.letrasp if not self.I[p]])\n",
    "        self.clausulas_sat = [C for C in self.S if any((True for x in self.I_lits if x in C))]\n",
    "        self.clausulas_unsat = [C for C in self.S if C not in self.clausulas_sat]\n",
    "\n",
    "    def actualizar(self, I):\n",
    "        self.I = I\n",
    "        self.I_lits = set([p for p in self.letrasp if self.I[p]] + ['-'+p for p in self.letrasp if not self.I[p]])\n",
    "        self.clausulas_sat = [C for C in self.S if any((True for x in self.I_lits if x in C))]\n",
    "        self.clausulas_unsat = [C for C in self.S if C not in self.clausulas_sat]\n",
    "       \n",
    "    def SAT(self):\n",
    "        return len(self.clausulas_unsat) == 0\n",
    "\n",
    "    def break_count(self, l):\n",
    "        if l in self.I_lits:\n",
    "            lit = l\n",
    "        else:\n",
    "            lit = complemento(l)\n",
    "        clausulas_break_count = [C for C in self.clausulas_sat if set(C).intersection(self.I_lits)=={lit}]\n",
    "        return len(clausulas_break_count)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Consideremos una fórmula en forma clausal y veamos el correspondiente objeto `WalkSatEstado`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Fórmula: [['r'], ['p', '-r'], ['q', '-r'], ['-p', '-q', 'r']]\n",
      "Letras proposicionales: ['q', 'r', 'p']\n",
      "Interpretación: {'q': False, 'r': False, 'p': True}\n",
      "Literales determinados por la interpretación: {'-q', '-r', 'p'}\n",
      "Cláusulas sat: [['p', '-r'], ['q', '-r'], ['-p', '-q', 'r']]\n",
      "Cláusulas unsat [['r']]\n",
      "I hace verdadera la fórmula?: False\n"
     ]
    }
   ],
   "source": [
    "S = [['r'], ['p', '-r'], ['q', '-r'], ['-p', '-q', 'r']]\n",
    "w = WalkSatEstado(S)\n",
    "print(\"Fórmula:\", S)\n",
    "print(\"Letras proposicionales:\", w.letrasp)\n",
    "print(\"Interpretación:\", w.I)\n",
    "print(\"Literales determinados por la interpretación:\", w.I_lits)\n",
    "print(\"Cláusulas sat:\", w.clausulas_sat)\n",
    "print(\"Cláusulas unsat\", w.clausulas_unsat)\n",
    "print(\"I hace verdadera la fórmula?:\", w.SAT())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Observe que esta clase tiene definido el método `break_count()` para determinar cuántas cláusulas sat se vuelven unsat si se voltea el valor de un literal:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "1"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "w.break_count('-r')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "---"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# WalkSAT <a class=\"anchor\" id=\"walk\"></a>\n",
    "\n",
    "([Volver al inicio](#inicio))\n",
    "\n",
    "Presentamos ahora el algoritmo walkSAT.\n",
    "\n",
    "<img src=\"./img/walksat.png\" width=\"auto\"/>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Ejercicio 1:**\n",
    "\n",
    "Implemente la función `walkSAT`.\n",
    "\n",
    "Pruebe su respuesta con los siguientes ejemplos:\n",
    "\n",
    "1. `S = [['r'], ['p', '-r'], ['q', '-r'], ['-p', '-q', 'r']]` \n",
    "\n",
    "Solución:  $I\\,{=}\\,\\{r: True, p: True, q: True\\}$.\n",
    "\n",
    "2. `S=[['s'], ['-r', '-q'], ['r', 'q'], ['p', '-s'], ['r', '-s'], ['-p', '-r', 's']]` \n",
    "\n",
    "Solución: $I\\,{=}\\,\\{s: True, p: True, r: True, q: False\\}$.\n",
    "\n",
    "3. `S = [['s'], ['p','-t'], ['q','-t'], ['-p','-q','t'], ['t','-s'], ['r','-s'], ['-t','-r','s']]` \n",
    "\n",
    "Solución: $I\\,{=}\\,\\{s: True, p: True, r: True, q: False\\}$.\n",
    "\n",
    "4. `S = [['p','-q'],['-p','-q'],['q','r'],['-q''-r'],['-p','-r'],['p','-r']]` \n",
    "\n",
    "Solución: Intento fallido."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Fórmula: [['r'], ['p', '-r'], ['q', '-r'], ['-p', '-q', 'r']]\n",
      "('Satisfacible', {'q': True, 'r': True, 'p': True})\n"
     ]
    }
   ],
   "source": [
    "def walkSAT(A, max_flips=10, max_tries=10, p=0.2):\n",
    "    w = WalkSatEstado(A)\n",
    "    for i in range(max_tries):\n",
    "        w.actualizar(interpretacion_aleatoria(w.letrasp))\n",
    "        for j in range(max_flips):\n",
    "            if w.SAT():\n",
    "                return \"Satisfacible\", w.I\n",
    "            C = choice(w.clausulas_unsat)\n",
    "            breaks = [(l, w.break_count(l)) for l in C]\n",
    "            if any((x[1] == 0 for x in breaks)) > 0:\n",
    "                v = choice(breaks)[0]\n",
    "            else:\n",
    "                if uniform(0, 1) < p:\n",
    "                    assert (len(C) > 0), f\"{C}\"\n",
    "                    v = choice(C)\n",
    "                else:\n",
    "                    min_count = min([x[1] for x in breaks])\n",
    "                    mins = [x[0] for x in breaks if x[1] == min_count]\n",
    "                    v = choice(mins)\n",
    "            I = flip_literal(w.I, v)\n",
    "            w.actualizar(I)\n",
    "    print(\"Intento Fallido\")\n",
    "    return None\n",
    "\n",
    "\n",
    "S = [['r'], ['p', '-r'], ['q', '-r'], ['-p', '-q', 'r']]\n",
    "print(\"Fórmula:\", S)\n",
    "print(walkSAT(S))\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "---"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Comparación de tiempos <a class=\"anchor\" id=\"comp\"></a>\n",
    "\n",
    "([Volver al inicio](#inicio))\n",
    "\n",
    "Comparamos los tiempos de búsqueda de modelo para fórmulas aleatorias cada vez más grandes, entre los algoritmos DPLL y walkSAT."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Ejercicio 2:**\n",
    "\n",
    "Incluya aquí su implementación del DPLL."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from Logica import *"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [],
   "source": [
    "from time import time\n",
    "import seaborn as sns\n",
    "import pandas as pd\n",
    "import matplotlib.pyplot as plt\n",
    "\n",
    "def obtiene_tiempos(fun, args, num_it=100):\n",
    "    tiempos_fun = []\n",
    "    for i in range(num_it):\n",
    "        arranca = time()\n",
    "        x = fun(*args)\n",
    "        para = time()\n",
    "        tiempos_fun.append(para - arranca)\n",
    "    return tiempos_fun\n",
    "\n",
    "def compara_entradas_funs(funs, nombres_funs, lista_args, N=100):\n",
    "    entradas = []\n",
    "    funcion = []\n",
    "    tiempos = []\n",
    "    lista_dfs = []\n",
    "    for i, args in enumerate(lista_args):\n",
    "        for j, fun in enumerate(funs):\n",
    "            t = obtiene_tiempos(fun, [args], N)\n",
    "            tiempos += t\n",
    "            n = len(t)\n",
    "            entradas += [i+1]*n\n",
    "            funcion += [nombres_funs[j]]*n\n",
    "        df = pd.DataFrame({'Long_entrada':entradas, \n",
    "                           'Funcion':funcion,\n",
    "                           'Tiempo_prom':tiempos})\n",
    "        lista_dfs.append(df)\n",
    "    df = pd.concat(lista_dfs).reset_index()\n",
    "    sns.lineplot(x='Long_entrada',y='Tiempo_prom',hue='Funcion',data=df)\n",
    "    plt.show()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [],
   "source": [
    "from random import uniform, choice\n",
    "\n",
    "cantidad = 40\n",
    "letras = [chr(i) for i in range(257, 257+cantidad)]\n",
    "lista = [letras[0]]\n",
    "formula = letras[0]\n",
    "for p in letras[1:]:\n",
    "            neg1 = '-' if uniform(0,1) < .5 else ''\n",
    "            neg2 = '-' if uniform(0,1) < .5 else ''\n",
    "            neg3 = '-' if uniform(0,1) < .5 else ''\n",
    "            conectivo = choice(['Y','O','>'])\n",
    "            if uniform(0,1) < .5:\n",
    "                formula = neg1 + \"(\" + neg2 + formula + conectivo + neg3 + p + \")\"\n",
    "            else:\n",
    "                formula = neg1 + \"(\" + neg2 + p + conectivo + neg3 + formula + \")\"\n",
    "            lista.append(formula)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {
    "scrolled": false
   },
   "outputs": [
    {
     "ename": "NameError",
     "evalue": "name 'tseitin' is not defined",
     "output_type": "error",
     "traceback": [
      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[0;31mNameError\u001b[0m                                 Traceback (most recent call last)",
      "Cell \u001b[0;32mIn[20], line 5\u001b[0m\n\u001b[1;32m      3\u001b[0m sat_walksat \u001b[38;5;241m=\u001b[39m \u001b[38;5;28;01mlambda\u001b[39;00m formula: walkSAT(tseitin(formula))\n\u001b[1;32m      4\u001b[0m funs \u001b[38;5;241m=\u001b[39m [sat_dpll, sat_walksat]\n\u001b[0;32m----> 5\u001b[0m \u001b[43mcompara_entradas_funs\u001b[49m\u001b[43m(\u001b[49m\u001b[43mfuns\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43mnombres\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43mlista\u001b[49m\u001b[43m)\u001b[49m\n",
      "Cell \u001b[0;32mIn[14], line 22\u001b[0m, in \u001b[0;36mcompara_entradas_funs\u001b[0;34m(funs, nombres_funs, lista_args, N)\u001b[0m\n\u001b[1;32m     20\u001b[0m \u001b[38;5;28;01mfor\u001b[39;00m i, args \u001b[38;5;129;01min\u001b[39;00m \u001b[38;5;28menumerate\u001b[39m(lista_args):\n\u001b[1;32m     21\u001b[0m     \u001b[38;5;28;01mfor\u001b[39;00m j, fun \u001b[38;5;129;01min\u001b[39;00m \u001b[38;5;28menumerate\u001b[39m(funs):\n\u001b[0;32m---> 22\u001b[0m         t \u001b[38;5;241m=\u001b[39m \u001b[43mobtiene_tiempos\u001b[49m\u001b[43m(\u001b[49m\u001b[43mfun\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43m[\u001b[49m\u001b[43margs\u001b[49m\u001b[43m]\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43mN\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m     23\u001b[0m         tiempos \u001b[38;5;241m+\u001b[39m\u001b[38;5;241m=\u001b[39m t\n\u001b[1;32m     24\u001b[0m         n \u001b[38;5;241m=\u001b[39m \u001b[38;5;28mlen\u001b[39m(t)\n",
      "Cell \u001b[0;32mIn[14], line 10\u001b[0m, in \u001b[0;36mobtiene_tiempos\u001b[0;34m(fun, args, num_it)\u001b[0m\n\u001b[1;32m      8\u001b[0m \u001b[38;5;28;01mfor\u001b[39;00m i \u001b[38;5;129;01min\u001b[39;00m \u001b[38;5;28mrange\u001b[39m(num_it):\n\u001b[1;32m      9\u001b[0m     arranca \u001b[38;5;241m=\u001b[39m time()\n\u001b[0;32m---> 10\u001b[0m     x \u001b[38;5;241m=\u001b[39m \u001b[43mfun\u001b[49m\u001b[43m(\u001b[49m\u001b[38;5;241;43m*\u001b[39;49m\u001b[43margs\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m     11\u001b[0m     para \u001b[38;5;241m=\u001b[39m time()\n\u001b[1;32m     12\u001b[0m     tiempos_fun\u001b[38;5;241m.\u001b[39mappend(para \u001b[38;5;241m-\u001b[39m arranca)\n",
      "Cell \u001b[0;32mIn[20], line 2\u001b[0m, in \u001b[0;36m<lambda>\u001b[0;34m(formula)\u001b[0m\n\u001b[1;32m      1\u001b[0m nombres \u001b[38;5;241m=\u001b[39m [\u001b[38;5;124m'\u001b[39m\u001b[38;5;124mdpll\u001b[39m\u001b[38;5;124m'\u001b[39m, \u001b[38;5;124m'\u001b[39m\u001b[38;5;124mwalksat\u001b[39m\u001b[38;5;124m'\u001b[39m]\n\u001b[0;32m----> 2\u001b[0m sat_dpll \u001b[38;5;241m=\u001b[39m \u001b[38;5;28;01mlambda\u001b[39;00m formula: dpll(\u001b[43mtseitin\u001b[49m(formula), {})\n\u001b[1;32m      3\u001b[0m sat_walksat \u001b[38;5;241m=\u001b[39m \u001b[38;5;28;01mlambda\u001b[39;00m formula: walkSAT(tseitin(formula))\n\u001b[1;32m      4\u001b[0m funs \u001b[38;5;241m=\u001b[39m [sat_dpll, sat_walksat]\n",
      "\u001b[0;31mNameError\u001b[0m: name 'tseitin' is not defined"
     ]
    }
   ],
   "source": [
    "nombres = ['dpll', 'walksat']\n",
    "sat_dpll = lambda formula: dpll(tseitin(formula), {})\n",
    "sat_walksat = lambda formula: walkSAT(tseitin(formula))\n",
    "funs = [sat_dpll, sat_walksat]\n",
    "compara_entradas_funs(funs, nombres, lista)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Vemos que en todos los casos el DPLL es más rápido que el walkSAT."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "---"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "logica-venv",
   "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.12.7"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}