Essa variação do TQBF ainda está completa no PSPACE?

31

Decidir se uma fórmula booleana quantificada, como

x1x2x3xnφ(x1,x2,,xn),

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 .φx8x3x1,,xn

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.φn

Ele permanece PSPACE completo?

JWM
fonte

Respostas:

35

É um jogo de Satisfação de Restrição Não Ordenada e é completo com PSPACE e foi provado ser completo com PSPACE apenas recentemente ; uma prova pode ser encontrada em:

Lauri Ahlroth e Pekka Orponen, jogos não ordenados de satisfação com restrições . Notas da Palestra em Ciência da Computação Volume 7464, 2012, pp 64-75.

Abstrato:Consideramos jogos de satisfação com restrições para dois jogadores em sistemas de restrições booleanas, nos quais os jogadores se revezam na seleção de uma das variáveis ​​disponíveis e na definição de verdadeiro ou falso, com o objetivo de maximizar (para o Jogador I) ou minimizar (para o Jogador II) o número de restrições satisfeitas. Diferentemente dos jogos padrão de atribuição de variáveis ​​do tipo QBF, não impomos uma ordem na qual as variáveis ​​devem ser jogadas. Isso torna a configuração do jogo mais natural, mas também mais difícil de controlar. Nós fornecemos estratégias de aproximação de fator constante de tempo polinomial para o Player I quando as restrições são funções de paridade ou funções de limite com um limite pequeno em comparação com a aridade das restrições. Além disso, provamos que o problema de determinar se o Player I pode satisfazer todas as restrições está completo no PSPACE, mesmo nessa configuração não ordenada,

A partir do conteúdo:

...
Nosso exemplo genérico de um jogo de satisfação de restrições não ordenadas é o Game on Boolean Formulas ( GBF ). Uma instância deste jogo é dada por um conjunto de m fórmulas booleanas não constantes sobre um conjunto comum de n variáveis . Nós nos referimos às fórmulas em como cláusulas, embora geralmente não exijamos que sejam disjunções. ... Um jogo em prossegue para que a cada turno o jogador se mova selecione uma das variáveis ​​não selecionadas anteriormente e atribua um valor verdadeiro a ela. O jogador I inicia e o jogo termina quando todas as variáveis ​​recebem um valor. Na versão de decisão do GBFX = { x 1 , . . . , x n } C CC={c1,...,cm}X={x1,...,xn}C

C, a questão é se o jogador I tem uma estratégia abrangente de ganhos, pela qual ele pode satisfazer todas as cláusulas, independentemente do jogador II. No caso positivo, dizemos que a instância é satisfatória para GBF. ..

... Teorema 4 : O problema de decidir a satisfação GBF de uma fórmula booleana é PSPACE-complete.

EDIT : Daniel Grier's descobriu que o resultado também foi acertado por Schaefer nos anos 70. Consulte a resposta nesta página para obter a referência (e faça o voto positivo :-). Schaefer provou que o jogo ainda está completo no PSPACE, mesmo que restrito a fórmulas positivas de CNF (ou seja, fórmulas proposicionais na forma conjuntiva normal na qual nenhuma variável negada ocorre) com no máximo 11 variáveis ​​em cada conjunção.

Marzio De Biasi
fonte
27

Também vale a pena notar que esse problema também foi resolvido nos anos 70 por Thomas Schaefer em  Complexidade dos problemas de decisão baseados em jogos finitos de informação perfeita para duas pessoas . De fato, ele mostra um resultado um pouco mais forte, pois o idioma permanece completo no PSPACE, mesmo quando restrito a fórmulas positivas de CNF.

Daniel Grier
fonte
2
Interessante! (Ahlroth e Orponen não sabiam disso? Aliás, eles citam outro artigo de Schaefer: Sobre a complexidade de alguns jogos de informação perfeita para duas pessoas (1978), que contêm os bem conhecidos resultados de completude do PSPACE de Geografia e Node-Kayles). Existe uma cópia gratuita do papel disponível? (o link está além do paywall).
Marzio De Biasi
Infelizmente, acho que não. Lembro-me de uma vez tentando encontrar uma cópia que não estivesse atrás de um paywall por algum tempo, com pouco sucesso.
Daniel Grier
BTW parabéns pelo seu bom resultado na PSPACE-completude dos Poset Games!
Marzio De Biasi
Tanto quanto posso dizer, o artigo de 1978 (Sobre a complexidade de algumas pessoas ...) é a versão em periódico do documento STOC de 1976 (Complexidade dos problemas de decisão ...), que ele cita.
András Salamon
10

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 .

Lutfar Rahman Milu
fonte