Lógica
Proposicional
SAT e Custo
Computacional
O problema SAT

Dada uma fórmula proposicional


Determinar se  é satisfazível


 = (a  b) ( a b  c)
Problema de decisão
Para n símbolos proposicionais, são necessárias
2n linhas numa tabela verdade e 2m+1 colunas
a
0
0
b
c
0
1
b
1
0
c
1 0
1
c
1 0
c
1 0
1
Aplicações

Um “resolvedor de SAT” é a principal
ferramenta computacional para:
 Em Inteligência Artificial:



Em Projeto Automático de Componentes
Eletrônicos:





Programação em lógica
Provadores de teoremas
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
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ãodeterministicamente 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)
Resolvedores de SAT




Davis-Puttnan
DPLL
Resolução
Todas elas exigem que a fórmula esteja
na forma normal conjuntiva
Forma normal conjuntiva


Uma fórmula está na forma normal
conjuntiva (fnc ou CNF, em inglês) se é
uma conjunção de disjunções de literais
F é da forma F1 ^ F2 ^ ... ^ Fn, onde



Fi é uma disjunção (da forma
A1 v A2 v ... v An ) e
Ai é um literal
Ex: G=(PvQ) ^ (RvQvP) ^ (PvS)
Algoritmos para obter CNF
usando leis (repetidamente)

1 -Leis de eliminação



2 -Lei da negação


(H)  H
2 -Leis de De Morgan



PQ = (PvQ)
P  Q = (P  Q)^(Q  P)
(PvQ) = P ^ Q
(P^Q) = P v Q
3 -Leis distributivas:


F v (G^H) = (FvG) ^ (FvH)
F ^ (GvH) = (F^G) v (F^H) (não usada para CNF)
Notação na forma de
conjuntos




H=(PvQvR)^(PvQ)^(PvP)
Representação na forma de conjuntos:
H={[P,Q,R],[P,Q],[P]}
Note que


(PvQvR) = [P,Q,R]
(PvP)=[P]

Não é necessário representar duplicidade na
forma de conjuntos
Cláusulas e literais
complementares

Cláusula em lógica proposicional é uma
disjunção de literais



Usando a notação de conjuntos:
C1=[P,Q,R], C2=[P,Q], C3=[P]
Dois literais são complementares
quando um é a negação do outro
Resolvente de 2 cláusulas

Supondo 2 cláusulas C1=[A1,..., An] e
C2=[B1, ..., Bn], com literais
complementares





A, um conjunto de literais em C1, tal que
-A, um conjunto de literais complementares
a A, estão em C2
Resolvente de C1 e C2:
Res(C1,C2)=(C1-A)U(C2- -A)
Res(C1,C2) pode ser {}

Resolvente vazio ou trivial
Exemplo de resolvente




C1=[P,Q,R] e C2=[P,R]
Res (C1,C2) = [Q,R], que também é
uma cláusula
D1=[P,Q] e D2=[P,Q]
Res (D1,D2) = {}, que também é uma
cláusula
Idéia básica em todos os
algoritmos: Resolução

Resolução de um par de cláusulas com exatamente UMA
variável incompatível
a + b + c’ + f
g + h’ + c + f
a + b + g + h’ + f

E se tivermos mais de uma variável incompatível?
Algoritmo de Davis Putnam
M .Davis, H. Putnam, “A computing procedure for quantification theory", J. of ACM,
Vol. 7, pp. 201-214, 1960



Escolher uma variável a cada iteração para resolução até elas acabarem
INSAT se aparecer a cláusula vazia
Descarta as cláusulas resolvidas depois de cada iteração
(a + b + c)(b + c’ + f’)(b’ + e)
(a + b) (a + b’) (a’ + c)(a’ + c’)
(a + c + e)(c’ + e + f’)
(a) (a’ + c)(a’ + c’)
(a + e + f’)
(c)(c’)
SAT
()
INSAT
Pode explodir a memória!!!
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
a
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
a
0
 Decisão
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
a
0
b
0
 Decisão
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
a
0
b
0
c
0
 Decisão
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
a
0
b
0
c
0
a=0
(a + c + d)
d=1
Conflict!
Grafo de Implicação
c=0
(a + c + d’)
d=0
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
a
0
b
0
c
0
a=0
(a + c + d)
d=1
Conflict!
Grafo de Implicação
c=0
(a + c + d’)
d=0
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
a
0
b
0
c
0
 Backtrack
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
a
0
b
0
c
0
1  Decisão Forçada
a=0
(a + c’ + d)
d=1
Conflict!
c=1
(a + c’ + d’)
d=0
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
a
0
b
0
 Backtrack
c
0
1
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
a
0
b
0
c
0
1
1  Decisão Forçada
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
a
0
b
0
1
c
0
c
1
0
a=0
 Decisão
