Fórmula booliana completamente quantificada

Em teoria da complexidade computacional, uma linguagem TQBF é uma linguagem formal consistindo de fórmulas booleanas completamente quantificadas. Uma fórmula booleana (completamente) quantificada é uma fórmula em lógica proposicional quantificada onde cada variável é quantificada (ou limitada), usando tanto quantificadores existenciais quanto universais no início da sentença. Tal fórmula é equivalente a tanto verdadeiro ou falso (desde que não existam variáveis livres). Se tal fórmula é avaliada como verdadeira, então esta fórmula é uma linguagem TQBF. Também conhecida como QSAT (Quantified SAT).

Visão Geral

Em teoria da complexidade computacional, uma fórmula booleana quantificada (FBQ) é uma generalização do problema da satisfatibilidade booleana na qual ambos quantificadores existenciais e quantificares universais podem ser aplicados para cada variável. Colocado de outra maneira, é perguntado se uma sentença quantificada formada sobre um conjunto de variáveis booleanas é verdadeiro ou falso. Por exemplo, a instância seguinte é uma FBQ:

$\forall x\ \exists y\ \exists z\ ((x\lor z)\land y)$

FBQ é um problema canônico completo para PSPACE, a classe dos problemas solúveis deterministicamente ou não-deterministicamente por uma máquina de Turing em espaço polinomial e em tempo ilimitado. Dado uma fórmula na forma de uma árvore sintática abstrata, o problema pode ser resolvido facilmente por um conjunto mutualmente recursivo de procedimentos que avaliam a fórmula. Tal algoritmo usa espaço proporcional a altura da árvore, que é linear no pior caso, mas utiliza tempo exponencial no número de quantificadores.

Dado que MA ⊊ PSPACE, que é amplamente aceito, FBQ não pode ser solúvel, nem dado uma solução, pode ser verificado, tanto em tempo polinomial determinístico ou probabilístico (de fato, diferentemente do problema da satisfatibilidade, não existe nenhuma maneira conhecida de especificar uma solução sucinta). É trivial resolver utilizando uma máquina de Turing alternada em tempo linear, o que não é nenhuma surpresa já que AP = PSPACE, onde AP é a classe dos problemas que as máquinas alternadas podem resolver em tempo polinomial.  

Quando o resultado pioneiro IP = PSPACE foi mostrado, este foi feito exibindo um sistema de prova interativo que poderia resolver FBQ solucionando uma aritmética particular do problema .

Fórmulas FBQ possuem um número útil de formas canônicas. Por exemplo, pode ser mostrado que existe uma redução em tempo polinomial de muitos para um que removerá todos os quantificadores do início da fórmula e os tornam alternados entre quantificadores universais e existenciais. Existe uma outra redução que é provada ser útil na prova IP = PSPACE onde não mais que um quantificador universal é colocado entre cada uso da variável e o quantificador liga esta variável. Isto foi crítico limitando o número de produtos de certas sub-expressões da aritmetização.  

Forma normal prenex 

Uma fórmula totalmente quantificada pode assumir uma forma bem específica chamada forma normal prenex.  Esta forma é constituída de duas partes básicas: uma parte contendo somente quantificadores e uma parte contendo uma fórmula booleana não quantificada, normalmente denotada por $\displaystyle \phi$. Se existem $\displaystyle n$ variáveis booleanas, a fórmula inteira pode ser escrita como

$\displaystyle \exists x_{1}\forall x_{2}\exists x_{3}\cdots Q_{n}x_{n}\phi (x_{1},x_{2},x_{3},\dots ,x_{n})$

onde cada variável cai dentro do escopo de algum quantificador. Introduzindo variáveis artificiais, qualquer fórmula na forma normal prenex pode ser convertida em uma sentença onde quantificadores existenciais e universais se alternam. Utilizando a variável artificial $\displaystyle y_{1}$,

$\displaystyle \exists x_{1}\exists x_{2}\phi (x_{1},x_{2})\quad \mapsto \quad \exists x_{1}\forall y_{1}\exists x_{2}\phi (x_{1},x_{2})$

