Resumo Técnico: Uma Abordagem Baseada em ASP para Resolver Jogos Estocásticos Gerais de Dois Jogadores

Declaração do Problema

Sistemas de Jogo Geral (GGP) visam jogar jogos estratégicos com base em descrições em tempo de execução, sem conhecimento prévio das regras. A Linguagem de Descrição de Jogos (GDL) e sua extensão GDL-II são os formalismos padrão para especificar tais jogos, com o GDL-II suportando aleatoriedade (estocasticidade) e observabilidade parcial. Embora a Programação por Respostas de Conjuntos (ASP) tenha sido aplicada com sucesso à resolução de jogos GDL determinísticos de um e dois jogadores, as estruturas existentes de ASP carecem da capacidade de expressar simultaneamente comportamentos adversariais (minimax) e estocásticos. Consequentemente, há uma lacuna no uso de métodos baseados em ASP para resolver jogos GDL de dois jogadores com turnos que envolvem incerteza.

Metodologia

Os autores propõem uma abordagem inovadora para resolver jogos GDL estocásticos de dois jogadores, introduzindo uma nova linguagem e um solucionador baseado em tradução.

1. Programação por Respostas de Conjuntos Quantificada Estocástica (SQASP)

Para preencher a lacuna entre a ASP e a resolução de jogos estocásticos, o artigo introduz a SQASP, uma linguagem que estende a QASP (ASP Quantificada) com quantificadores de chance.

• Sintaxe: Um programa SQASP assume a forma $Q_1.x_1 \dots Q_n.x_n \ P$, onde $P$ é um programa lógico normal e os quantificadores $Q_i$ podem ser existenciais ($\exists$), universais ($\forall$) ou de chance ($\mathcal{R}_{p}$).
• Semântica: A probabilidade máxima de satisfazer um programa SQASP é definida recursivamente. O quantificador de chance $\mathcal{R}_{p}$ atribui uma probabilidade $p$ a uma variável ser verdadeira, calculando o valor esperado com base nas probabilidades das sub-fórmulas.
• Tradução: Os autores implementam uma ferramenta, sqasp2xssat, que traduz programas SQASP em fórmulas de Satisfatibilidade Estocástica Estendida (XSSAT). A XSSAT estende Fórmulas Booleanas Quantificadas (QBF) com quantificadores de chance. A tradução aproveita ferramentas existentes (como lp2sat) para converter o programa lógico $P$ em uma fórmula CNF $\psi$ cujos modelos correspondem aos modelos estáveis de $P$.

2. Codificação de Jogos GDL em SQASP

A contribuição central é a construção de um programa SQASP $\Psi$ tal que sua probabilidade máxima de satisfatibilidade seja igual à probabilidade máxima de vitória de um jogador $x$ dentro de $n$ passos ($P_x^w(S_0, n)$). A codificação procede em duas fases principais:

• Linha de Base Cooperativa: Primeiro, um programa lógico $P_c$ é construído assumindo que todos os jogadores (incluindo o oponente $o$ e o jogador aleatório $r$) cooperam para alcançar um estado terminal onde $x$ vence. Isso garante uma progressão válida do jogo, término dentro de $n$ passos e a realização do estado objetivo.
• Modelagem Adversarial e Estocástica: O programa é então estendido para capturar os comportamentos específicos do oponente e do ambiente:
  • Jogador Adversarial ($o$): Modelado usando quantificação universal ($\forall$) sobre variáveis de decisão (dec_o). Isso força o solucionador a considerar o pior cenário possível, onde o oponente minimiza a probabilidade de vitória de $x$. A codificação usa uma representação logarítmica de ações para reduzir o número de regras.
  • Jogador Estocástico ($r$): Modelado usando quantificadores de chance ($\mathcal{R}_{1/i}$). A codificação garante que, se o jogo não tiver terminado, o jogador aleatório selecione exatamente uma ação legal uniformemente entre as jogadas legais disponíveis. Isso é alcançado contando as ações legais e aplicando restrições de probabilidade às variáveis de decisão (dec_r).

