fork download 
  1. # ---------- Algoritmo para resolver 2-SAT ----------
  2. # Usa el método de "grafo de implicaciones" + componentes fuertemente conexas (Tarjan)
  3. # Cada variable x_i tiene dos nodos:
  4. #   i       -> representa x_i
  5. #   i + n   -> representa ¬x_i
  6. #
  7. # Si una variable y su negación están en la misma SCC => no hay solución.
  8. # Si no, se asignan según el orden inverso de las SCC.
  9.  
  10. # ---------- Entrada ----------
  11. n, m = map(int, input("Ingrese n (variables) y m (cláusulas): ").split())
  12.  
  13. # Creamos el grafo de 2n nodos
  14. N = 2 * n
  15. out = [[] for _ in range(N)]
  16. inv = [[] for _ in range(N)]  # grafo inverso para Kosaraju
  17.  
  18. # Función auxiliar para obtener el índice de una variable
  19. # Ejemplo:  x3  => 2
  20. #           ¬x3 => 2 + n
  21. def var_index(x):
  22.     # x viene como entero positivo o negativo
  23.     v = abs(x) - 1
  24.     return v if x > 0 else v + n
  25.  
  26. # ---------- Construcción del grafo de implicaciones ----------
  27. for _ in range(m):
  28.     a, b = map(int, input().split())
  29.     # cláusula (a ∨ b) -> (¬a → b) y (¬b → a)
  30.     out[var_index(-a)].append(var_index(b))
  31.     out[var_index(-b)].append(var_index(a))
  32.     inv[var_index(b)].append(var_index(-a))
  33.     inv[var_index(a)].append(var_index(-b))
  34.  
  35. # ---------- Kosaraju para SCC ----------
  36. marked = [False] * N
  37. order = []
  38. comp = [-1] * N
  39.  
  40. def dfs1(v):
  41.     marked[v] = True
  42.     for u in out[v]:
  43.         if not marked[u]:
  44.             dfs1(u)
  45.     order.append(v)
  46.  
  47. def dfs2(v, c):
  48.     comp[v] = c
  49.     for u in inv[v]:
  50.         if comp[u] == -1:
  51.             dfs2(u, c)
  52.  
  53. # Primer paso: orden topológico por postorden
  54. for v in range(N):
  55.     if not marked[v]:
  56.         dfs1(v)
  57.  
  58. # Segundo paso: recorrer grafo inverso en orden inverso
  59. c = 0
  60. for v in reversed(order):
  61.     if comp[v] == -1:
  62.         dfs2(v, c)
  63.         c += 1
  64.  
  65. # ---------- Verificación de satisfacibilidad ----------
  66. satisfacible = True
  67. for i in range(n):
  68.     if comp[i] == comp[i + n]:
  69.         satisfacible = False
  70.         break
  71.  
  72. if not satisfacible:
  73.     print("La fórmula NO es satisfacible.")
  74. else:
  75.     print("La fórmula es satisfacible.")
  76.     # Determinar asignación
  77.     assignment = [False] * n
  78.     for i in range(n):
  79.         assignment[i] = comp[i] > comp[i + n]
  80.     print("Asignación posible (x1..xn):")
  81.     print(" ".join("1" if val else "0" for val in assignment))
  82.  
Success #stdin #stdout 0.11s 14208KB
comments (?)
stdin 
3 3
1 2
-1 3
-2 -3
stdout 
Ingrese n (variables) y m (cláusulas): La fórmula es satisfacible.
Asignación posible (x1..xn):
1 0 1
https://ideone.com/vwPaWG
language:
Python 3 (python  3.12)
created:
2 days ago
visibility:
public

Share or Embed source code

Discover > Sphere Engine API

The brand new service which powers Ideone!

Discover > IDE Widget

Widget for compiling and running the source code in a web browser!