A segunda sentença tem o mesmo valor verdade mas segue a restrição da sintaxe. Assumir que fórmulas booleanas completamente quantificadas estão na forma normal prenex é uma característica frequente em provas. 

Solucionando

Existe um algoritmo recursive simples para determinar se uma FBQ é uma TQBF (i.e. é verdadeira). Dado alguma FBQ

$Q_{1}x_{1}Q_{2}x_{2}\cdots Q_{n}x_{n}\phi (x_{1},x_{2},\dots ,x_{n}).$

Se a fórmula não contém quantificadores, retorna-se apenas a fórmula. Caso contrário, partindo do primeiro quantificador and verificando ambos possíveis valores para a primeira variável:

$A=Q_{2}x_{2}\cdots Q_{n}x_{n}\phi (0,x_{2},\dots ,x_{n}),$

$B=Q_{2}x_{2}\cdots Q_{n}x_{n}\phi (1,x_{2},\dots ,x_{n}).$

Se $Q_{1}=\exists$, então retorne $A\lor B$. Se $Q_{1}=\forall$, então retorne $A\land B$.

Quão rápido este algoritmo roda? Para cada quantificador na FBQ inicial, o algoritmo toma duas chamadas recursivas em apenas um subproblema menor. Isto faz com que o algoritmo rode em tempo exponencial O(2ⁿ).

Quanto espaço esse algoritmo usa? Dentro de cada chamada do algoritmo, ele precisa os resultados intermediários da computação de A e B. Cada chamada recursiva parte um quantificador, então a profundidade total recursiva é linear em termos do número de quantificadores.  As fórmulas que carecem de quantificadores podem ser avaliados no espaço logarítmico em função do número de variáveis.A FBQ inicial foi totalmente quantificada, então existe no mínimo tantos quantificadores quanto variáveis. Dessa forma, este algoritmo usa O(n + log n) = O(n) espaço. Isto faz com que a linguagem TQBF seja parte da classe PSPACE.

PSPACE-completude

A linguagem TBQF se apresenta para a teoria da complexidade como um problema PSPACE-completo canônico. Dizer que uma linguagem está em PSPACE-completo significa dizer que a linguagem também está em PSPACE-difícil. O algoritmo abaixo mostra que TQBF está em PSPACE. Mostrando que TQBF é PSPACE-difícil requer mostrar que qualquer linguagem pertencente a classe de complexidade de PSPACE pode ser reduzida a TQBF em tempo polinomial. I.e.,

$\forall L\in {\textrm {PSPACE}},L\leq _{p}{\textrm {TQBF}}.$

Significa que, para uma linguagem L em PSPACE, se uma entrada $x$ está em L, ela pode ser decidida verificando se $f(x)$ está em TQBF, para alguma função $f$ que roda em tempo polinomial (relativa ao tamanho da entrada). Simbolicamente,

$x\in L\iff f(x)\in {\textrm {TQBF}}.$

Provar que TQBF está em PSPACE-difícil, requer uma especificação de $f$.

Então, suponha que L é uma linguagem em PSPACE. Isto significa que L pode ser decidida por uma Máquina de Turing deterministica em espaço polinomial. Isto é muito importante para a redução de L para TQBF, pois as configurações de tails Máquinas de Turing podem ser representadas por fórmulas booleanas, com variáveis booleanas representando o estado da máquina bem como o conteúdo de cada célula na fita da Máquina de Turing, com a posição da cabeça da Máquina de Turing decodificada na fórmula pela ordenação da fórmula. Em particular, esta redução usará as variáveis $c_{1}$ e $c_{2}$, que representam duas possíveis configurações da Máquina de Turing deterministica para L, e um número natural t, construindo uma FB $\phi _{c_{1},c_{2},t}$ que resulta em verdadeiro se e somente se a Máquina de Turing deterministica para L pode ir da configuração decodificada em  $c_{1}$ para a configuração codificada em $c_{2}$ em não mais que t passos. A função $f$, então, irá construir a partir da Máquina de Turing deterministica para L uma FBQ $\phi _{c_{start},c_{accept},T}$, onde $c_{start}$ é a configuração inicial da Máquina de Turing deterministica, $c_{accept}$ é a configuração de aceitação da Máquina de Turing deterministica e T é o número máximo de passos que a Máquina de Turing deterministica pode precisar para mover de uma configuração para outra. Sabemos que  T = O(exp(n)), onde n é o tamanho da entrada, porque ele limita o número total de possíveis configurações da Máquina de Turing deterministica. Claro, a Máquina de Turing  não se pode tomar mais passos do que há configurações possíveis para alcançar$c_{\mathrm {accept} }$ ao menos que ela entre em loop, e nesse caso ela nunca mais alcançar $c_{\mathrm {accept} }$ de qualquer forma.

