Resumen Técnico: Un Enfoque basado en ASP para Resolver Juegos Generales de Dos Jugadores Estocásticos

Declaración del Problema

Los sistemas de Juego General (GGP) tienen como objetivo jugar juegos estratégicos basándose en descripciones en tiempo de ejecución sin conocimiento previo de las reglas. El Lenguaje de Descripción de Juegos (GDL) y su extensión GDL-II son los formalismos estándar para especificar dichos juegos, siendo GDL-II el que soporta aleatoriedad (estocasticidad) y observabilidad parcial. Si bien la Programación de Conjuntos de Respuesta (ASP) se ha aplicado con éxito a la resolución de juegos GDL deterministas de uno y dos jugadores, los marcos ASP existentes carecen de la capacidad para expresar simultáneamente comportamientos adversarios (minimax) y estocásticos. En consecuencia, existe una brecha en el uso de métodos basados en ASP para resolver juegos GDL de dos jugadores con turnos que involucran incertidumbre.

Metodología

Los autores proponen un enfoque novedoso para resolver juegos GDL estocásticos de dos jugadores mediante la introducción de un nuevo lenguaje y un solucionador basado en traducción.

1. Programación de Conjuntos de Respuesta Cuantificada Estocástica (SQASP)

Para cerrar la brecha entre ASP y la resolución de juegos estocásticos, el artículo introduce SQASP, un lenguaje que extiende QASP (ASP Cuantificado) con cuantificadores de azar.

• Sintaxis: Un programa SQASP toma la forma $Q_1.x_1 \dots Q_n.x_n \ P$, donde $P$ es un programa de lógica normal y los cuantificadores $Q_i$ pueden ser existenciales ($\exists$), universales ($\forall$) o de azar ($\mathcal{R}_{p}$).
• Semántica: La probabilidad máxima de satisfacer un programa SQASP se define recursivamente. El cuantificador de azar $\mathcal{R}_{p}$ asigna una probabilidad $p$ a que una variable sea verdadera, calculando el valor esperado basándose en las probabilidades de las subfórmulas.
• Traducción: Los autores implementan una herramienta, sqasp2xssat, que traduce programas SQASP a fórmulas de Satisfacibilidad Estocástica Extendida (XSSAT). XSSAT extiende las Fórmulas Booleanas Cuantificadas (QBF) con cuantificadores de azar. La traducción aprovecha herramientas existentes (como lp2sat) para convertir el programa de lógica $P$ en una fórmula CNF $\psi$ cuyos modelos corresponden a los modelos estables de $P$.

2. Codificación de Juegos GDL en SQASP

La contribución central es la construcción de un programa SQASP $\Psi$ tal que su probabilidad máxima de satisfacibilidad sea igual a la probabilidad máxima de victoria de un jugador $x$ en $n$ pasos ($P_x^w(S_0, n)$). La codificación procede en dos fases principales:

• Línea Base Cooperativa: Primero, se construye un programa de lógica $P_c$ asumiendo que todos los jugadores (incluido el oponente $o$ y el jugador aleatorio $r$) cooperan para alcanzar un estado terminal donde $x$ gana. Esto asegura una progresión válida del juego, la terminación dentro de $n$ pasos y el logro del estado objetivo.
• Modelado Adversario y Estocástico: Luego, el programa se extiende para capturar los comportamientos específicos del oponente y del entorno:
  • Jugador Adversario ($o$): Se modela utilizando cuantificación universal ($\forall$) sobre las variables de decisión (dec_o). Esto obliga al solucionador a considerar el peor escenario posible donde el oponente minimiza la probabilidad de victoria de $x$. La codificación utiliza una representación logarítmica de las acciones para reducir el número de reglas.
  • Jugador Estocástico ($r$): Se modela utilizando cuantificadores de azar ($\mathcal{R}_{1/i}$). La codificación asegura que, si el juego no ha terminado, el jugador aleatorio seleccione exactamente una acción legal uniformemente entre los movimientos legales disponibles. Esto se logra contando las acciones legales y aplicando restricciones de probabilidad a las variables de decisión (dec_r).

