{ "nbformat": 4, "nbformat_minor": 0, "metadata": { "colab": { "provenance": [] }, "kernelspec": { "name": "python3", "display_name": "Python 3" }, "language_info": { "name": "python" } }, "cells": [ { "cell_type": "code", "source": [ "\"\"\"\n", "Implementación: \"Reducing SAT to 2-SAT\" - Sergey Gubin (arXiv:0704.0108)\n", "\"\"\"\n", "\n", "import itertools\n", "import random\n", "import time\n", "from typing import List, Tuple, Dict, Optional, Set\n", "\n", "# =============================================================================\n", "# SAT Instance\n", "# =============================================================================\n", "class SATInstance:\n", " def __init__(self, num_vars: int, clauses: List[List[int]]):\n", " self.num_vars = num_vars\n", " self.clauses = clauses\n", " self.m = len(clauses)\n", "\n", " def __repr__(self):\n", " parts = []\n", " for c in self.clauses:\n", " lits = [f\"x{l}\" if l > 0 else f\"¬x{-l}\" for l in c]\n", " parts.append(\"(\" + \"∨\".join(lits) + \")\")\n", " return \" ∧ \".join(parts)\n", "\n", " def brute_force(self) -> Optional[Dict[int, bool]]:\n", " for bits in itertools.product([False, True], repeat=self.num_vars):\n", " asgn = {i+1: bits[i] for i in range(self.num_vars)}\n", " if all(\n", " any((l > 0 and asgn[abs(l)]) or (l < 0 and not asgn[abs(l)]) for l in c)\n", " for c in self.clauses\n", " ):\n", " return asgn\n", " return None\n", "\n", "# =============================================================================\n", "# 2-SAT Solver (Kosaraju SCCs)\n", "# =============================================================================\n", "class TwoSAT:\n", " def __init__(self, num_vars: int, clauses: list):\n", " self.n = num_vars\n", " self.clauses = clauses\n", "\n", " def solve(self) -> Optional[Dict[int, bool]]:\n", " n = self.n\n", " N = 2 * n\n", " adj = [[] for _ in range(N)]\n", " radj = [[] for _ in range(N)]\n", "\n", " def node(lit):\n", " return 2*(abs(lit)-1) + (0 if lit > 0 else 1)\n", "\n", " def neg(nd):\n", " return nd ^ 1\n", "\n", " for cl in self.clauses:\n", " if len(cl) == 1:\n", " a = node(cl[0])\n", " adj[neg(a)].append(a)\n", " radj[a].append(neg(a))\n", " elif len(cl) == 2:\n", " a, b = node(cl[0]), node(cl[1])\n", " adj[neg(a)].append(b); radj[b].append(neg(a))\n", " adj[neg(b)].append(a); radj[a].append(neg(b))\n", "\n", " visited = [False]*N; order = []\n", " def dfs1(s):\n", " stk = [(s,False)]\n", " while stk:\n", " v, done = stk.pop()\n", " if done: order.append(v); continue\n", " if visited[v]: continue\n", " visited[v] = True\n", " stk.append((v,True))\n", " for w in adj[v]:\n", " if not visited[w]: stk.append((w,False))\n", " for i in range(N):\n", " if not visited[i]: dfs1(i)\n", "\n", " comp = [-1]*N; c = 0\n", " def dfs2(s, c):\n", " stk = [s]\n", " while stk:\n", " v = stk.pop()\n", " if comp[v] != -1: continue\n", " comp[v] = c\n", " for w in radj[v]:\n", " if comp[w] == -1: stk.append(w)\n", " for v in reversed(order):\n", " if comp[v] == -1: dfs2(v, c); c += 1\n", "\n", " for i in range(n):\n", " if comp[2*i] == comp[2*i+1]: return None\n", "\n", " return {i+1: comp[2*i] > comp[2*i+1] for i in range(n)}\n", "\n", "# =============================================================================\n", "# Sección 2: Representación SAT con XOR + restricciones de compatibilidad\n", "# =============================================================================\n", "class GubinReduction:\n", " def __init__(self, sat: SATInstance):\n", " self.sat = sat\n", " self.m = sat.m\n", " self.clauses = sat.clauses\n", "\n", " # Variables indicadoras ξ_{i,j}: variable_id para cada literal de cada cláusula\n", " self.xi = {} # (clause_idx, lit_idx) -> var_id\n", " self.xi_inv = {} # var_id -> (clause_idx, lit_idx)\n", " vid = 1\n", " for i, cl in enumerate(self.clauses):\n", " for j in range(len(cl)):\n", " self.xi[(i,j)] = vid\n", " self.xi_inv[vid] = (i,j)\n", " vid += 1\n", " self.num_xi = vid - 1\n", "\n", " # Conjuntos B_{ij} - pares de indicadores con literales complementarios\n", " self.B = {}\n", " for i in range(self.m):\n", " for j in range(i+1, self.m):\n", " pairs = set()\n", " for mu, li in enumerate(self.clauses[i]):\n", " for nu, lj in enumerate(self.clauses[j]):\n", " if li == -lj:\n", " pairs.add((self.xi[(i,mu)], self.xi[(j,nu)]))\n", " if pairs:\n", " self.B[(i,j)] = pairs\n", "\n", " def build_g(self) -> List[List[int]]:\n", " \"\"\"Ecuación (3): g = ∧_i (ξ_{i,1} ⊕ ξ_{i,2} ⊕ ... ⊕ ξ_{i,n_i}) = true\"\"\"\n", " xor_constraints = []\n", " for i in range(self.m):\n", " vars_in_clause = [self.xi[(i,j)] for j in range(len(self.clauses[i]))]\n", " xor_constraints.append(vars_in_clause)\n", " return xor_constraints\n", "\n", " def build_h(self) -> List[Tuple[int,int]]:\n", " \"\"\"Ecuación (4): h = ∧ (¬ξ ∨ ¬ζ) para pares complementarios\"\"\"\n", " clauses_2sat = []\n", " for pairs in self.B.values():\n", " for (a, b) in pairs:\n", " clauses_2sat.append((-a, -b))\n", " return clauses_2sat\n", "\n", " def xor_to_2sat_clauses(self, variables: List[int]) -> Tuple[List, int]:\n", " \"\"\"\n", " Convierte XOR(v1, v2, ..., vk) = true a cláusulas 2-SAT usando\n", " variables auxiliares con la descomposición estándar en cadena.\n", "\n", " XOR(a,b) = true: (a∨b) ∧ (¬a∨¬b)\n", "\n", " XOR(a,b,c) = true: introducir aux t:\n", " XOR(a,b) = t y XOR(t,c) = true\n", "\n", " XOR(a,b) = t equivale a:\n", " (a∨b∨¬t) ∧ (a∨¬b∨t) ∧ (¬a∨b∨t) ∧ (¬a∨¬b∨¬t)\n", "\n", " Pero necesitamos cláusulas de tamaño ≤ 2, así que usamos\n", " la técnica de Tseitin extendida con más auxiliares.\n", "\n", " Para XOR de k variables, generamos k-1 auxiliares encadenados.\n", " \"\"\"\n", " n = len(variables)\n", " if n == 0:\n", " return [], 0\n", " if n == 1:\n", " # XOR(a) = true → a = true → cláusula unitaria (a)\n", " return [(variables[0],)], 0\n", "\n", " clauses = []\n", " aux_count = 0\n", " next_aux = self._next_var\n", "\n", " if n == 2:\n", " a, b = variables\n", " # XOR(a,b) = true: (a∨b) ∧ (¬a∨¬b)\n", " clauses.append((a, b))\n", " clauses.append((-a, -b))\n", " return clauses, 0\n", "\n", " # Para n ≥ 3: cadena de XORs con auxiliares\n", " # t1 = XOR(v1, v2), t2 = XOR(t1, v3), ..., t_{n-2} = XOR(t_{n-3}, v_{n-1})\n", " # final: XOR(t_{n-2}, v_n) = true\n", "\n", " chain_var = None\n", " for idx in range(n - 1):\n", " if idx == 0:\n", " a = variables[0]\n", " b = variables[1]\n", " else:\n", " a = chain_var\n", " b = variables[idx + 1]\n", "\n", " if idx == n - 2:\n", " # Última etapa: XOR(a, b) = true\n", " clauses.append((a, b))\n", " clauses.append((-a, -b))\n", " else:\n", " # Etapa intermedia: XOR(a, b) = t (nuevo auxiliar)\n", " t = next_aux\n", " next_aux += 1\n", " aux_count += 1\n", "\n", " # XOR(a,b) = t ↔ (a⊕b) ↔ t\n", " # Esto en CNF es:\n", " # (¬a ∨ ¬b ∨ ¬t) ∧ (a ∨ b ∨ ¬t) ∧ (a ∨ ¬b ∨ t) ∧ (¬a ∨ b ∨ t)\n", " # Pero son cláusulas de 3 literales...\n", " #\n", " # Necesitamos bajar a 2-SAT. Usamos la descomposición:\n", " # Introducimos auxiliar extra u para cada cláusula de 3.\n", " #\n", " # (x∨y∨z) se convierte en: (x∨u) ∧ (y∨¬u_... ) - pero esto\n", " # no preserva equivalencia perfecta para 3→2.\n", " #\n", " # Alternativa: codificar la tabla de verdad directamente.\n", " # XOR(a,b)=t tiene 4 filas true en la tabla:\n", " # a=0,b=0,t=0 | a=0,b=1,t=1 | a=1,b=0,t=1 | a=1,b=1,t=0\n", " #\n", " # Las implicaciones 2-SAT que se pueden extraer:\n", " # No hay conjunto de cláusulas 2-SAT que sea equivalente a XOR de 3 vars.\n", " #\n", " # SOLUCIÓN: Usar la representación exacta del paper.\n", " # El paper dice que g se procesa mediante las \"m iteraciones del método\n", " # de matrices de compatibilidad\" y NO se convierte directamente a 2-SAT.\n", " # Lo que queda después son las matrices 3×3 que se codifican como w.\n", " #\n", " # Entonces implementamos el método de compatibilidad directamente.\n", " chain_var = t\n", "\n", " self._next_var = next_aux\n", " return clauses, aux_count\n", "\n", " def compute_compatibility_and_reduce(self):\n", " \"\"\"\n", " Implementa las secciones 2-3 del paper:\n", "\n", " 1. Construir g (XOR constraints) y h (2-SAT clauses)\n", " 2. Aplicar el método de matrices de compatibilidad (m iteraciones)\n", " procesando las restricciones XOR de g\n", " 3. Las matrices restantes son 3×3 (una por cada par de cláusulas de h)\n", " 4. Codificar como w (1-SAT)\n", " 5. Retornar h ∧ w como instancia 2-SAT\n", "\n", " El \"método de matrices de compatibilidad\" según el paper:\n", " - Cada cláusula de la fórmula combinada g∧h tiene una tabla de verdad\n", " - Para cada par de cláusulas, la matriz de compatibilidad tiene las\n", " combinaciones de filas satisfactorias que no se contradicen\n", " - En cada iteración, se \"procesa\" una cláusula, actualizando todas\n", " las matrices de compatibilidad restantes\n", " \"\"\"\n", " g_xors = self.build_g() # XOR constraints\n", " h_clauses = self.build_h() # 2-SAT clauses (¬ξ ∨ ¬ζ)\n", " n_h = len(h_clauses)\n", "\n", " if n_h == 0:\n", " return \"SAT\", None, {\"case\": \"no_complementary\"}\n", "\n", " # -------------------------------------------------------------------\n", " # Método de matrices de compatibilidad\n", " # -------------------------------------------------------------------\n", " # Cada cláusula tiene asignaciones satisfactorias (filas de su truth table)\n", " # Para XOR(v1,...,vk)=true: todas las asignaciones con #true impar\n", " # Para (¬a ∨ ¬b): {(F,F),(F,T),(T,F)} = 3 asignaciones\n", "\n", " # Representar cada cláusula como lista de (asignación_satisfactoria)\n", " # donde asignación = dict{var: bool}\n", "\n", " all_clauses = [] # lista de cláusulas de g∧h en orden\n", " clause_sat_rows = [] # para cada cláusula, sus asignaciones satisfactorias\n", "\n", " # Primero las m cláusulas XOR de g\n", " for xor_vars in g_xors:\n", " rows = []\n", " for bits in itertools.product([False, True], repeat=len(xor_vars)):\n", " if sum(bits) % 2 == 1: # XOR = true\n", " row = {xor_vars[k]: bits[k] for k in range(len(xor_vars))}\n", " rows.append(row)\n", " all_clauses.append((\"xor\", xor_vars))\n", " clause_sat_rows.append(rows)\n", "\n", " # Luego las n cláusulas 2-SAT de h\n", " for cl in h_clauses:\n", " a, b = abs(cl[0]), abs(cl[1])\n", " sa = cl[0] > 0 # True si literal es positivo\n", " sb = cl[1] > 0\n", " rows = []\n", " for va in [False, True]:\n", " for vb in [False, True]:\n", " # Evaluar cláusula (la ∨ lb)\n", " la = va if sa else not va\n", " lb = vb if sb else not vb\n", " if la or lb:\n", " rows.append({a: va, b: vb})\n", " all_clauses.append((\"disj\", cl))\n", " clause_sat_rows.append(rows)\n", "\n", " total_clauses = len(all_clauses)\n", " m = self.m # número de cláusulas XOR\n", "\n", " # Matrices de compatibilidad: para cada par (i,j) con i k:\n", " # nueva_compat[i][j][r][s] = OR sobre t de (compat[k,i][t][r] AND compat[k,j][t][s])\n", " # pero solo para aquellos t donde la fila t de la cláusula k es \"aún válida\"\n", " #\n", " # Una fila t de la cláusula k es válida si existe al menos un par\n", " # compatible en alguna matriz que la involucre.\n", "\n", " for k in range(total_clauses - 2):\n", " # Determinar filas válidas de cláusula k\n", " rows_k = clause_sat_rows[k]\n", " num_rows_k = len(rows_k)\n", "\n", " valid_k = [True] * num_rows_k # inicialmente todas válidas\n", "\n", " # Verificar validez: fila t de k es válida si para todo j > k,\n", " # existe al menos un s en cláusula j tal que compat[k,j][t][s] = True\n", " for j in range(k+1, total_clauses):\n", " if (k,j) not in compat:\n", " continue\n", " mat_kj = compat[(k,j)]\n", " for t in range(num_rows_k):\n", " if not valid_k[t]:\n", " continue\n", " if not any(mat_kj[t][s] for s in range(len(mat_kj[t]))):\n", " valid_k[t] = False\n", "\n", " # Actualizar matrices para pares (i,j) donde i,j > k\n", " new_compat = {}\n", " remaining = list(range(k+1, total_clauses))\n", "\n", " for idx_i, i in enumerate(remaining):\n", " for j in remaining[idx_i+1:]:\n", " mat_ki = compat.get((k,i))\n", " mat_kj = compat.get((k,j))\n", " old_mat = compat.get((i,j))\n", "\n", " if old_mat is None:\n", " continue\n", "\n", " ri = clause_sat_rows[i]\n", " rj = clause_sat_rows[j]\n", "\n", " new_mat = [[False]*len(rj) for _ in range(len(ri))]\n", "\n", " for r in range(len(ri)):\n", " for s in range(len(rj)):\n", " if not old_mat[r][s]:\n", " continue\n", " # Verificar si existe alguna fila válida t de k\n", " # compatible con ambos r y s\n", " if mat_ki is not None and mat_kj is not None:\n", " found = False\n", " for t in range(num_rows_k):\n", " if valid_k[t] and mat_ki[t][r] and mat_kj[t][s]:\n", " found = True\n", " break\n", " new_mat[r][s] = found\n", " else:\n", " # Si no hay matriz de compatibilidad con k,\n", " # entonces k no comparte variables → siempre compatible\n", " new_mat[r][s] = any(valid_k)\n", "\n", " new_compat[(i,j)] = new_mat\n", "\n", " # Reemplazar matrices\n", " # Eliminar todas las que involucran k\n", " keys_to_del = [key for key in compat if k in key]\n", " for key in keys_to_del:\n", " del compat[key]\n", " # Actualizar con las nuevas\n", " for key, mat in new_compat.items():\n", " compat[key] = mat\n", "\n", " # Verificar si alguna matriz quedó toda False → UNSAT\n", " for key, mat in compat.items():\n", " if all(not mat[r][s] for r in range(len(mat)) for s in range(len(mat[r]))):\n", " return \"UNSAT\", None, {\"case\": \"all_false_matrix\", \"step\": k}\n", "\n", " # -------------------------------------------------------------------\n", " # Después de m iteraciones, quedan las matrices entre cláusulas de h\n", " # Según el paper, estas son matrices 3×3 (ecuación 7)\n", " # -------------------------------------------------------------------\n", "\n", " # Construir la fórmula 2-SAT: h ∧ w\n", " # h ya tenemos (h_clauses)\n", " # w codifica el contenido de las matrices restantes como 1-SAT\n", "\n", " # Recopilar las matrices restantes\n", " remaining_matrices = {}\n", " for (i,j), mat in compat.items():\n", " remaining_matrices[(i,j)] = mat\n", "\n", " # Crear variables para w: una variable por cada elemento de cada matriz\n", " next_var = self.num_xi + 1\n", " w_unit_clauses = [] # cláusulas unitarias para w\n", "\n", " for (i,j), mat in remaining_matrices.items():\n", " for r in range(len(mat)):\n", " for s in range(len(mat[r])):\n", " vid = next_var\n", " next_var += 1\n", " if mat[r][s]:\n", " w_unit_clauses.append((vid,))\n", " else:\n", " w_unit_clauses.append((-vid,))\n", "\n", " total_vars = next_var - 1\n", "\n", " # Fórmula 2-SAT final: h ∧ w (ecuación 9)\n", " final_clauses = []\n", " for cl in h_clauses:\n", " final_clauses.append(cl) # 2-literal clauses\n", " for cl in w_unit_clauses:\n", " final_clauses.append(cl) # 1-literal clauses (unit)\n", "\n", " info = {\n", " \"case\": \"reduced\",\n", " \"h_clauses\": len(h_clauses),\n", " \"w_clauses\": len(w_unit_clauses),\n", " \"total_2sat_clauses\": len(final_clauses),\n", " \"total_vars\": total_vars,\n", " \"remaining_matrices\": len(remaining_matrices),\n", " }\n", "\n", " solver = TwoSAT(total_vars, final_clauses)\n", " result = solver.solve()\n", "\n", " if result is not None:\n", " return \"SAT\", result, info\n", " else:\n", " return \"UNSAT\", None, info\n", "\n", "\n", "# =============================================================================\n", "# Tests\n", "# =============================================================================\n", "def run_tests():\n", " print(\"=\" * 70)\n", " print(\" Reducing SAT to 2-SAT (Gubin, arXiv:0704.0108)\")\n", " print(\"=\" * 70)\n", "\n", " tests = [\n", " (\"SAT simple\", 3, [[1, 2, 3]]),\n", " (\"3-SAT sat\", 3, [[1, 2, 3], [-1, -2, 3], [1, -2, -3]]),\n", " (\"UNSAT 1 var\", 1, [[1], [-1]]),\n", " (\"UNSAT 2 vars\", 2, [[1, 2], [-1, -2], [1, -2], [-1, 2]]),\n", " (\"3-SAT 4 vars\", 4, [[1, 2, 3], [-2, 3, 4], [-1, -3, 4], [1, -2, -4]]),\n", " (\"2-SAT nativo\", 3, [[1, 2], [-1, 3], [-2, -3]]),\n", " (\"3-SAT 5 vars\", 5, [[1,2,3],[-1,4,5],[-2,-3,4],[1,-4,-5],[-1,-2,5]]),\n", " (\"UNSAT pigeon\", 2, [[1, 2], [-1], [-2]]),\n", " ]\n", "\n", " ok = 0\n", " total = 0\n", " print(f\"\\n{'Test':<30} {'BF':>6} {'Gubin':>7} {'Match':>6}\")\n", " print(\"─\" * 55)\n", "\n", " for name, nv, cls in tests:\n", " sat = SATInstance(nv, cls)\n", " bf = sat.brute_force()\n", " bf_sat = bf is not None\n", "\n", " try:\n", " reducer = GubinReduction(sat)\n", " status, asgn, info = reducer.compute_compatibility_and_reduce()\n", " gubin_sat = (status == \"SAT\")\n", " except Exception as e:\n", " gubin_sat = None\n", " info = {\"error\": str(e)}\n", "\n", " total += 1\n", " match = (bf_sat == gubin_sat)\n", " if match: ok += 1\n", "\n", " bf_str = \"SAT\" if bf_sat else \"UNSAT\"\n", " g_str = \"SAT\" if gubin_sat else (\"UNSAT\" if gubin_sat is not None else \"ERR\")\n", " m_str = \"✅\" if match else \"❌\"\n", " print(f\" {name:<28} {bf_str:>6} {g_str:>7} {m_str:>6}\")\n", "\n", " print(\"─\" * 55)\n", " print(f\" Resultado: {ok}/{total} correctos\\n\")\n", "\n", " # Tests aleatorios\n", " print(\"Tests aleatorios:\")\n", " print(\"─\" * 55)\n", " random.seed(42)\n", " mismatches = 0\n", " rand_total = 0\n", "\n", " for nv in [3, 4]:\n", " for nc in [3, 4, 5, 6]:\n", " for _ in range(20):\n", " cls = []\n", " for _ in range(nc):\n", " sz = random.randint(2, 3)\n", " vs = random.sample(range(1, nv+1), min(sz, nv))\n", " cls.append([v if random.random() > 0.5 else -v for v in vs])\n", "\n", " sat = SATInstance(nv, cls)\n", " bf = sat.brute_force()\n", " bf_sat = bf is not None\n", "\n", " try:\n", " reducer = GubinReduction(sat)\n", " status, _, info = reducer.compute_compatibility_and_reduce()\n", " gubin_sat = (status == \"SAT\")\n", " except:\n", " gubin_sat = None\n", "\n", " rand_total += 1\n", " if bf_sat != gubin_sat:\n", " mismatches += 1\n", " if mismatches <= 5:\n", " print(f\" Mismatch: vars={nv} clauses={cls}\")\n", " print(f\" BF={'SAT' if bf_sat else 'UNSAT'} vs \"\n", " f\"Gubin={'SAT' if gubin_sat else 'UNSAT'}\")\n", "\n", " print(f\"\\n Aleatorios: {rand_total - mismatches}/{rand_total} correctos\")\n", " if mismatches > 0:\n", " print(f\" Discrepancias: {mismatches}\")\n", " print()\n", "\n", "run_tests()" ], "metadata": { "colab": { "base_uri": "https://localhost:8080/" }, "id": "Pmr9Zs7gVWep", "outputId": "f956c6b4-4681-4da5-a504-e55d4f9ea42e" }, "execution_count": 2, "outputs": [ { "output_type": "stream", "name": "stdout", "text": [ "======================================================================\n", " Reducing SAT to 2-SAT (Gubin, arXiv:0704.0108)\n", "======================================================================\n", "\n", "Test BF Gubin Match\n", "───────────────────────────────────────────────────────\n", " SAT simple SAT SAT ✅\n", " 3-SAT sat SAT SAT ✅\n", " UNSAT 1 var UNSAT UNSAT ✅\n", " UNSAT 2 vars UNSAT UNSAT ✅\n", " 3-SAT 4 vars SAT SAT ✅\n", " 2-SAT nativo SAT SAT ✅\n", " 3-SAT 5 vars SAT SAT ✅\n", " UNSAT pigeon UNSAT UNSAT ✅\n", "───────────────────────────────────────────────────────\n", " Resultado: 8/8 correctos\n", "\n", "Tests aleatorios:\n", "───────────────────────────────────────────────────────\n", "\n", " Aleatorios: 160/160 correctos\n", "\n" ] } ] } ] }