Fórmula booliana totalmente quantificada

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa
Ambox rewrite.svg
Esta página precisa ser reciclada de acordo com o livro de estilo (desde julho de 2011).
Sinta-se livre para editá-la para que esta possa atingir um nível de qualidade superior.
NoFonti.svg
Este artigo ou se(c)ção cita fontes confiáveis e independentes, mas que não cobrem todo o conteúdo. Por favor, adicione mais referências e insira-as corretamente no texto ou no rodapé. Material sem fontes poderá ser removido.
Encontre fontes: Google (notícias, livros e acadêmico)
Ambox grammar.svg
Esta página ou secção precisa de correção ortográfico-gramatical.
Pode conter incorreções textuais, podendo ainda necessitar de melhoria em termos de vocabulário ou coesão, para atingir um nível de qualidade superior conforme o livro de estilo da Wikipédia. Se tem conhecimentos linguísticos, sinta-se à vontade para ajudar.

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 proposicional, 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[editar | editar código-fonte]

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:

xyz (( xz ) ∧ y)

QBF é o problema canônico completo para PSPACE, a classe de problemas solúveis por uma Máquina de Turing deterniní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[editar | editar código-fonte]

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:

x1x2x1...QnxnΦ(x1, x2, x3 ... xn)


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",

x1x2Φ(x1, x2) ⇔ ∃x1∀y1x2Φ(x1, x2)


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 é uma característica frequente de provas.

Resolvendo[editar | editar código-fonte]

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

Q1x1Q2x2...QnxnΦ(x1, x2, ..., xn)

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

A = Q2x2 ... QnxnΦ(0, x2, ..., xn),

B = Q2x2 ... QnxnΦ(1, x2, ..., xn).

Se Q1 = ∃, então retorne A ∨ B. Se Q1 = ∀, 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 que faltam quantificadores podem ser avaliados no espaço logaritmico 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[editar | editar código-fonte]

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 é 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 C1 e C2, 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 c1 em não mais que t passos. Então, a função f construirá da MTD para L uma QBF Φ cstart, caccept, T , onde cstart é uma configuração inicial da MTD, caccept é 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 possiveis para chegar a caceita, a menos que ela entre em loop. De qualquer forma, ela nunca vai chegar a caceita.

Nessa fase da prova, nós já reduzimos a questão de saber se uma fórmula de entrada w (codificado, é claro, em cstart) 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” m1. Neste caso, reescrevemos a fórmula seguinte:

Φc1,c2,t = ∃m1c1,m1,[t/2] ∧ Φm1,c2,[t/2]).

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

Agora, t é apenas limitado por T, que é exponencial(e por isso, não polnomial) 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, {( c1 , m1 ), ( m1 , c2 )}), 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 = ∃ m1 ∀ (c3, c3) ∈ {(c1, m1), (m1, c2)}(Φ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 ( c3 , c4 ) é 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[editar | editar código-fonte]

  • Um subproblema importante na TQBF é o problema da satifatibilidade 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:

∃x1... ∃xnΦ(x1,..., xn)

  • 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 temTQBF como seu problema completo. Em outras palavras, para a classe que compreende todas as linguagem 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 ⇔ ∃y1∀y2 ... Qiyi (x, y1, y2, ..., yi) = 1.

o qual tem uma configuração específica para QBF que é dada como:

∃Φ ∃x1∀x2 ... QixiΦ(x1, x2, ... , xi ) = 1 onde os xis 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 é frequente mente usada (ainda neste artigo), para representar uma fórmula booleana totalmente quantificada, muitas vezes chamado simplesmente de QBF(quantified Boolean formula, conhecido como “totalmente” quantificados). É 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 é correspondente a um jogo de fórmula em que o primeiro jogador tem um estratégia vencedora.
  • A TQBF para o qual a fórmula quantificada está em 2-CNF pode ser resolvido 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[editar | editar código-fonte]

  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[editar | editar código-fonte]