(a + c’ + d)
d=1
Conflict!
c=0
(a + c’ + d’)
d=0
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
a
0
b
0
1
c
0
c
1
0
 Backtrack
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
a
0
b
0
1
c
0
c
1
0
a=0
1  Decisão Forçada
(a + c’ + d)
d=1
Conflict!
c=1
(a + c’ + d’)
d=0
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
a
0
b
0
1
c
0
c
1
0
1
 Backtrack
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
a
0
1
b
0
1
c
0
c
1
0
1
 Decisão Forçada
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
a
0
1
b
0
b
c
0
0  Decisão
1
c
1
0
1
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
a
0
1
b
0
b
1
c
0
0
c
1
a=1
0
1
(a’ + b + c)
c=1
Conflito!
b=0
(a’ + b + c’)
c=0
Algoritmo DPLL
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
a
0
1
b
0
b
1
c
0
0
c
1
0
1
 Backtrack
Algoritmo DPLL
a
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
0
1
b
0
b
1
c
0
a=1
b=1
0
c
1
(a’ + b’ + c)
0
c=1
1
1  Decisão Forçada
Algoritmo DPLL
a
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
0
1
b
0
b
1
c
0
a=1
b=1
0
1
c
1
(a’ + b’ + c)
0
c=1
1
(b’ + c’ + d)
d=1
Algoritmo DPLL
a
(a’ + b + c)
(a + c + d)
(a + c + d’)
(a + c’ + d)
(a + c’ + d’)
(b’ + c’ + d)
(a’ + b + c’)
(a’ + b’ + c)
0
1
b
0
b
1
c
0
a=1
b=1
0
1
 SAT
c
1
(a’ + b’ + c)
0
c=1
1
(b’ + c’ + d)
d=1
Análise de DPLL e assorted…



Podem ser usados para provar tanto satisfatibilidade
quanto insatisfatibilidade
Mas DPLL não faz busca exaustiva, então não prova
insatisfatibilidade (e portanto conseqüência lógica)
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
Métodos de Busca
(GSAT, WSAT)
Cost
Local Minima
Global
minimum
Solution Space
Com Lógica de Predicados, o
método mais popular é a
resolução
Prova por resolução




Método por refutação
Dadas uma fórmula H e Hc, a forma
clausal associada a H
Uma Prova de H por resolução é uma
expansão fechada sobre Hc
H é um teorema do sistema de
resolução
Exemplo de Prova por
resolução







H=((P1vP2vP3)^(P1P4)^(P2P4)^ (P3P4))
 P4
Determinar Hc associada a H
Hc=(((P1vP2vP3)^(P1P4)^(P2P4)^
(P3P4)) P4))
=(((P1vP2vP3)^(P1P4)^(P2P4)^(P3P4))
vP4)
=(P1vP2vP3)^(P1vP4)^(P2vP4)^(P3vP4)^
P4
={[P1,P2,P3],[P1,P4],[P2,P4],[P3,P4],[P4]}
Agora, é só fazer a expansão por resolução!
Exemplo de Prova por
resolução (cont.)









1. [P1,P2,P3]
2. [P1,P4]
3. [P2,P4]
4. [P3,P4]
5. [P4]
6. [P2,P3,P4]
7. [P3,P4]
8. [P4]
9. {}
Res(1,2)
Res(3,6)
Res(4,7)
Res(5,8)
Lógica de
Predicados
Sintaxe
Alfabeto da Lógica de
Predicados






Símbolos de pontuação: (,)
Símbolos de verdade: false, true
Conjunto enumerável de símbolos para
variáveis: x, y, z, w, x1, y1, x2, z2...
Conjunto enumerável de símbolos para
funções: f, g, h, f1, g1, f2, g2...
Conjunto enumerável de símbolos para
predicados: p, q, r, s, p1, q1, p2, q2...
Conectivos proposicionais: ,v, , 
Termos

São construídos a partir destas regras:


Constantes e variáveis são termos
(representam objetos)
Se t1, t2, ..., tn são termos


f é um símbolo de função n-ária,
então f(t1, t2, ..., tn) também é um termo
Exemplos de termos




x, a (constante, função zero-ária)
f(x,a) se e somente se f é binária
g(y, f(x,a), c) se e somente se g é
ternária
+(9,10), -(9,5)



interpretados como 10+9, 9-5
Notação polonesa
h(x,y,z), considerada implicitamente
como ternária
Átomos

São construídos a partir destas regras:


O símbolo de verdade false é um átomo
Se t1, t2, ..., tn são termos


p é um símbolo de predicado n-ário
então p(t1, t2, ..., tn) é um átomo
Exemplos de átomos

P (símbolo proposicional)




Predicado zero-ário)
p(f(x,a),x) se e somente se p é binário
q(x,y,z) considerado implicitamente como
ternário
Ex: >(9,10), =(9,+(5,4))



interpretados como 10>9, 9=5+4
Interpretados como T
Note os abusos de linguagem


> e = são predicados
+ e – são funções
Fórmulas

São construídos a partir destas regras:




Todo átomo é uma fórmula da Lógica de
Predicados
Se H é fórmula então (H) também é
Se H e G são fórmulas, então (HvG)
também é
Se H é fórmula e x variável, então

((x)H) e ((x)H) são fórmulas
Construção de fórmulas



Átomos p(x), R e false
((p(x)) v R)
Que equivale a (p(x)  R)

também fórmula

((x) p(x)  R)

Expressão = termo v fórmula
Correspondência entre
quantificadores


((x)H)= ((z)(H))
((x)H)= ((z)(H))