SAT e Custo Computacional

Prévia do material em texto

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 ↔ 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 (pergunta com resposta sim 
ou não)
 Para n símbolos proposicionais, são necessárias 
2n linhas numa tabela verdade e 2m+1 colunas
a
b b
c c c c
0
0 0
00 001
1 1
1 1 1
1
K-SAT
 Se uma fórmula da lógica proposicional 
está na CNF e cada cláusula contém 
exatamente k literais, nós dizemos que 
a fórmula é uma instância de k-SAT
 Exemplo, fórmula em 3-SAT
 (x v y v z) ^ (x v ~y v z) ^ (x v y v ~z)
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 parece ser 
exponencial
 Não-deterministicamente, 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
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
 Explicação menos técnica: 
B. Hayes, Can’t get no satisfaction, American Scientist, Vol. 
85, nr. 2, Mar-Apr 1997, 108-112
 São os mais complexos da classe NP
 Se resolvido um problema NP completo, todos da classe NP 
estariam resolvidos.
Resumo
 Problema de decisão: com resposta S ou N
 P: um problema de decisão que pode ser 
resolvido em tempo polinomial. Isto é, dada 
uma instância do problema, a resposta (SIM 
ou NÃO) pode ser decidida em tempo 
polinomial.
 Exemplo: Dado um mapa, é possível colorir os 
territórios com apenas duas cores, sem que 
territórios adjacentes tenham a mesma cor?
Resumo
 NP: um problema de decisão onde uma 
vez que nos seja dada (por um oráculo) 
uma solução (para SIM), é possível 
verificar que a solução é correta em 
tempo polinomial.
 Exemplo: Dados dois inteiros n e m, existe 
um inteiro f, com 1 < f < m tal que f divide 
n?
Resumo
 NP-completo: um problema NP x tal 
que é possível reduzir qualquer outro 
problema y em NP para x em tempo 
polinomial. 
 Exemplo: SAT, 3-SAT
Resumo
 NP-difícil: O problema x é NP-difícil se existe 
um problema NP-completo y que pode ser 
reduzido para x em tempo polinomial. (x não 
precisa ser NP)
 P=NP? É o problema mais famoso (em aberto) 
da computação
 Solução vale 1 milhão de dólares e fama maior que 
os Beatles: 
http://www.claymath.org/millenium-problems/p-vs-n
p-problem
 
Complexidade Computacional 
(cont.)
 Algoritmos deterministicamente polinomiais: 
logarítmico (log n), linear (n), quadrático 
(n2), cúbico (n3), n500,…
 Algoritmos exponenciais ou não-
deterministicamente polinomiais: 2n,nn,nlog n
 Algoritmos exponenciais são muito mais 
lentos que os polinomiais para valores altos 
de n
 Polinomiais são fortemente preferíveis!
Complexidade e SAT
 1-SAT:linear
 Como podemos solucionar?
 2-SAT: polinomial (Krom, 1967)
 3-SAT: NP-completo (Karp, 1972)
 (x11 OR x12 OR x13) AND
(x21 OR x22 OR x23) AND
(x31 OR x32 OR x33) AND ...
 Não existe um algoritmo 
polinomial para todas as 
instâncias do problema SAT, 
a não ser que P = NP (Cook, 
1971)
 Vira deterministicamente 
polinomial quando as 
sentenças viram 
 2-SAT (no máximo 2 
símbolos proposicionais por 
fórmula)
 Cláusula de Horn (No 
máximo 1 símbolo 
proposicional positivo em 
todas as sub-fórmulas) 
(Dowling e Gallier, 1984)
Resolvedores de SAT
 Davis-Putnan
 DPLL
 Resolução
 Todas elas exigem que a fórmula esteja 
na forma normal conjuntiva
Algoritmo DPLL
 Inicialmente descrito por Martin Davis e 
Hilary Putnam (1960)
 Depois uma nova versão foi publicada 
por Davis, Logemann e Loveland (1962)
 Daí o DPLL
 Faz uma busca em profundidade 
recursiva enumerando interpretações 
possíveis
Algoritmo DPLL
 Incorpora melhorias na busca
 Terminação prematura
 Heurística de símbolo puro
 Heurística de cláusula unitária
DPLL - Melhorias
 Terminação prematura: O algoritmo detecta se a 
sentença tem que ser verdadeira ou falsa, mesmo no 
caso de uma interpretação parcialmente concluída.
 Uma cláusula é verdadeira se qualquer literal é verdadeiro
 Uma sentença pode ser considerada verdadeira antes 
mesmo da interpretação estar completa: (AvB)^(AvC) com 
A verdadeiro
 Uma sentença é falsa se qualquer cláusula é falsa (todos os 
literais são falsos). Também pode ocorrer antes da 
interpretação completa
DPLL - Melhorias
 Heurística de símbolo puro: aquele que sempre 
aparece com o mesmo “sinal” em todas as cláusulas. 
 Na determinação de símbolo puro, o algoritmo pode ignorar 
as cláusulas que já são conhecidas como verdadeiras, dada 
a interpretação atual.
 Heurística de cláusula unitária: aquelas em que todos 
os literais com exceção de um já têm o valor falso 
atribuído pelo modelo.
 Ou seja, esse literal tem que ser verdadeiro
 A atribuição de uma cláusula unitária pode criar outras 
cláusulas unitárias
Algoritmo DPLL
Fonte: Figura 7.17 do livro Inteligência Artificial 3ª. ed (Russell e Norvig)
Algoritmo DPLL – Exercício
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(a’ + b + c)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
Notação: ´(negação); + (OU); E entre as linhas
Análise de DPLL
 Pode ser usado para provar tanto satisfatibilidade 
quanto insatisfatibilidade
 Outros métodos:
 WalkSAT (método incompleto):
 Estado Inicial: sorteia valorações de variáveis pré-
ordenadas
 Operador de busca: 
 Pega uma cláusula ainda insatisfeita e um literal nela
 Sorteia uma valoração pro literal
 A cada passo, escolhe aleatoriamente entre as seguintes 
estratégias para pegar um literal:
 Pega o literal cujo sorteio resulta na maior redução no número de 
cláusulas insatisfeitas
 Pega um literal aleatório
Incompletude de WalkSAT
 Quando uma interpretação é encontrada, a sentença de 
entrada de fato é satisfazível
 Quando não é encontrada podem ser duas razões:
 A sentença é insatisfazível
 Precisamos dar mais tempo para o WalkSAT tentar encontrar 
uma interpretação
 WalkSAT tem boa performance em muitos casos quando 
há uma interpretação que satisfaz a sentença.
 No entanto não pode ser usado para detectar a não 
satisfazibilidade (necessária para definir a consequência 
lógica)
	Slide 1
	Slide 2
	Slide 3
	Slide 4
	Slide 5
	Slide 6
	Slide 7
	Slide 8
	Slide 9
	Slide 10
	Slide 11
	Slide 12
	Slide 13
	Slide 14
	Slide 15
	Slide 16
	Slide 17
	Slide 18
	Slide 19
	Slide 20
	Slide 21
	Slide 22
	Slide 23
	Slide 24