Fórmula booliana totalmente quantificada

Uma fórmula booleana totalmente quantificada, na teoria da complexidade computacional, é uma fórmula em lógica proposicional na qual cada variável é quantificada (ou vinculada) utilizando o quantificador universal ou existencial no início da expressão. A linguagem TBQF é uma linguagem formal que consiste na quantificação exata dessas fórmulas booleanas. Tal fórmula resulta em um valor verdadeiro ou falso, visto que não contém variáveis livres. Se a fórmula é avaliada como verdadeira, então ela pertence à linguagem TBQF. Esta linguagem é também referida como QSAT (SAT Quantificada).

Visão geral

Na teoria da complexidade computacional, o problema da quantificação da fórmula booleana (QBF) é uma generalização do problema de satisfatibilidade booleana em que tanto quantificadores existenciais quanto quantificadores universais podem ser aplicados a cada variável. Dito de outra forma, pergunta-se se uma fórmula sentencial quantificada sobre um conjunto de variáveis booleanas é verdadeira ou falsa. Por exemplo, a instância a seguir é um exemplo de QBF:

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

QBF é o problema canônico completo para PSPACE, a classe de problemas solúveis por uma Máquina de Turing determinística ou não determinística no espaço polinomial e tempo ilimitado. Dada uma fórmula na árvore de sintaxe abstrata (AST), o problema pode ser resolvido por um conjunto de procedimentos mutuamente recursivos que avalia a fórmula. Tal algoritmo usa o espaço proporcional à altura da árvore, que é linear no pior caso, mas usa tempo exponencial no número de quantificadores.

Desde que MA ⊂ PSPACE, o que se acredita amplamente, QBF não pode ser resolvido, nem mesmo uma solução dada pode ser verificada em qualquer tempo determinístico e probabilístico polinomial (de fato, ao contrário do problema da satisfatibilidade, não há qualquer maneira conhecida para especificar uma solução de forma sucinta). É trivial resolver usando uma Máquina de Turing Alternada em tempo linear, o que não é nenhuma surpresa, uma vez que, de facto, AP = PSPACE, onde AP é a classe de problemas que podem ser resolvidos por máquinas alternadas em tempo polinomial.

Quando o resultado seminal IP = PSPACE foi mostrado (veja sistema de prova interativa), foi feito para exibir um sistema de prova interativa que poderia resolver QBF resolvendo uma aritmetização particular do problema.

As fórmulas em QBF têm uma série de formas canônicas úteis. Por exemplo, pode-se mostrar que há uma redução muitos-para-um em tempo polinomial que moverá todos os quantificadores para frente da fórmula e então alterná-los entre quantificadores universais e existenciais. Há outra redução que se prova útil no contexto de IP = PSPACE, onde não mais que um quantificador universal é colocado entre o uso de cada variável e a ligação entre o quantificador e a variável. Isso foi fundamental no limite do número de produtos em certas subexpressões da aritmetização.

Forma normal prenex

Uma fórmula booleana totalmente quantificada pode ser considerada como tendo uma forma muito específica, chamada forma normal prenex. Ela tem duas partes básicas: uma porção contendo quantificadores e apenas uma parte contendo uma fórmula booleana não quantificada, normalmente denotada como φ. Se existem n variáveis booleanas, toda a fórmula pode ser escrita como:

$\exists x_{1}\forall x_{2}\exists x1...Q_{n\times n}\Phi (x_{1},x_{2},x_{3},...x_{n})$

onde cada variável é abrangida pelo escopo de algum quantificador. Com a introdução de variáveis fictícias, qualquer fórmula na forma normal prenex pode ser convertida em uma sentença onde quantificadores existenciais e universais alternam. Utilizando a variável fictícia "y1":

$\exists x_{1}\exists x_{2}\Phi (x_{1},x_{2})\Leftrightarrow \exists x_{1}\forall y_{1}\exists x_{2}\Phi (x_{1},x_{2})$

A segunda sentença possui o mesmo valor verdadeiro, mas segue a sintaxe restrita. Assumindo que a conversão de fórmulas booleanas totalmente quantificadas para a forma normal prenex seja uma característica comum de provas.

Resolvendo

Há um simples algoritmo para verificar se um TBQF é verdade. Dadas algumas QBF:

$Q_{1}x_{1}Q_{2}x_{2}...Q_{n}x_{n}\Phi (x_{1},x_{2},...,x_{n})$

Se a fórmula não contém quantificadores, podemos simplesmente voltar à fórmula. Caso contrário, tiramos o primeiro quantificador e verificamos os valores possíveis para a primeira variável:

$A=Q_{2}x_{2}...Q_{n}x_{n}\Phi (0,x_{2},...,x_{n})$,

$B=Q_{2}x_{2}...Q_{n}x_{n}\Phi (1,x_{2},...,x_{n})$.

Se Q₁ = ∃, então retorne A ∨ B. Se Q₁ = ∀, então retorne A ∧ B.

