Conecta 4 - SAT

Question

Mi pregunta es sobre cómo el juego de Hasbro Connect4 puede ser visto como un problema de SAT.

Mi suposición inicial es que en realidad sería QSAT, y que el "problema" sería algo parecido a: "¿Existe un conjunto de giros blancos/negros de tal manera que ocurra X?" donde X es alguna condición en el tablero.

Supongo que incluso se podría especificar que X tiene que ser alcanzado después de un cierto número de turnos n.

Cualquier idea sobre la codificación de connect4 como un problema Q/SAT o cualquier idea sobre preguntas interesantes que se puedan plantear al respecto son bienvenidas. ¡Muchas gracias!

Como referencia, si es necesario: Tesis sobre Connect4 desde la perspectiva de la IA

Answer 1

Mi suposición inicial es que en realidad sería QSAT, y que el "problema" sería algo parecido a: "¿Existe un conjunto de giros blancos/negros de tal manera que ocurra X?" donde X es alguna condición en el tablero.

Los cuantificadores no son necesarios para codificar este juego. En primer lugar, se construye una instancia SAT cuyas asignaciones satisfactorias codifican las posiciones legales del tablero después del primer movimiento de una partida de Conecta 4. A continuación, se añaden cláusulas y nuevas variables cuyas asignaciones satisfactorias codifican las posiciones legales del tablero después de un segundo movimiento dado un primer movimiento legal. Repita este proceso, en efecto, creando una muñeca Matrioshka de instancias, para cubrir el número de capas que desea permitir que el solucionador SAT explore. Añada cláusulas para reconocer una partida ganada por cualquiera de los dos bandos que induzcan un valor de verdad en una variable selectora especial que satisfaga todas las cláusulas y cortocircuite la búsqueda.