3. Estrategias de Cuantificación

El artículo investiga dos estrategias de cuantificación para la fórmula XSSAT resultante:

• Método de Línea Base ($Q_b$): Todos los átomos no de elección (por ejemplo, legal, terminal) se colocan en el bloque existencial más interno, siguiendo un orden temporal estricto de los átomos de elección.
• Método Basado en Dependencias ($Q_d$): Inspirado en técnicas para juegos deterministas, este método desplaza los átomos no de elección para que aparezcan lo antes posible en el prefijo de cuantificadores, inmediatamente después de los átomos de elección de los que dependen. Esto tiene como objetivo reducir el espacio de búsqueda fijando valores como legal antes de ramificar sobre does.

Contribuciones Clave

1. Primer Solucionador basado en ASP para GDL Estocástico: El artículo presenta el primer enfoque para resolver juegos GDL de dos jugadores, estocásticos y con turnos utilizando ASP.
2. Lenguaje SQASP: La introducción de la Programación de Conjuntos de Respuesta Cuantificada Estocástica, que unifica el razonamiento adversario y estocástico dentro de un marco de programación lógica.
3. Solucionador Basado en Traducción: El desarrollo de sqasp2xssat, que convierte programas SQASP en fórmulas XSSAT, permitiendo el uso de solucionadores XSSAT existentes (específicamente SharpSSAT) para la resolución de juegos.
4. Corrección Teórica: Los autores proporcionan pruebas formales (Teoremas 2 y 3) que establecen la equivalencia entre la probabilidad máxima de victoria en el juego GDL y la probabilidad máxima de satisfacibilidad de la fórmula SQASP/XSSAT generada.

Resultados Experimentales

Los autores evaluaron su enfoque en variaciones estocásticas de Tres en Raya, Conecta-4 y Nim, comparando el método basado en SQASP (utilizando tanto la cuantificación $Q_b$ como $Q_d$) contra un solucionador de Búsqueda Hacia Adelante Minimax Esperado (EMM).

• Rendimiento: El enfoque basado en ASP es competitivo con la búsqueda hacia adelante en juegos estocásticos pequeños. En muchos casos (por ejemplo, Tres en Raya, Conecta-3), el solucionador ASP calcula probabilidades de victoria comparables a las de EMM, a menudo en marcos de tiempo similares.
• Desplazamiento de Cuantificadores: Sorprendentemente, la cuantificación basada en dependencias ($Q_d$) no produjo mejoras significativas de rendimiento sobre la línea base ($Q_b$) al utilizar el solucionador SharpSSAT. Los autores atribuyen esto al mecanismo interno de propagación de unidades de SharpSSAT, que puede derivar valores de átomos (como legal) independientemente del orden de los cuantificadores, mitigando efectivamente la necesidad de un desplazamiento explícito.
• Límites de Escalabilidad: El enfoque lucha con espacios de estado más grandes, como Nim Estocástico con tamaños de pila grandes. Las fórmulas XSSAT resultantes se vuelven demasiado grandes (más de un millón de cláusulas) para que los solucionadores actuales las manejen de manera eficiente, mientras que EMM escala bien debido a la programación dinámica y las tablas de transposición.

Significado y Afirmaciones

El artículo afirma que el enfoque basado en ASP propuesto proporciona una alternativa viable para la evaluación de finales de juego en sistemas de Juego General. Al extender la aplicación exitosa de ASP a juegos deterministas hacia el dominio estocástico, el trabajo demuestra que la programación lógica puede manejar eficazmente la incertidumbre y el razonamiento adversario.

Los autores notan modestamente que, si bien el enfoque no domina a la búsqueda hacia adelante en todos los casos (particularmente para juegos con espacios de estado muy grandes o estructuras específicas como Nim), generaliza con éxito los resultados anteriores para juegos deterministas a los estocásticos. Identifican la extensión a la observabilidad parcial (por ejemplo, Poker, Krieg-Tres en Raya) como una dirección crítica para el trabajo futuro, reconociendo que el método actual está limitado a juegos de información perfecta.