Lógica para Computação - Lógica Proposicional: Custo computacional do problema SAT, Método dos “Tableaux” Semânticos - aula8 log cin

Prévia do material em texto

Lógica Matemática 
Para Computação 
Lógica Proposicional 
Custo computacional do problema SAT 
 
 Problema SAT: Dada uma expressão φ da lógica 
proposicional pergunta-se: φ é satisfatível? 
 Note que para resolver uma instância do problema 
SAT, temos que realizar um certo número de 
operações booleanas, que depende do “tamanho” 
da expressão de entrada φ. 
 Que tal tentar encontrar uma forma razoavelmente 
precisa para estimar o número máximo de 
operações que devemos realizar para chegar a 
uma solução para o SAT? 
 
 
Lógica Proposicional 
Custo computacional do problema SAT 
 Problema SAT: Dada uma expressão φ da lógica 
proposicional pergunta-se: φ é satisfatível? 
 Estimativa: 
 Seja φ uma expressão. Assuma que: 
 “n”: número de operadores em φ. 
 “k”: número de variáveis listadas em φ. 
 Sabemos do conceito de valoração-verdade que 
vamos ter que testar (2 elevado a k) valorações. 
 Também vimos que o número de subexpressões de 
φ é no máximo igual a duas vezes o número de 
operadores + 1. Daí, para cada uma dessas (2 
elevado a k) valorações, vamos ter que fazer no 
máximo 2n+1 operações. 
 
 Vimos que seria enfadonho provar o 
seguinte argumento usando a tabela verdade 
 
 O unicórnio é bruxaria. 
 
É consequência lógica de: 
 
 O unicórnio, se não é lenda , é mamífero, mas se é 
lenda , ele é imortal. 
 
 Se o unicórnio é imortal ou mamífero, ele possui 
chifres. 
 
 O unicórnio, se ele possui chifres, é bruxaria. 
 
Método dos “Tableaux” Semânticos 
- Evert Beth (1954) 
- Jaakko Hintikka (1955) 
 
 
 Qual seria o significado intuitivo da 
noção de valoração-verdade? 
 
 
Método dos “Tableaux” Semânticos 
 
 Qual seria o significado intuitivo da 
noção de valoração-verdade? 
 
 Beth e Hintikka associaram o conceito de 
valoração-verdade à noção de 
possibilidade (``mundo possível´´). 
 
 Daí, ao perguntar se uma fórmula  é 
satisfatível, estamos perguntando se existe 
um mundo possível no qual  é verdadeira. 
 
Método dos “Tableaux” Semânticos 
 
 
 O método consiste na montagem de uma ``árvore 
de possibilidades´´, que se baseia em um conjunto 
de regras simples. 
 
 A árvore resultante indica os ``mundos possíveis´´ 
como sendo os caminhos de sua raiz até as folhas. 
 
 A árvore é construída adicionando-se nós às folhas 
de acordo com as regras, até que uma contradição 
seja encontrada ou não seja mais possível expandir 
a árvore. 
 
 
“Tableaux” : REGRAS 
1) ŵ(φ→ψ) = 1 
ŵ(ψ) = 1 ŵ(φ) = 0 
2) ŵ(φ→ψ) = 0 
ŵ(φ) = 1 
ŵ(ψ) = 0 
“Tableaux” : REGRAS 
3) ŵ(φψ) = 0 
ŵ(ψ) = 0 ŵ(φ) = 0 
4) ŵ(φψ) = 1 
ŵ(φ) = 1 
ŵ(ψ) = 1 
“Tableaux” : REGRAS 
5) ŵ(φψ) = 1 
ŵ(ψ) = 1 
6) ŵ(φψ) = 0 
ŵ(φ) = 0 
ŵ(ψ) = 0 
ŵ(φ) = 1 
“Tableaux” : REGRAS 
7) ŵ(φ) = 1 
ŵ(φ) = 0 
8) ŵ(φ) = 0 
ŵ(φ) = 1 
“Tableaux” Semânticos : Exemplo 
 
 φ = ( (X→(¬Y)) → ((¬Z)  (Y→(¬X))) ) 
 φ é satisfatível? 
 
 Quero saber se existe pelo menos uma valoração que 
satisfaz a expressão φ. Em outras palavras, quero saber 
se existe um mundo possível no qual φ seja verdadeira. 
 
 Vamos construir a árvore de possibilidades para a 
expressão φ. Vamos começar com φ e então ir 
“desmontando” esta expressão em subexpressões 
através das regras do tableaux, até não haver mais 
subexpressões no qual possamos usar alguma regra. 
Fazemos isso de cima para baixo, i.e., da raiz em direção 
as folhas. 
 
 
“Tableaux” Semânticos : Exemplo 
 
 φ = ( (X→(¬Y)) → ((¬Z)  (Y→(¬X))) ) 
 φ é satisfatível? 
 
 A árvore resultante indica os mundos possíveis, 
como sendo os caminhos da sua raiz até as folhas. 
 
 Um ramo da árvore é um caminho da raiz até uma 
das folhas. 
 
 Um ramo é dito fechado se ele contem nós rotulados 
com  e  (para uma dada fórmula ). Caso 
contrário, ele é chamado de ramo ou caminho 
aberto. 
 
 
“Tableaux” Semânticos : Exemplo 
 
 
 φ = ( (X→(¬Y)) → ((¬Z)  (Y→(¬X))) ) 
 φ é satisfatível? 
 
 
 
 
 Observe que as fórmulas nos nós de um mesmo 
ramo são consideradas como conjunção. Ao passo 
que diferentes ramos são considerados disjunções. 
 
 
 
 
“Tableaux” Semânticos : Exemplo 
 
 
 φ = (x→y) → ((z → x)  (zy)) 
 φ é uma tautologia? 
 
 O método do tableaux não é um método exaustivo, 
uma vez que não analisa todas as possibilidades. 
 
 Dessa forma, quando perguntamos se uma fórmula 
é tautologia, vamos verificar se existe a 
possibilidade dela ser falsa. 
 
 Por isso é um método de prova por refutação. 
 
 
“Tableaux” Semânticos : Mais exemplos 
 
 
 φ = (((x→y) → x)  x) 
 φ é uma tautologia? 
 
 E, se a pergunta fosse 
 φ é refutável? 
 
 E, se a pergunta fosse 
 φ é insatisfatível? 
 
 
 
 
 
“Tableaux” Semânticos : Mais exemplos 
 
 
 φ é consequência lógica de  ? ( | φ ?) 
 
 Estamos perguntando se   {} é insatisfatível. 
 
 Seja  = {1,2,...,n}. 
 
 Vamos procurar valorações que satisfaçam i e 
refute φ.