Aula_lógica_-_Algoritmo_BDD

Prévia do material em texto

Algoritmos BDD
Carlos Andrade
Equivalência entre fórmulas
 Sejam A1 e A2 fórmulas. 
 Desejamos saber se elas são logicamente equivalentes.
 Como?
 Tabelas verdades
 Tableaux (A1  A2)
 Resolução
 Outros
 Problema:
 Todos os métodos são ineficientes para fórmulas grandes
 Qual seria uma alternativa?
Binary Decision Diagrams (BDDs)
 BDDs são estrutura de dados para fórmulas 
proposicionais.
 Sobre determinadas condições BBDs possuem uma 
estrutura única para fórmulas equivalentes.
 Algoritmos para BDDs são eficientes em muitos casos.
 BDDs têm sido utilizados extensivamente em aplicações 
como design de circuitos e verificação de programas. 
 Verifica-se a equivalência entre fórmulas, que por sua vez descrevem 
a operação de um circuito ou programa.
Apresentação Intuitiva de BDD (Ex. 1)
Apresentação Intuitiva de BDDs
p q r p v (q^r) 
T T T T
T T F T
T F T T
T F F T
F T T T
F T F F
F F T F
F F F F
• Tabelas verdades eficientes 
Apresentação Intuitiva de BDDs
p q r p v (q^r) 
T T * T
T T * T
T F T T
T F F T
F T T T
F T F F
F F T F
F F F F
• Tabelas verdades eficientes 
Apresentação Intuitiva de BDDs
p q r p v (q^r) 
T T * T
T T * T
T F * T
T F * T
F T T T
F T F F
F F T F
F F F F
• Tabelas verdades eficientes 
Apresentação Intuitiva de BDDs
p q r p v (q^r) 
T T * T
T T * T
T F * T
T F * T
F T T T
F T F F
F F T F
F F F F
• Tabelas verdades eficientes 
Apresentação Intuitiva de BDDs
p q r p v (q^r) 
T T * T
T F * T
F T T T
F T F F
F F T F
F F F F
• Tabelas verdades eficientes 
Apresentação Intuitiva de BDDs
p q r p v (q^r) 
T * * T
T * * T
F T T T
F T F F
F F T F
F F F F
• Tabelas verdades eficientes 
Apresentação Intuitiva de BDDs
p q r p v (q^r) 
T * * T
F T T T
F T F F
F F T F
F F F F
• Tabelas verdades eficientes 
Apresentação Intuitiva de BDDs
p q r p v (q^r) 
T * * T
F T T T
F T F F
F F * F
F F * F
• Tabelas verdades eficientes 
Apresentação Intuitiva de BDDs
p q R p v (q^r) 
T * * T
F T T T
F T F F
F F * F
• Tabelas verdades eficientes 
Apresentação Intuitiva de BDDs
p q R p v 
(q^r) 
T * * T
F T T T
F T F F
F F * F
p q r p v 
(q^r) 
T T T T
T T F T
T F T T
T F F T
F T T T
F T F F
F F T F
F F F F
=>
Apresentação Intuitiva de BDD (Ex. 2)
Apresentação Intuitiva de BDDs
p q r p + q+r 
T T T T
T T F F
T F T F
T F F T
F T T F
F T F T
F F T T
F F F F
• Tabelas verdades eficientes
• Legenda: ‘+’ representa ou exclusivo.
Apresentação Intuitiva de BDDs
p q r p + q+r 
T T ** T
T T ** F
T F * F
T F * T
F T * F
F T * Ver linhas 3 e 4
F F ** T
F F ** Ver linhas 1 e 2
• Tabelas verdades eficientes
• Legenda: ‘+’ representa ou exclusivo.
Apresentação Intuitiva de BDDs
p q r p + q+r 
T T ** T
T T ** F
T F * F
T F * T
F T * Ver linhas 3 e 4
F F ** T
F F ** Ver linhas 1 e 2
• Tabelas verdades eficientes
• Pense em ‘Ver linha 3 e 4’ como um ponteiro para r.
• O comportamento de r é igual ao da linha 3 ou ao da linha 4.
Redução de BDDs
 Representamos BDDs através de árvores binárias, tal 
