Lógica Proposicional II - Diagramas de Decisão Binários

O grande problema do algoritmo baseado em tabelas de verdade é o seu crescimento exponencial. Assim sendo, foram desenvolvidos outros algoritmos que permitem aferir de modo mais eficiente os valores lógicos de uma fbf. Nesta secção serão abordados os Diagramas de Decisão Binários, desordenados e ordenados, e na secção seguinte os Algoritmos de SAT.

Diagramas de Decisão Binários - (O)BDDs

Precisamos, para falar de BDDs, de definir primeiro árvore de decisão.

As árvores de decisão e as tabelas de verdade são, contudo, bastante semelhantes em relação ao seu tamanho e quantidade de pontos de decisão. Podemos, no entanto, transformá-las em grafos acíclicos dirigidos e rotulados para representar, de modo mais condensado, a mesma informação.

É, então, interessante definir algumas propriedades que nos serão úteis:

Um BDD é um grafo acíclico, dirigido e rotulado em que os rótulos dos nós podem tanto ser proposições (em nós iniciais/não terminais) como valores lógicos (folhas). Continuamos a ter os tais arcos a "cheio" e tracejado.

Um diagrama de decisão binário ordenado, OBDD, é um BDD que satisfaz alguma relação de ordem total para os símbolos de proposição que contém. Num OBDD não podem existir caminhos que contenham mais que uma vez o mesmo símbolo de proposição.

• O nível, $i$, de um OBDD é o conjunto de todos os seus nós de profundidade $i$.
• Dois OBDDs dizem-se compatíveis caso exista uma ordem aplicada aos seus símbolos de proposição tal que ambos os OBDDs a satisfaçam - se $P$ vem antes de $Q$ em $OBDD_{1}$, $P$ não pode vir depois de Q em $OBDD_{2}$.

Exemplos de OBDDs incompatíveis

Os exemplos abaixo não são compatíveis, visto que não há uma ordem clara - no primeiro, $R$ vem antes de $Q$; no segundo $R$ vem depois de $Q$. Não podendo estabelecer uma relação de ordem entre os símbolos de proposição, dizemos que são incompatíveis.

Dada a importância dos resultados obtidos pelos testes de verificação de propriedades de fbfs que utilizam OBDDs, devemos olhar para os algoritmos que nos ajudam a manipulá-los.

Algoritmo reduz

Percorre, por níveis, o grafo correspondente ao OBDD, começando pelas folhas. Atribui um identificador a cada OBDD tal que:

• todas as folhas F têm o id 0 e todas as folhas V têm o id 1;

• a atribuição dos identificadores de um nível é feita considerando que todos os OBDDs abaixo já foram identificados. Assim sendo:

  • caso dois sub-OBDDs positivo e negativo (em relação ao "pai") tenham o mesmo identificador, esse identificador é dado também ao OBDD "pai".

  • caso entre os OBDDs já identificados exista um OBDD tal que o OBDD a identificar e ele têm raízes com rótulos iguais, com OBDDs positivos e negativos com os mesmos identificadores, então o identificador do OBDD a identificar é o mesmo desse que estamos a comparar.

  • caso contrário, atribuímos um novo identificador.

Só teoricamente este algoritmo pode ser difícil de entender à primeira, pelo que talvez o exemplo seguinte (e a sua explicação) ajudem a entender:

Exemplo - Algoritmo Reduz

Ora, vamos por partes:

• o primeiro passo consiste em atribuir os identificadores 0 e 1 às folhas F e V, respetivamente;

• passamos para o OBDD de raiz R mais à direita - os "sub-OBDDs" não têm o mesmo identificador, nem existem outros OBDDs identificados com raízes de rótulo igual que possamos considerar; assim sendo, atribuímos um novo identificador, 2;

• olhamos agora para o OBDD de raiz R mais à esquerda: de facto os seus "sub-OBDDs" continuam sem ter o mesmo identificador, mas existe um OBDD já identificado com rótulo R, que por acaso tem OBDDs positivo e negativo iguais. Assim sendo, podemos atribuir o mesmo identificador a este OBDD, 2;

• temos agora o OBDD de raiz Q mais à direita - os seus "filhos" têm ambos o mesmo rótulo e o mesmo identificador, pelo que podemos atribuir esse identificador ao "pai" - 2;

• passando para o OBDD de raiz Q mais à esquerda, podemos reparar que não só os seus filhos não têm rótulos iguais como o OBDD de raiz Q já identificado não tem OBDDs positivo e negativo iguais aos seus. Não nos resta, portanto, outra alternativa senão atribuir um novo identificador, 3;

• por fim, olhando para a raiz P, podemos perceber que os seus "filhos" não têm o mesmo identificador, e que os seus OBDDs positivo e negativo são claramente distintos, levando-nos portanto à atribuição de um novo identificador, 4!

