{ "nbformat": 4, "nbformat_minor": 0, "metadata": { "colab": { "provenance": [] }, "kernelspec": { "name": "python3", "display_name": "Python 3" }, "language_info": { "name": "python" } }, "cells": [ { "cell_type": "code", "execution_count": 3, "metadata": { "colab": { "base_uri": "https://localhost:8080/" }, "id": "jUxZP_GaG0wG", "outputId": "936f6fca-1590-458b-e8e6-27c657ceb251" }, "outputs": [ { "output_type": "stream", "name": "stdout", "text": [ "βœ… Solver v3 implementado\n", "\n", "======================================================================\n", "πŸ§ͺ TESTS EXHAUSTIVOS - SOLVER V3\n", "======================================================================\n", "\n", "──────────────────────────────────────────────────────────────────────\n", "πŸ“Œ Unit clauses\n", "──────────────────────────────────────────────────────────────────────\n", "πŸ“Š 3 variables, 3 clΓ‘usulas\n", "\n", " Unit: (1) β†’ Β¬1β†’1\n", " Unit: (2) β†’ Β¬2β†’2\n", " Unit: (3) β†’ Β¬3β†’3\n", "\n", "πŸ” SCCs encontradas: 6\n", " x1: SCC(+)=0, SCC(-)=1 β†’ True\n", " x2: SCC(+)=2, SCC(-)=3 β†’ True\n", " x3: SCC(+)=4, SCC(-)=5 β†’ True\n", "\n", " AsignaciΓ³n: {1: True, 2: True, 3: True}\n", " VerificaciΓ³n: βœ…\n", "\n", "──────────────────────────────────────────────────────────────────────\n", "πŸ“Œ Mixed\n", "──────────────────────────────────────────────────────────────────────\n", "πŸ“Š 3 variables, 3 clΓ‘usulas\n", "\n", " Unit: (1) β†’ Β¬1β†’1\n", " Binary: (-1 ∨ 2) β†’ Β¬-1β†’2, Β¬2β†’-1\n", " Binary: (-2 ∨ 3) β†’ Β¬-2β†’3, Β¬3β†’-2\n", "\n", "πŸ” SCCs encontradas: 6\n", " x1: SCC(+)=2, SCC(-)=3 β†’ True\n", " x2: SCC(+)=1, SCC(-)=4 β†’ True\n", " x3: SCC(+)=0, SCC(-)=5 β†’ True\n", "\n", " AsignaciΓ³n: {1: True, 2: True, 3: True}\n", " VerificaciΓ³n: βœ…\n", "\n", "──────────────────────────────────────────────────────────────────────\n", "πŸ“Œ ContradicciΓ³n\n", "──────────────────────────────────────────────────────────────────────\n", "πŸ“Š 1 variables, 2 clΓ‘usulas\n", "\n", " Unit: (1) β†’ Β¬1β†’1\n", " Unit: (-1) β†’ Β¬-1β†’-1\n", "\n", "πŸ” SCCs encontradas: 1\n", "❌ ContradicciΓ³n en x1\n", " ❌ UNSAT (correcto)\n", "\n", "──────────────────────────────────────────────────────────────────────\n", "πŸ“Œ 2-SAT simple\n", "──────────────────────────────────────────────────────────────────────\n", "πŸ“Š 3 variables, 3 clΓ‘usulas\n", "\n", " Binary: (1 ∨ 2) β†’ Β¬1β†’2, Β¬2β†’1\n", " Binary: (-1 ∨ 3) β†’ Β¬-1β†’3, Β¬3β†’-1\n", " Binary: (-2 ∨ -3) β†’ Β¬-2β†’-3, Β¬-3β†’-2\n", "\n", "πŸ” SCCs encontradas: 2\n", " x1: SCC(+)=0, SCC(-)=1 β†’ True\n", " x2: SCC(+)=1, SCC(-)=0 β†’ False\n", " x3: SCC(+)=0, SCC(-)=1 β†’ True\n", "\n", " AsignaciΓ³n: {1: True, 2: False, 3: True}\n", " VerificaciΓ³n: βœ…\n", "\n", "──────────────────────────────────────────────────────────────────────\n", "πŸ“Œ 3-SAT\n", "──────────────────────────────────────────────────────────────────────\n", "πŸ“Š 4 variables, 3 clΓ‘usulas\n", "\n", " Ternary: (1 ∨ 2 ∨ 3) usando y=5\n", " Binary: (1 ∨ 5) β†’ Β¬1β†’5, Β¬5β†’1\n", " Binary: (-5 ∨ 2) β†’ Β¬-5β†’2, Β¬2β†’-5\n", " Binary: (-5 ∨ 3) β†’ Β¬-5β†’3, Β¬3β†’-5\n", " Ternary: (-1 ∨ -2 ∨ 4) usando y=6\n", " Binary: (-1 ∨ 6) β†’ Β¬-1β†’6, Β¬6β†’-1\n", " Binary: (-6 ∨ -2) β†’ Β¬-6β†’-2, Β¬-2β†’-6\n", " Binary: (-6 ∨ 4) β†’ Β¬-6β†’4, Β¬4β†’-6\n", " Ternary: (-3 ∨ -4 ∨ 1) usando y=7\n", " Binary: (-3 ∨ 7) β†’ Β¬-3β†’7, Β¬7β†’-3\n", " Binary: (-7 ∨ -4) β†’ Β¬-7β†’-4, Β¬-4β†’-7\n", " Binary: (-7 ∨ 1) β†’ Β¬-7β†’1, Β¬1β†’-7\n", "\n", "πŸ” SCCs encontradas: 2\n", " x1: SCC(+)=0, SCC(-)=1 β†’ True\n", " x2: SCC(+)=1, SCC(-)=0 β†’ False\n", " x3: SCC(+)=1, SCC(-)=0 β†’ False\n", " x4: SCC(+)=0, SCC(-)=1 β†’ True\n", "\n", " AsignaciΓ³n: {1: True, 2: False, 3: False, 4: True}\n", " VerificaciΓ³n: βœ…\n", "\n", "──────────────────────────────────────────────────────────────────────\n", "πŸ“Œ Chain implication\n", "──────────────────────────────────────────────────────────────────────\n", "πŸ“Š 4 variables, 4 clΓ‘usulas\n", "\n", " Unit: (1) β†’ Β¬1β†’1\n", " Binary: (-1 ∨ 2) β†’ Β¬-1β†’2, Β¬2β†’-1\n", " Binary: (-2 ∨ 3) β†’ Β¬-2β†’3, Β¬3β†’-2\n", " Binary: (-3 ∨ 4) β†’ Β¬-3β†’4, Β¬4β†’-3\n", "\n", "πŸ” SCCs encontradas: 8\n", " x1: SCC(+)=3, SCC(-)=4 β†’ True\n", " x2: SCC(+)=2, SCC(-)=5 β†’ True\n", " x3: SCC(+)=1, SCC(-)=6 β†’ True\n", " x4: SCC(+)=0, SCC(-)=7 β†’ True\n", "\n", " AsignaciΓ³n: {1: True, 2: True, 3: True, 4: True}\n", " VerificaciΓ³n: βœ…\n", "\n", "======================================================================\n", "πŸ“Š RESULTADO: 6/6 tests pasaron\n", "======================================================================\n" ] } ], "source": [ "#@title πŸ”§ **Solver v3 - PropagaciΓ³n Correcta**\n", "\n", "from collections import defaultdict\n", "from typing import List, Tuple, Optional, Dict, Set\n", "\n", "class TarjanSCC:\n", " \"\"\"\n", " Algoritmo de Tarjan para encontrar Componentes Fuertemente Conexas\n", " Complejidad: O(V + E)\n", " \"\"\"\n", "\n", " def __init__(self, graph: Dict[int, List[int]]):\n", " self.graph = graph\n", " self.index_counter = [0]\n", " self.stack = []\n", " self.lowlinks = {}\n", " self.index = {}\n", " self.on_stack = set()\n", " self.sccs = []\n", " self.scc_map = {} # nodo -> id de SCC\n", "\n", " def strongconnect(self, v: int):\n", " self.index[v] = self.index_counter[0]\n", " self.lowlinks[v] = self.index_counter[0]\n", " self.index_counter[0] += 1\n", " self.stack.append(v)\n", " self.on_stack.add(v)\n", "\n", " for w in self.graph.get(v, []):\n", " if w not in self.index:\n", " self.strongconnect(w)\n", " self.lowlinks[v] = min(self.lowlinks[v], self.lowlinks[w])\n", " elif w in self.on_stack:\n", " self.lowlinks[v] = min(self.lowlinks[v], self.index[w])\n", "\n", " if self.lowlinks[v] == self.index[v]:\n", " scc = []\n", " while True:\n", " w = self.stack.pop()\n", " self.on_stack.remove(w)\n", " scc.append(w)\n", " self.scc_map[w] = len(self.sccs)\n", " if w == v:\n", " break\n", " self.sccs.append(scc)\n", "\n", " def find_sccs(self) -> List[List[int]]:\n", " all_nodes = set(self.graph.keys())\n", " for neighbors in self.graph.values():\n", " all_nodes.update(neighbors)\n", "\n", " for v in all_nodes:\n", " if v not in self.index:\n", " self.strongconnect(v)\n", "\n", " return self.sccs\n", "\n", "\n", "class SATSolverV3:\n", " \"\"\"\n", " SAT Solver con propagaciΓ³n de implicaciones correcta\n", " \"\"\"\n", "\n", " def __init__(self, verbose=False):\n", " self.verbose = verbose\n", " self.num_vars = 0\n", " self.clauses = []\n", " self.graph = defaultdict(list)\n", " self.aux_var_counter = 0\n", "\n", " def var_to_node(self, lit: int) -> int:\n", " var = abs(lit)\n", " is_neg = lit < 0\n", " return 2 * var + (1 if is_neg else 0)\n", "\n", " def node_to_lit(self, node: int) -> int:\n", " var = node // 2\n", " is_neg = node % 2 == 1\n", " return -var if is_neg else var\n", "\n", " def neg(self, node: int) -> int:\n", " return node ^ 1\n", "\n", " def add_edge(self, u: int, v: int):\n", " self.graph[u].append(v)\n", "\n", " def add_unit_clause(self, lit: int):\n", " \"\"\"ClΓ‘usula unitaria: Β¬lit β†’ lit\"\"\"\n", " node = self.var_to_node(lit)\n", " self.add_edge(self.neg(node), node)\n", "\n", " if self.verbose:\n", " print(f\" Unit: ({lit}) β†’ Β¬{lit}β†’{lit}\")\n", "\n", " def add_binary_clause(self, a: int, b: int):\n", " \"\"\"ClΓ‘usula binaria: Β¬aβ†’b y Β¬bβ†’a\"\"\"\n", " node_a = self.var_to_node(a)\n", " node_b = self.var_to_node(b)\n", "\n", " self.add_edge(self.neg(node_a), node_b)\n", " self.add_edge(self.neg(node_b), node_a)\n", "\n", " if self.verbose:\n", " print(f\" Binary: ({a} ∨ {b}) β†’ Β¬{a}β†’{b}, Β¬{b}β†’{a}\")\n", "\n", " def add_ternary_clause(self, a: int, b: int, c: int):\n", " \"\"\"ReducciΓ³n Tseitin: (a∨b∨c) β†’ (a∨y)∧(Β¬y∨b)∧(Β¬y∨c)\"\"\"\n", " self.aux_var_counter += 1\n", " y = self.num_vars + self.aux_var_counter\n", "\n", " if self.verbose:\n", " print(f\" Ternary: ({a} ∨ {b} ∨ {c}) usando y={y}\")\n", "\n", " self.add_binary_clause(a, y)\n", " self.add_binary_clause(-y, b)\n", " self.add_binary_clause(-y, c)\n", "\n", " def add_clause(self, literals: List[int]):\n", " self.clauses.append(literals)\n", "\n", " if len(literals) == 0:\n", " self.add_unit_clause(1)\n", " self.add_unit_clause(-1)\n", " elif len(literals) == 1:\n", " self.add_unit_clause(literals[0])\n", " elif len(literals) == 2:\n", " self.add_binary_clause(literals[0], literals[1])\n", " elif len(literals) == 3:\n", " self.add_ternary_clause(literals[0], literals[1], literals[2])\n", " else:\n", " self.reduce_long_clause(literals)\n", "\n", " def reduce_long_clause(self, literals: List[int]):\n", " if len(literals) <= 3:\n", " self.add_clause(literals)\n", " return\n", "\n", " self.aux_var_counter += 1\n", " y = self.num_vars + self.aux_var_counter\n", "\n", " self.add_binary_clause(literals[0], y)\n", " self.reduce_long_clause([-y] + literals[1:])\n", "\n", " def parse_dimacs(self, dimacs_text: str):\n", " lines = dimacs_text.strip().split('\\n')\n", "\n", " for line in lines:\n", " line = line.strip()\n", " if not line or line.startswith('c'):\n", " continue\n", "\n", " if line.startswith('p cnf'):\n", " parts = line.split()\n", " self.num_vars = int(parts[2])\n", " if self.verbose:\n", " print(f\"πŸ“Š {self.num_vars} variables, {parts[3]} clΓ‘usulas\\n\")\n", " continue\n", "\n", " tokens = line.split()\n", " literals = [int(x) for x in tokens if x != '0']\n", "\n", " if literals:\n", " self.add_clause(literals)\n", "\n", " def solve(self) -> Tuple[bool, Optional[Dict[int, bool]]]:\n", " \"\"\"Resolver usando Tarjan + asignaciΓ³n correcta por orden topolΓ³gico\"\"\"\n", "\n", " # Ejecutar Tarjan\n", " tarjan = TarjanSCC(dict(self.graph))\n", " sccs = tarjan.find_sccs()\n", "\n", " if self.verbose:\n", " print(f\"\\nπŸ” SCCs encontradas: {len(sccs)}\")\n", "\n", " # Verificar satisfacibilidad\n", " total_vars = self.num_vars + self.aux_var_counter\n", "\n", " for var in range(1, total_vars + 1):\n", " pos = self.var_to_node(var)\n", " neg = self.var_to_node(-var)\n", "\n", " scc_pos = tarjan.scc_map.get(pos, -1)\n", " scc_neg = tarjan.scc_map.get(neg, -1)\n", "\n", " if scc_pos != -1 and scc_neg != -1 and scc_pos == scc_neg:\n", " if self.verbose:\n", " print(f\"❌ ContradicciΓ³n en x{var}\")\n", " return False, None\n", "\n", " # Construir asignaciΓ³n usando orden topolΓ³gico CORRECTO\n", " # En Tarjan, las SCCs se descubren en orden topolΓ³gico INVERSO\n", " # Entonces: scc_id mayor = viene ANTES en el orden topolΓ³gico\n", " # Si SCC(x) viene DESPUΓ‰S de SCC(Β¬x) en orden topolΓ³gico β†’ x = True\n", " # Esto significa: si scc_id(x) < scc_id(Β¬x) β†’ x = True\n", "\n", " assignment = {}\n", "\n", " for var in range(1, self.num_vars + 1):\n", " pos = self.var_to_node(var)\n", " neg = self.var_to_node(-var)\n", "\n", " scc_pos = tarjan.scc_map.get(pos, -1)\n", " scc_neg = tarjan.scc_map.get(neg, -1)\n", "\n", " # Regla: x = True si SCC(x) viene DESPUΓ‰S de SCC(Β¬x) topolΓ³gicamente\n", " # Como Tarjan da orden inverso: scc_id menor = despuΓ©s topolΓ³gicamente\n", " assignment[var] = (scc_pos < scc_neg)\n", "\n", " if self.verbose:\n", " print(f\" x{var}: SCC(+)={scc_pos}, SCC(-)={scc_neg} β†’ {assignment[var]}\")\n", "\n", " return True, assignment\n", "\n", " def verify(self, assignment: Dict[int, bool]) -> bool:\n", " for clause in self.clauses:\n", " satisfied = any(\n", " (lit > 0 and assignment.get(abs(lit), False)) or\n", " (lit < 0 and not assignment.get(abs(lit), False))\n", " for lit in clause\n", " )\n", " if not satisfied:\n", " return False\n", " return True\n", "\n", "print(\"βœ… Solver v3 implementado\")\n", "\n", "# Tests exhaustivos\n", "def exhaustive_test():\n", " print(\"\\n\" + \"=\"*70)\n", " print(\"πŸ§ͺ TESTS EXHAUSTIVOS - SOLVER V3\")\n", " print(\"=\"*70)\n", "\n", " tests = [\n", " (\"Unit clauses\", \"p cnf 3 3\\n1 0\\n2 0\\n3 0\", True),\n", " (\"Mixed\", \"p cnf 3 3\\n1 0\\n-1 2 0\\n-2 3 0\", True),\n", " (\"ContradicciΓ³n\", \"p cnf 1 2\\n1 0\\n-1 0\", False),\n", " (\"2-SAT simple\", \"p cnf 3 3\\n1 2 0\\n-1 3 0\\n-2 -3 0\", True),\n", " (\"3-SAT\", \"p cnf 4 3\\n1 2 3 0\\n-1 -2 4 0\\n-3 -4 1 0\", True),\n", " (\"Chain implication\", \"p cnf 4 4\\n1 0\\n-1 2 0\\n-2 3 0\\n-3 4 0\", True),\n", " ]\n", "\n", " passed = 0\n", " failed = 0\n", "\n", " for name, dimacs, expected_sat in tests:\n", " print(f\"\\n{'─'*70}\")\n", " print(f\"πŸ“Œ {name}\")\n", " print(f\"{'─'*70}\")\n", "\n", " solver = SATSolverV3(verbose=True)\n", " solver.parse_dimacs(dimacs)\n", " is_sat, assignment = solver.solve()\n", "\n", " if is_sat != expected_sat:\n", " print(f\"❌ ERROR: Esperaba {'SAT' if expected_sat else 'UNSAT'}, obtuvo {'SAT' if is_sat else 'UNSAT'}\")\n", " failed += 1\n", " continue\n", "\n", " if is_sat:\n", " verified = solver.verify(assignment)\n", " print(f\"\\n AsignaciΓ³n: {assignment}\")\n", " print(f\" VerificaciΓ³n: {'βœ…' if verified else '❌'}\")\n", "\n", " if verified:\n", " passed += 1\n", " else:\n", " failed += 1\n", " print(f\" ⚠️ AsignaciΓ³n incorrecta!\")\n", " # Debug: mostrar quΓ© clΓ‘usula falla\n", " for i, clause in enumerate(solver.clauses):\n", " sat = any(\n", " (lit > 0 and assignment.get(abs(lit), False)) or\n", " (lit < 0 and not assignment.get(abs(lit), False))\n", " for lit in clause\n", " )\n", " if not sat:\n", " print(f\" ClΓ‘usula {i+1} falla: {clause}\")\n", " else:\n", " print(f\" ❌ UNSAT (correcto)\")\n", " passed += 1\n", "\n", " print(f\"\\n{'='*70}\")\n", " print(f\"πŸ“Š RESULTADO: {passed}/{passed+failed} tests pasaron\")\n", " print(f\"{'='*70}\")\n", "\n", "exhaustive_test()\n" ] } ] }