que:
 Cada nó é uma fórmula atômica
 Linhas sólida = True
 Linha pontilhada = False
 Todas as folhas são rotuladas com a fórmula formada do 
caminho da raiz até determinada folha. 
 Figura 1, pág 83.
Redução de BDDs
 Podemos reduzir esta árvore mantendo a mesma 
interpretação das fórmulas.
 Quais modificações deveriam ser realizadas?
Redução de BDDs
 Reduzir todas as folhas em apenas duas, uma para T 
e outra para F. 
 Qual seria a segunda modificação para simplificar a 
árvore?
Redução de BDDs
 Remoção dos nós que não são necessários para 
avaliar a formula. 
 Este processo é similar com a simplificação da tabela 
verdade descrito anteriormente no Exemplo 1.
De árvore para tabela verdade
 Exercício: Desenhe a representação da árvore da 
segunda figura da pág 83 na forma de tabela 
verdade.
Tabela verdade da fig 2. pág 83
p q r p v (q^r) 
T T T T
T T F T
T F T T
T F F T
F T T T
F T F F
F F T F
F F F F
Redução de BDDs
 Figuras da pág 83, e 84. Tipo de redução 1 e tipo de redução 2. 
 r possui caminhos levando ao mesmo nó. Na tabela, isso equivaleria 
a dizer que r não interfere no resultado final da fórmula. Logo 
podemos retira-lo. 
 A segunda simplificação de q parte da mesma regra e equivale 
também a simplificação de q na primeira tabela. 
 A simplificação mais esquerda equivale a simplificação das duas 
ultimas linhas da tabela. 
 Notar a equivalência das simplificações através da tabela e do 
diagrama BDD.
Redução de BDDs
 O exemplo 2 também é observado na redução dos 
BDDs na figuras ultimas figuras da pág 84 e 85. 
 Na tabela tínhamos r como ‘ponteiro’. Seu valor 
determinava no resultado final da fórmula. 
 Exercício: Fazer a redução no BDD olhando para 
como foi feita a redução do tipo 2 na tabela.
Redução BDD
 Dica: Observe o comportamento dos nós internos r 
(segundo mais a esquerda, segundo mais a direita), e 
dos nós externos r (mais a esquerda e mais a direita)
Redução BDD
 Como os comportamentos são iguais, podemos ligar 
a linha sólida do q mais a direita ao r mais á 
esquerda, e podemos ligar a linha pontilhada desse 
mesmo q ao segundo r da esquerda para direita. 
 O diagrama resultante é dado pela figura da pág 85.
Operações de BDDs
A operação Apply
 Não é muito eficiente construir um BDD com a quantidade de 
nós praticamente igual ao de fórmulas em uma tabela 
verdade.
 BDDs permitem criar operações lógicas diretamente de dois 
BDDs reduzidos, ou seja: 
 Existe uma operação apply que constrói um BDD para A1 op A2, tal que 
op é um operador lógico qualquer, de forma direta e eficiente a partir dos 
BDDs reduzidos A1 e A2.
 O algoritmo também é utilizado para construir um BDD 
inicial de uma fórmula arbitrária construindo-o dos BDDs 
para átomos. 
 Exemplo do BDD para o átomo p. Pág 86.
A operação Apply
 O algoritmo utiliza indução estrutural no par de 
BDDs.
 Toda sub-árvore é por indução estrutural um BDD, e 
portanto o passo da operação Apply garante que o 
novo BDD é também um BDD.
A operação de restrição
 Uma operação de restrição toma uma fórmula A, um 
átomo p e um valor v = T ou v = F e retorna uma 
fórmula obtida substituindo v por p e avaliando 
parcialmente A. 
 Notação: A|p=v
 Exemplo 4.59, pág 91
Algoritmos BDD
 Definição: Ordered Binary Decision Diagram 
(OBDD)
 Algoritmos:
 Reduce
 Apply
 Restrict
 Ver referência.
Trabalho de BDD
Referência
 Mordenchai Bem-Ari. Mathematical Logic for 
Computer Science, Second Edition. Editora: 
Springer.