Nesse estágio da prova, nós já temos reduzido a questão de se uma dada entrada $w$ (decodificada, claro, em $c_{start}$) está em L para a questão de se a FBQ $\phi _{c_{start},c_{accept},T}$, i.e., $f(w)$, está em TQBF. O restante dessa prova prova que $f$ pode ser computada em tempo polinomial.

Para $t=1$, a computação de $\phi _{c_{1},c_{2},t}$ é simples - quer uma das configurações mude para o outra em um passo ou não. Uma vez que a máquina de Turing que a nossa fórmula representa é determinística, este não apresenta nenhum problema.

Para $t>1$, a computacão de $\phi _{c_{1},c_{2},t}$ envolve uma avaliação recursiva, procurando por um conhecido "ponto do meio" $m_{1}$. Neste caso, nós rescrevemos a fórmula como segue:

$\phi _{c_{1},c_{2},t}=\exists m_{1}(\phi _{c_{1},m_{1},\lceil t/2\rceil }\wedge \phi _{m_{1},c_{2},\lceil t/2\rceil }).$

Isto converte a questão de se $c_{1}$ pode alcançar $c_{2}$ em t passos para a questão de se $c_{1}$ alcança um ponto do meio $m_{1}$ em $t/2$ passos, que por si só alcança $c_{2}$ em $t/2$ passos. A resposta a esta última questão, claro, dá a resposta à primeira.

Agora, t só é limitada por T, que é exponencial (e assim não polinomial) no comprimento da entrada.Além disso, cada camada recursiva duplica praticamente o comprimento da fórmula. (A variável $m_{1}$ é somente um ponto no meio - para um t maior, existem mais paradas ao longo do caminho, por assim dizer).  Assim, o tempo necessário para avaliar recursivamente $\phi _{c_{1},c_{2},t}$ desta maneira podia ser exponencial assim, simplesmente porque a fórmula poderia tornar-se exponencialmente grande. Este problema é resolvido por quantificando universalmente usando as variáveis $c_{3}$ e $c_{4}$ o longo dos pares de configuração (e.g., $\{(c_{1},m_{1}),(m_{1},c_{2})\}$), que impede que o comprimento da fórmula se expanda, devido às camadas recursivas. Isso produz a seguinte interpretação de $\phi _{c_{1},c_{2},t}$:

$\phi _{c_{1},c_{2},t}=\exists m_{1}\forall (c_{3},c_{4})\in \{(c_{1},m_{1}),(m_{1},c_{2})\}(\phi _{c_{3},c_{4},\lceil t/2\rceil }).$

Esta versão da fórmula pode, efetivamente, ser calculado em tempo polinomial, uma vez que qualquer instância pode ser calculada em tempo polinomial. O par ordenado quantificado universal simplesmente nos diz que quaisquer escolha de $(c_{3},c_{4})$ é feita, $\phi _{c_{1},c_{2},t}\iff \phi _{c_{3},c_{4},\lceil t/2\rceil }$.

Assim, $\forall L\in {\textrm {PSPACE}},L\leq _{p}{\textrm {TQBF}}$, então TQBF é PSPACE-hard. Juntamente com o resultado acima, que TQBF está em PSPACE, isso completa a prova que TQBF é uma linguagem PSPACE-completa.

