7 - SAT e Custo Computacional

Esta é uma pré-visualização de arquivo. Entre para ver o arquivo original

Clique para editar o estilo do título mestre
Clique para editar o estilo do subtítulo mestre
*
*
*
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
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 D H € INSAT
H € INSAT D (H) € TAUT
H € SAT D (H) € TAUT
H € REFUT D H € TAUT
H € REFUT D (H) € INSAT
*
*
*
Lema entre os conjuntos
SAT, INSAT, TAUT, REFUT  FOR
TAUT  SAT
INSAT  REFUT
TAUT I REFUT = {}
INSAT I SAT = {}
SAT U REFUT = FOR
TAUT U INSAT  FOR
SAT I 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 colunas
*
*
*
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 
2m+1 é o número de sub-proposições, por indução 
m= no. de conectivos da fórmula
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
Criação da classe de problemas NP-Completo
S. 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
	
*
*
*
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)