Quão rápido executa esse algoritmo? Para cada quantificador na QBF inicial, o algoritmo faz duas chamadas recursivas em problemas linearmente menores. Isso dá ao algoritmo um tempo de execução exponencial O(2^n).

Quanto de espaço esse algoritmo usa? Em cada chamada do algoritmo, é necessário armazenar os resultados intermediários da computação de A e B. Cada chamada recursiva retira um quantificador, e apenas a profundidade recursiva é linear no número de quantificadores. Fórmulas em que faltam quantificadores podem ser avaliadas no espaço logarítmico no número de variáveis. A QBF inicial foi totalmente quantificada, então há tantos quantificadores quanto variáveis. Assim, o algoritmo usa espaço O(n + log n) = O(n). Isso faz com que TQBF seja parte da classe de complexidade PSPACE.

PSPACE completude

A linguagem TQBF serve na teoria da complexidade como a canônica do problema PSPACE-completo. Ser PSPACE-completo significa que uma linguagem está em PSPACE e que a linguagem também é PSPACE-difícil. O algoritmo acima mostra que TQBF está em PSPACE. Mostrar que uma linguagem está em PSPACE-difícil requer mostrar que qualquer linguagem na classe de complexidade PSPACE pode ser reduzida, em tempo polinomial, a TQBF. Em outras palavras,

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

Isso significa que, para uma linguagem LSPACE, se uma linguagem x está em L, pode ser decidida verificando se f(x) está na TQBF, para alguma função f que seja necessária para executar em tempo polinomial (em relação ao comprimento da entrada). Simbolicamente:

$x\in L\Leftrightarrow f(x)\in TQBF$.

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

Então, suponhamos que L é uma linguagem PSPACE. Isso significa que L pode ser decidida por uma Máquina de Turing Determinística no espaço polinomial (MTD). Isso é crucial para a redução de L a TQBF, pois as configurações de qualquer Máquina de Turing podem ser representadas como fórmulas booleanas, com variáveis booleanas que representam o estado da máquina, bem como o conteúdo da fita em cada célula da Máquina de Turing. A posição da cabeça da Máquina de Turing é codificada na fórmula por meio de ordenações da fórmula.

Em particular, nossa redução usará as variáveis $C_{1}$ e $C_{2}$, representando duas configurações possíveis da MTD para L, e t, um número natural, na construção de uma QBF $\Phi _{C_{1},C_{2},t}$, a qual é verdadeira se e somente se a MTD para L pode ir de uma configuração codificada em $C_{1}$ em não mais que t passos. Então, a função f construirá da MTD para L uma QBF $\Phi _{C_{\text{start}},C_{\text{accept}},T}$, onde $C_{\text{start}}$ é uma configuração inicial da MTD, $C_{\text{accept}}$ é a configuração de aceitação da MTD e T é o número máximo de passos que uma MTD poderia precisar para mudar de uma configuração para outra. Sabemos que $T=O({\text{exp}}(n))$, onde n é o tamanho da entrada, porque isso limita o número de configurações possíveis relevantes na MTD. Claramente, a MTD não pode dar mais passos do que as configurações possíveis para chegar a $C_{\text{accept}}$, a menos que entre em loop. De qualquer forma, nunca chegará a $C_{\text{accept}}$.

Nessa fase da prova, nós já reduzimos a questão de saber se uma fórmula de entrada w (codificado, é claro, em $C_{\text{start}}$) está em L para a questão de saber se o QBF $\Phi _{C_{\text{start}},C_{\text{accept}},T}$, ou seja, f(w) está em TQBF. O restante dessa prova mostra que f pode ser computada em tempo polinomial.

Para t = 1, cálculo de $\Phi _{C_{1},C_{2},t}$ é simples — ou uma configurações muda para outro passo ou não. A máquina de Turing que representa a nossa fórmula é determinística, esta não apresenta nenhum problema.

Para t > 1, o cálculo de $\Phi _{C_{1},C_{2},t}$ envolve uma avaliação recursiva, à procura de um assim chamado “ponto médio” m₁. Neste caso, reescrevemos a fórmula seguinte:

$\Phi _{c_{1},c_{2},t}=\exists m_{1}(\Phi _{c_{1},m_{1},[t/2]}\land \Phi _{m_{1},c_{2},[t/2]})$.

Esta fórmula converte a questão de saber se um c um pode chegar a c₂ em t etapas, para a questão de saber se c₁ atinge um ponto médio m₁ em t/2 etapas, que se alcança c₂ em t / 2 passos. A resposta à última pergunta, naturalmente, dá resposta à primeira.

Agora, t é apenas limitado por T, que é exponencial (e por isso, não polinomial) no comprimento da entrada. Além disso, cada camada recursiva, praticamente, dobra o tamanho da fórmula. (A variável m 1 é apenas um ponto médio - para t maior existem mais paradas ao longo do caminho, por assim dizer). Assim, o tempo necessário para avaliar recursivamente (fórmula) desta forma poderia ser exponencial, bem como, simplesmente porque a fórmula poderia se tornar exponencialmente grande. Este problema é resolvido com o uso de um quantificador universal, usando as variáveis c 3 e c 4 sobre os pares de configurações, (por exemplo, {( c₁ , m₁ ), ( m₁ , c₂ )}), que impede a extensão da fórmula devida para expansão das camadas recursivas. Isso gera a seguinte interpretação $\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},[t/2]})$.