(Esta prova segue Sipser 2006 pp. 310–313 em todos os fundamentos. Papadimitriou 1994 também inclui uma prova.)

Miscellany

• Uma subproblema importante em TQBF é o problema de satisfatibilidade booleana. Neste problema, deseja saber se uma determinada fórmula booleana $\phi$ pode se tornar verdadeira com algum atribuição variáveis. Este é equivalente ao TQBF usando quantificadores existenciais únicos:

$\exists x_{1}\cdots \exists x_{n}\phi (x_{1},\ldots ,x_{n})$

Este é também um exemplo do resultado maior NP $\subseteq$ PSPACE que resulta diretamente da observação de que um verificador de tempo polinomial para provar que uma linguagem é aceita por uma MTM (Máquina de Turing não-determinística) requer espaço polinomial para armazenar a prova.

• Qualquer classe na hierarquia polinomial tem TQBF como um problema difícil. Em outras palavras, para a classe que compreende todas as linguagens L para o qual não existe uma Máquina de Turing de tempo polinomial, um verificador, tal que para todo x como entrada e alguma constante i,

$x\in L\Leftrightarrow \exists y_{1}\forall y_{2}\cdots Q_{i}y_{i}\ V(x,y_{1},y_{2},\dots ,y_{i})\ =\ 1$

na qual tem uma FBQ específica que é formulada como sendo 

$\exists \phi$ tal que $\exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1$

onde os ${\vec {x_{i}}}$'s são vetores de variáveis booleanas.

• É importante notar que, enquanto em TQBF a linguagem é definida como a coleção de fórmulas quantificadas booleanas verdadeiras, a TQBF abreviatura é frequentemente utilizado (mesmo neste artigo) para representar uma fórmula booleana totalmente quantificados, muitas vezes chamado simplesmente de um FBQ (fórmula booleana quantificada, entendida como "totalmente" ou "totalmente" quantificado). É importante fazer a distinção entre os dois contextualmente usos do TQBF abreviatura na leitura da literatura.
• Uma TQBF pode ser pensada como um jogo jogado entre dois jogadores, com movimentos alternados. Existencialmente variáveis quantificadas são equivalentes à noção de que um movimento está disponível para um jogador de cada vez. Universalmente variáveis quantificadas significam que o resultado do jogo não depende do movimento de um jogador faz naquele turno. Além disso, uma TQBF cujo primeiro quantificador é existencial corresponde a um jogo de fórmula em que o primeiro jogador tem uma estratégia vencedora.
• Para que uma fórmula quantificada TQBF esteja em 2-CNF pode ser resolvido em tempo linear, por um algoritmo envolvendo forte análise de conectividade de seu gráfico. O problema 2-satisfatibilidade é um caso especial de TQBF para estas fórmulas, em que cada quantificador é existencial.
• Existe um tratamento sistemático para versões restritas de fórmulas booleanas quantificadas proposto em um paper expositivo por Hubie Chen.

Notas e referências

Referências

• Fortnow & Homer (2003) provides some historical background for PSPACE and TQBF.
• Zhang (2003) provides some historical background of Boolean formulas.
• Arora, Sanjeev. (2001). COS 522: Computational Complexity. Lecture Notes, Princeton University. Retrieved October 10, 2005.
• Fortnow, Lance & Steve Homer. (2003, June). A short history of computational complexity. The Computational Complexity Column, 80. Retrieved October 9, 2005.
• Papadimitriou, C. H. (1994). Computational Complexity. Reading: Addison-Wesley.
• Sipser, Michael. (2006). Introduction to the Theory of Computation. Boston: Thomson Course Technology.
• Zhang, Lintao. (2003). Searching for truth: Techniques for satisfiability of boolean formulas. Retrieved October 10, 2005.

Ver também

• Teorema de Cook-Levin, afirmando que SAT é NP-completo

Ligações externas

• Biblioteca de fórmulas booleanas quantificadas (em inglês) (QBFLIB)
• DepQBF - um buscador baseado em fórmula booleana quantificada (em inglês)
• International Workshop on Quantified Boolean Formulas