Lógica Proposicional SAT e Custo Computacional. Conjuntos FOR: conjunto das fórmulas SAT: conjunto...

Lógica Proposicional

SAT e Custo Computacional

Conjuntos FOR: conjunto das fórmulas SAT: conjunto das fórmulas

satisfazíveis INSAT: conjunto das fórmulas

insatisfazíveis TAUT: conjunto das tautologias REFUT: conjunto das fórmulas

refutáveis(Falsificável) Refutável é toda fórmula H tal que exista

pelo menos uma interpretação I[H]=F

Lema de pertinência

Para H € FOR: H € SAT H € INSAT H € INSAT (H) € TAUT H € SAT (H) € TAUT H € REFUT H € TAUT H € REFUT (H) € INSAT

Lema entre os conjuntos SAT, INSAT, TAUT, REFUT FOR TAUT SAT INSAT REFUT TAUT REFUT = {} INSAT SAT = {} SAT U REFUT = FOR TAUT U INSAT FOR SAT REFUT = {}

O problema SAT Dada uma fórmula proposicional

= (a b) ( a b c) Determinar se é satisfazível

Problema de decisão Para n símbolos proposicionais, são

necessárias 2n linhas numa tabela verdade e 2m+1 colunasa

b b

c c c c

0

0 0

00 001

1 1

1 1 1

1

Aplicações Um “resolvedor de SAT” é a principal

ferramenta computacional para: Em Inteligência Artificial:

Programação em lógica Provadores de teoremas

Em Projeto Automático de Componentes Eletrônicos:

Teste e Verificação Síntese

Escalonamento Planejamento …

Custo Computacional O custo (determinístico) de SAT é dito

exponencial Não-determinísticamente, o custo de SAT cai

para cerca de 2m+1 Custo não-deterministicamente polinomial (NP) Testam-se apenas algumas linhas da tabela O no. de sub-fórmulas é sempre até 2 vezes o

número de conectivos mais 1

Complexidade Computacional (cont.) Algoritmos deterministicamente

polinomiais: logarítmico, linear quadrático, cúbico (log n, n, n**2, n**3, …, n**500,…)

Algoritmos exponenciais (ou não-deterministicamente polinomiais): 2**n,n**n,n**log n

Algoritmos exponenciais são mais lentos que os polinomiais para valores altos de n

Polinomiais são preferíveis!

Complexidade e SAT 1-SAT:linear (um literal por

subfórmula) 2-SAT: linear (com fases)

(x11 OR x12) AND(x21 OR x22) AND(x31 OR x32) AND…

3-SAT: NP-completo (x11 OR x12 OR x13) AND

(x21 OR x22 OR x23) AND(x31 OR x32 OR x33) AND ...

O problema são os conflitos, que diminuem a satisfabilidade!

Não existe um algoritmo polinomial para todas as instâncias do problema SAT, a não ser que P = NP

Vira deterministicamente polinomial quando as sentenças viram

2-SAT (no máximo 2 símbolos proposicionais por fórmula)

Cláusula de Horn – 1-SAT (No máximo 1 símbolo proposicional positivo em todas as sub-fórmulas)

Complexidade Computacional

Criação da classe de problemas NP-CompletoS. A. Cook, The complexity of theorem proving

procedures, Proceedings, Third Annual ACM Symp. on the Theory of Computing,1971, 151-158

Abordagem mais simples: B. Hayes, Can’t get no satisfaction, American

Scientist, Vol. 85, nr. 2, Mar-Apr 1997, 108-112

Vocabulário

Sistemas de Dedução, Decidibilidade,

Corretude, Completude, Consistência,

Monotonicidade

Cálculo Proposicional

Cálculo = Lógica + Sistema de Prova (ou dedução)

Um sistema de prova serve para analisar e raciocinar sobre argumentos de uma lógica, de maneira a prová-los válidos ou inválidos.

Sistema de dedução

Alfabeto de uma Lógica Conjunto de fórmulas desta Lógica Conjunto de regras de dedução (ou

regras de inferência)

Como avaliar sistemas de dedução?? Avaliação do problema de dedução

Finitude da solução algorítmica (decidibilidade)

Avaliação do algoritmo de dedução Complexidade

Avaliação da capacidade de inferência Qualidade: Consistência Eficiência: Completude

Avaliação de lógicas e seus algoritmos de dedução Análise de lógicas Expressividade Finitude = Decidibilidade

Tem a ver com teoria da computação Computabilidade, Máquinas de Turing, funções

recursivas, ... Análise para métodos de dedução

Correção Completude Consistência Monotonicidade

Computabilidade

Intuitivamente uma função é dita computável se é possível calcular seu valor, dado qualquer elemento do seu domínio

Será toda função, bem definida, computável?

NEM SEMPRE!!!

Decidibilidade Caso particular de computabilidade

quando a função só admite dois valores É possível resolver um problema

algoritmicamente (insolubilidade)? Quando se fala se um problema é solúvel

tem-se um problema de decidibilidade Trata-se de saber se um algoritmo acaba

Devolvendo uma resposta, no nosso caso, T ou F

Há lógicas que são assim!

Complexidade Computabilidade diz respeito a se um

problema pode ou não ser resolvido Complexidade diz respeito à

quantidade de recursos necessários para resolver um problema

Os recursos (normalmente) são: Memória Tempo

Porém... Complexidade não será analisada nesse curso

E para sistemas de dedução?

Desejamos que nossos sistemas de dedução tenham certas propriedades...

Quais??

Relembrando conceitos Conseqüência lógica Contradição Lógicas precisam ter sintaxe e

semântica bem definidas!

Avaliando sistemas de dedução

Queremos que o nosso sistema de dedução hipotético SD para ela (a lógica proposicional) seja correto, completo e consistente

Verificar também monotonicidade

Que danado é isso???

Correto Correto:

Toda sentença deduzida por SD a partir de um dado conjunto de

sentenças S inclusive o conjunto vazio de sentenças!

Seja realmente dedutível a partir de S!

Se as premissas são válidas, a conclusão também é válida!

Completo e Consistente

Completo: Toda sentença realmente dedutível a

partir de S, seja também dedutível através de SD

Consistente: Não seja possível gerar contradições

usando SD

Teorema da correção Um sistema de dedução SD é correto se

satisfaz à condição abaixo Todas as condições são a mesma no fundo

Se H é conseqüência lógica de um

conjunto de hipóteses a partir de SD, H é realmente conseqüência lógica de

Se ├SD H, então ⊨ H SD só deduz fórmulas corretas!!

Teorema da completude Um sistema de dedução SD é completo se

satisfaz às condições abaixo Todas as condições são a mesma no fundo

Se H é conseqüência lógica de um conjunto de hipóteses , H também é conseqüência lógica de a partir de SD

Se ⊨ H, então ├SD H Toda fórmula dedutível também é

dedutível por SD!!

Teorema da Consistência

Um sistema de dedução SD é consistente sse não é possível deduzir usando SD duas fórmulas que se contradizem

Não é possível ├SD H e ├SD H Teorema: Um sistema correto é

também consistente

Prova do Teorema da Consistência

Se ├SD H, pelo teorema da correção:

H é tautologia H é contraditória Não é possível ├SD H,

pois H seria uma tautologia Não é possível que H e H sejam

tautologias

Monotonicidade

Definição fraca: Se KBi├ H, então KBj├ H Não perder o que é dedutível

Definição forte: Se KBi├ H e j>i, então KBj├ H e KBj KBi KB só aumenta