Decidir se uma fórmula booleana quantificada, como
sempre avalia como verdadeiro é um problema clássico completo do PSPACE. Isso pode ser visto como um jogo entre dois jogadores, com movimentos alternados. O primeiro jogador decide o valor de verdade das variáveis de número ímpar e o segundo jogador decide o valor de verdade das variáveis de número par. O primeiro jogador tenta tornar falso e o segundo jogador tenta torná-lo verdadeiro. A decisão de quem tem uma estratégia vencedora é completa no PSPACE.
Estou pensando em um problema semelhante com dois jogadores, um tentando tornar uma fórmula booleana verdadeira e a outra tentando torná-la falsa. A diferença é que, em um movimento, um jogador pode escolher uma variável e um valor de verdade para ele (por exemplo, como o primeiro movimento, o jogador 1 pode decidir definir como verdadeiro e, no próximo movimento, o jogador 2 pode decidir para definir como false). Isso significa que os jogadores podem decidir quais das variáveis (daquelas que ainda não receberam um valor de verdade) querem atribuir um valor de verdade, em vez de terem que jogar o jogo na ordem .
O problema recebe uma fórmula booleana em variáveis para decidir se o jogador um (tentando torná-lo falso) ou o jogador dois (tentando torná-lo verdadeiro) tem uma estratégia vencedora. Esse problema ainda está claramente no PSPACE, pois a árvore do jogo tem profundidade linear.
Ele permanece PSPACE completo?
Provamos que este jogo é completo para o PSPACE para 5-CNFs, mas possui o algoritmo Linear Time para 2-CNFs. O melhor resultado anterior foram os 6-CNFs de Ahlroth e Orponen.
Você pode encontrar o documento da conferência no ISAAC 2018 .
Atualização: 16 de novembro de 2019
Provamos que o jogo é tratável para 3-CNFs sob algumas restrições aos 3-CNFs. Também conjeturamos radicalmente que este jogo também é tratável sem restrições aos 3-CNFs. Você pode encontrar a versão inicial no ECCC .
fonte