Fórmula booliana totalmente quantificada

Na teoria da complexidade computacional, a linguagem TBQF é uma linguagem formal que consiste na quantificação verdadeira das fórmulas booleanas. Uma fórmula booleana totalmente quantificada é uma fórmula em quantificadores lógicos proporcional, onde cada variável é quantificada (ou vinculada), usando o quantificador universal ou o existencial no início da sentença. Tal fórmula é equivalente a verdadeiro ou falso (já que não há variáveis livres). Se a fórmula é avaliada como verdadeira, então ela está na linguagem TBQF. É também conhecida como QSAT (SAT quantificado).

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 ambos, quantificadores existenciais e quantificadores universais podem ser aplicados a cada variável. Dito de outra forma, pergunta se uma forma sentencial quantificada sobre um conjunto de variáveis booleanas é verdadeira ou falsa. Por exemplo, a instância seguinte é 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 [1]. Dada uma fórmula na árvore de sintaxe abstrata, o problema pode ser resolvido por um conjunto de procedimentos mutuamente recursivo que avalia a fórmula. Tal algoritmo usa o espaço proporcional à altura da árvore, o qual é linear no pior caso, mas usa o 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 que não é nenhuma surpresa uma vez que, de fato, AP = PSPACE, onde AP é a classe de problemas que podem ser resolvidas por máquinas alternadas em tempo polinomial[2].

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 [3].

As fórmulas em QBF tem 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 irá mover todos os quantificadores para frente da fórmula e então alterná-los entre quantificadores universal e existencial. Há outra redução que prova ser útil no IP = PSPACE, onde não mais que um quantificador universal é colocado entre o 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 para ter uma forma muito específica, chamada forma normal prenex. Ela tem duas partes básicas: uma porção contendo quantificadores e só 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 se insere no âmbito 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 existencial e universal alternados. Usando 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 teve o mesmo valor verdade, 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 frequente de provas.

Resolvendo

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

Q₁x₁Q₂x₂...Q_nx_nΦ(x₁, x₂, ..., 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₂x₂ ... Q_nx_nΦ(0, x₂, ..., x_n),

B = Q₂x₂ ... Q_nx_nΦ(1, x₂, ..., 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 apenas um problema linearmente menor. 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 tira um quantificador, 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. O QBF inicial foi totalmente quantificado, por isso há tanto quantificadores quanto variáveis. Assim, o algoritmo usa de espaço O ( n + log n ) = O ( n). Isso faz TQBF parte da classe de complexidade PSPACE.

PSPACE completude

A linguagem TQBF serve na teoria da complexidade como a canônica do problema PSPACE-completo. Sendo PSPACE-completo significa que uma linguagem está em PSPACE e que a linguagem também é PSPACE-difícil. O algoritmo acima mostra que TBQF 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. Ou seja,

∀L ∈ PSPACE, L ≤_p TQBF.

Isso significa que para uma linguagem L SPACE, se uma linguagem x está em L pode ser decidida por verificar 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 ∈ L ⇔ f(x) ∈ 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 é muito importante para a redução de L a TQBF, porque as configurações de qualquer máquina de Turing pode ser representada 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. Com a posição da cabeça da máquina de Turing codificada na fórmula por ordenações da fórmula. Em particular, nossa redução vai usar as variáveis C₁ e C₂, que representam duas configurações possíveis da MTD para L, e t um número natural, na construção de uma QBF Φ_{c1, c2, t}, o qual é verdadeiro, se e somente se a MTD para L pode ir de uma configuração codificada em c₁ em não mais que t passos. Então, a função f construirá da MTD para L uma QBF Φ _{cstart, caccept, T} , onde c_start é uma configuração inicial da MTD, c_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 (exp ( n )), onde n é o tamanho da entrada porque esta limita o número de configurações possíveis de relevância na MTD. É claro que a MTD não pode tomar as medidas mais que as configurações possíveis para chegar a c_aceita, a menos que ela entre em loop. De qualquer forma, ela nunca vai chegar a c_aceita.

Nessa fase da prova, nós já reduzimos a questão de saber se uma fórmula de entrada w (codificado, é claro, em c_start) está em L para a questão de saber se o QBF Φ_{Cstart, Caccept, 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 Φ_c1,c2,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 Φ_c1,c2,t envolve uma avaliação recursiva, à procura de um assim chamado “ponto médio” m₁. Neste caso, reescrevemos a fórmula seguinte:

Φ_c1,c2,t = ∃m₁(Φ_c1,m1,[t/2] ∧ Φ_m1,c2,[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 Φ_c1,c2,t:

Φ_c1,c2,t = ∃ m₁ ∀ (c₃, c₃) ∈ {(c₁, m₁), (m₁, c₂)}(Φ_c3,c4,[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, Φ_c1,c2,t ⇔ Φ_c3,c4,[t/2].

Assim, ∀L ∈ PSPACE, L ≤_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:

∃x₁... ∃x_nΦ(x₁,..., 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 ∈ L ⇔ ∃y₁∀y₂ ... Q_iy_i ∨ (x, y₁, y₂, ..., y_i) = 1 o qual tem uma configuração específica para QBF que é dada como:

∃Φ ∃x₁∀x₂ ... Q_ix_iΦ(x₁, x₂, ... , x_i ) = 1 onde os x_is 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 [4][5].

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)