3. Estratégias de Quantificação

O artigo investiga duas estratégias de quantificação para a fórmula XSSAT resultante:

• Método de Linha de Base ($Q_b$): Todos os átomos não de escolha (por exemplo, legal, terminal) são colocados no bloco existencial mais interno, seguindo uma ordem temporal estrita dos átomos de escolha.
• Método Baseado em Dependência ($Q_d$): Inspirado em técnicas para jogos determinísticos, este método desloca átomos não de escolha para aparecerem o mais cedo possível no prefixo de quantificadores, imediatamente após os átomos de escolha dos quais dependem. Isso visa reduzir o espaço de busca fixando valores como legal antes de ramificar sobre does.

Contribuições Principais

1. Primeiro Solucionador Baseado em ASP para GDL Estocástico: O artigo apresenta a primeira abordagem para resolver jogos GDL de dois jogadores, estocásticos e com turnos, usando ASP.
2. Linguagem SQASP: A introdução da Programação por Respostas de Conjuntos Quantificada Estocástica, que unifica o raciocínio adversarial e estocástico dentro de um framework de programação lógica.
3. Solucionador Baseado em Tradução: O desenvolvimento do sqasp2xssat, que converte programas SQASP em fórmulas XSSAT, permitindo o uso de solucionadores XSSAT existentes (especificamente o SharpSSAT) para resolução de jogos.
4. Correção Teórica: Os autores fornecem provas formais (Teoremas 2 e 3) estabelecendo a equivalência entre a probabilidade máxima de vitória no jogo GDL e a probabilidade máxima de satisfatibilidade da fórmula SQASP/XSSAT gerada.

Resultados Experimentais

Os autores avaliaram sua abordagem em variações estocásticas de Jogo da Velha, Conecta-4 e Nim, comparando o método baseado em SQASP (usando tanto a quantificação $Q_b$ quanto $Q_d$) com um solucionador Minimax Esperado (EMM) de busca para frente.

• Desempenho: A abordagem baseada em ASP é competitiva com a busca para frente em jogos estocásticos pequenos. Em muitos casos (por exemplo, Jogo da Velha, Conecta-3), o solucionador ASP calcula probabilidades de vitória comparáveis ao EMM, frequentemente dentro de prazos similares.
• Deslocamento de Quantificadores: Surpreendentemente, a quantificação baseada em dependência ($Q_d$) não produziu melhorias significativas de desempenho sobre a linha de base ($Q_b$) ao usar o solucionador SharpSSAT. Os autores atribuem isso ao mecanismo interno de propagação de unidades do SharpSSAT, que pode derivar valores de átomos (como legal) independentemente da ordem dos quantificadores, mitigando efetivamente a necessidade de deslocamento explícito.
• Limites de Escalabilidade: A abordagem luta com espaços de estado maiores, como Nim Estocástico com tamanhos grandes de pilha. As fórmulas XSSAT resultantes tornam-se grandes demais (mais de um milhão de cláusulas) para os solucionadores atuais lidarem com eficiência, enquanto o EMM escala bem devido à programação dinâmica e tabelas de transposição.

Significado e Alegações

O artigo afirma que a abordagem proposta baseada em ASP fornece uma alternativa viável para avaliação de finais de jogo em sistemas de Jogo Geral. Ao estender a aplicação bem-sucedida da ASP em jogos determinísticos para o domínio estocástico, o trabalho demonstra que a programação lógica pode lidar efetivamente com incerteza e raciocínio adversarial.

Os autores observam modestamente que, embora a abordagem não domine a busca para frente em todos os casos (particularmente para jogos com espaços de estado muito grandes ou estruturas específicas como Nim), ela generaliza com sucesso resultados anteriores para jogos determinísticos para jogos estocásticos. Eles identificam a extensão para observabilidade parcial (por exemplo, Poker, Krieg-Jogo da Velha) como uma direção crítica para trabalhos futuros, reconhecendo que o método atual é limitado a jogos de informação perfeita.