Esta versão da fórmula pode, realmente, ser computada em tempo polinomial. O par ordenado universalmente quantificado simplesmente nos diz que qualquer escolha de ( c₃ , c₄ ) é feita, $\Phi _{c_{1},c_{2},t}\Leftrightarrow \Phi _{c_{3},c_{4},[t/2]}$.

Assim,$\forall L\in PSPACE,L\leq _{p}TQBF$por isso, TQBF está em PSPACE-difícil. Juntamente com o resultado acima de que TQBF está em PSPACE, isso completa a prova de que TQBF está em PSPACE-completo.

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

Miscelânea

• Um subproblema importante na TQBF é o problema da satisfatibilidade booleana. Neste problema, deseja saber se uma fórmula dada boolean φ pode ser feita verdadeira com alguma atribuição de variáveis. Isto é equivalente ao TQBF usando apenas quantificadores existencial:$\exists x_{1}\ldots \exists x_{n}\Phi (x_{1},\ldots ,x_{n})$

• Este é também um exemplo de maior resultado em NP ℵ PSPACE, o qual segue diretamente da observação que a prova de um verificador em tempo polinomial de uma MTN (máquina de Turing não-determinística) requer espaço polinomial para armazenar a prova.

• Qualquer classe na hierarquia polinomial tem TQBF como seu problema completo. Em outras palavras, para a classe que compreende todas as linguagens que estão em L, existe um verificador de tempo polinomial MT V, tal que, para toda entrada x e alguma constante i,

$x\in L\Leftrightarrow \exists y_{1}\forall y_{2}\ldots \forall y_{i}\lor (x,y_{1},y_{2},\ldots ,y_{i})=1$ o qual tem uma configuração específica para QBF que é dada como:

$\exists \Phi \exists x_{1}\forall x_{2}\ldots \forall x_{i}{\big (}Q_{i}x_{i}\Phi (x_{1},x_{2},\ldots ,x_{i}){\big )}=1$ onde (x₁, x₂, ... , x_i) são vetores de variáveis booleanas.

• É importante notar que, embora TQBF seja uma linguagem definida como uma coleção de fórmulas booleanas verdadeiras, a sigla TQBF é frequentemente usada (inclusive neste artigo), para representar uma fórmula booleana totalmente quantificada, muitas vezes chamada simplesmente de QBF (Quantified Boolean Formula, conhecida como “totalmente” quantificada). É importante distinguir contextualmente o uso das duas abreviaturas na leitura da literatura.
• A TQBF pode ser pensada como um jogo entre dois jogadores com a alternância de movimentos. Variáveis quantificadas existenciais são equivalentes à noção de que um movimento está disponível para um jogador em um turno. Variáveis universalmente quantificadas significam que o resultado do jogo não depende de que um jogador faça um movimento naquele turno. Além disso, um TQBF cujo primeiro quantificador é existencial corresponde a um jogo de fórmula em que o primeiro jogador tem uma estratégia vencedora.
• A TQBF para a qual a fórmula quantificada está em 2-CNF pode ser resolvida em tempo linear por um algoritmo que envolve análise de conectividade forte na sua implicação do grafo correspondente. O problema 2-satisfatibilidade é um caso especial de TQBF para essas fórmulas em cada quantificador existencial .

Notas e referências

1. M. Garey and D. Johnson (1979). Computers and intractability: a guide to the theory of NP-completeness. W. H. Freeman, San Francisco, California. ISBN 0-7167-1045-5.
2. A. Chandra, D. Kozen, and L. Stockmeyer (1981). "Alternation". Journal of the ACM 28 (1): 114–133. doi:10.1145/322234.322243. http://portal.acm.org/citation.cfm?id=322243.
3. Adi Shamir (1992). "Ip = Pspace". Journal of the ACM 39 (4): 869–877. doi:10.1145/146585.146609. http://portal.acm.org/citation.cfm?doid=146585.146609.
4. Krom, Melven R. (1967), "The Decision Problem for a Class of First-Order Formulas in Which all Disjunctions are Binary", Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 13: 15–20, doi:10.1002/malq.19670130104 .
5. Aspvall, Bengt; Plass, Michael F.; Tarjan, Robert E. (1979), "A linear-time algorithm for testing the truth of certain quantified boolean formulas", Information Processing Letters 8 (3): 121–123, doi:10.1016/0020-0190(79)90002-4, http://www.math.ucsd.edu/~sbuss/CourseWeb/Math268_2007WS/2SAT.pdf .

• 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.

Ligações externas

• Generalized geography
• Teorema de Cookin-Levin
• The Quantified Boolean Formulas Library (QBFLIB)