Temos, então, o nosso OBDD todo identificado, pronto para aplicação do algoritmo seguinte, o compacta!

Algoritmo compacta

Com o nosso OBDD identificado, fruto do trabalho realizado com o reduz, passamos à fase de compactação do OBDD.

O algoritmo recebe um OBDD já identificado e a sua lista associativa, substituindo cada sub-OBDD cujo identificador é $i$ pela correspondente chave na lista associativa. Por exemplo, a lista associativa do exemplo acima tem chaves de 1 a 4 e os valores associados tal como demonstrados abaixo (o OBDD à esquerda é o resultado final):

Note-se que, começando pela raiz, P tem sub-OBDDs 3 e 2, com raízes Q e R, respetivamente; Q está ligado a R e a falso, R ligado a falso e a verdadeiro, originando o OBDD compactado tal como o temos à direita.

Cada fbf $\alpha$ tem um único OBDD reduzido que segue uma dada ordem de relação. Podemos, a partir do que foi visto até agora, retirar algumas noções interessantes:

• Uma fbf é tautológica apenas se o seu OBDD reduzido é $V$.

• Uma fbf é satisfazível apenas se o seu OBDD reduzido não é $F$.

• Uma fbf é não satisfazível/contraditória apenas se o seu OBDD reduzido é $F$.

• Duas fbfs são equivalentes apenas se os seus OBDDs são estruturalmente semelhantes. Dizemos que dois OBDDs são estruturalmente semelhantes se as raízes tiverem o mesmo rótulo e os respetivos OBDDs positivo e negativo forem estruturalmente semelhantes.

Algoritmo aplica

O algoritmo em questão recebe um operador lógico binário (op) e dois OBDDs reduzidos e compatíveis de duas fbfs distintas, $\alpha$ e $\beta$, devolvendo o OBDD reduzido da fbf que correspondente a $\alpha$ op $\beta$. Se quisermos que o operador seja $\neg$, faremos a disjunção exclusiva (vulgo XOR).

A intuição utilizada durante o algoritmo é:

• Se ambos os OBDDs considerados forem folhas, aplicamos a operação aos correspondentes valores lógicos (i.e $V \vee F$ resulta em $V$, etc.);

• Caso contrário, escolhemos o símbolo de proposição com mais prioridade entre $\alpha$ e $\beta$, que será a raiz de pelo menos um dos OBDDs, dividindo o problema em 2 subproblemas, um onde o símbolo de proposição é verdadeiro e no outro falso:

  • se o símbolo de proposição for a raiz de ambos os OBDDs, o resultante tem esse símbolo de proposição como raiz - o OBDD negativo resulta de aplicar o algoritmo recursivamente aos negativos, os positivos aos positivos;

  • caso contrário, o resultante terá esse símbolo de proposição como raiz. O OBDD negativo resulta de aplicar o algoritmo ao seu OBDD negativo e ao OBDD que não contém o símbolo de proposição (o mesmo para o positivo).

Mais uma vez, provavelmente fica mais fácil a ver o exemplo e ler a explicação.

Vejamos então o que acontece com $aplica(\wedge, O_{\neg P \wedge \neg R}, O_{P \vee (Q \wedge R)})$.

(Acima encontram-se os OBDDs reduzidos de cada fbf)

Podemos notar que em ambos os OBDDs o símbolo de proposição com maior prioridade é $P$, raiz de ambos os OBDDs, pelo que o seu OBDD negativo resulta de aplicar o algoritmo aos respetivos OBDDs negativos e o positivo aos positivos (o "resultante" tem como linhas a cheio as linhas originalmente ligadas por $P$ a cheio, a tracejado as originalmente ligadas a tracejado). Num dos caminhos temos a conjunção de verdadeiro e falso, que é falso, mas ainda temos de olhar para o outro caminho, visto que não sabemos se nos pode dar uma resposta diferente.

Aplicar o algoritmo ao OBDD negativo é diferente, visto que os sub-OBDDs não têm a mesma raiz. Assim sendo, pegamos no símbolo de proposição com mais prioridade na relação de ordem total (neste caso Q ou vem antes de R ou não aparece, pelo que escolhemos Q) e fazemos dele a raiz. Temos, então, que o seu OBDD negativo resulta de aplicar op ao OBDD que não contém Q e ao OBDD negativo de Q; o seu OBDD positivo resulta de aplicar op ao OBDD que não contém Q e ao OBDD positivo de Q. Aqui podemos verificar que ambos os caminhos resultam em falso, pelo que o resultado final é também falso (todos os caminhos levam a falso) e a conjunção das 2 fbfs é uma contradição.