Diagrama de decisión binaria
En informática , un diagrama de decisión binario ( BDD ) o un programa de ramificación es una estructura de datos que se utiliza para representar una función booleana . En un nivel más abstracto, los BDD pueden considerarse como una representación comprimida de conjuntos o relaciones . A diferencia de otras representaciones comprimidas, las operaciones se realizan directamente sobre la representación comprimida, es decir, sin descompresión.
Estructuras de datos similares incluyen forma normal de negación (NNF), polinomios de Zhegalkin y gráficos acíclicos dirigidos proposicionales (PDAG).
Una función booleana se puede representar como un gráfico acíclico dirigido y con raíz , que consta de varios nodos (de decisión) y dos nodos terminales. Los dos nodos terminales están etiquetados como 0 (FALSO) y 1 (VERDADERO). Cada nodo (de decisión) está etiquetado por una variable booleana y tiene dos nodos secundarios llamados hijo bajo y hijo alto. El borde del nodo a un hijo bajo (o alto) representa una asignación del valor FALSO (o VERDADERO, respectivamente) a la variable . Tal BDD se llama 'ordenado' si diferentes variables aparecen en el mismo orden en todas las rutas desde la raíz. Se dice que un BDD está 'reducido' si se han aplicado las siguientes dos reglas a su gráfico:
En el uso popular, el término BDD casi siempre se refiere al Diagrama de Decisión Binario Ordenado Reducido ( ROBDD en la literatura, usado cuando es necesario enfatizar los aspectos de ordenación y reducción). La ventaja de un ROBDD es que es canónico (único) para una función particular y orden variable. [1] Esta propiedad lo hace útil en la verificación de equivalencia funcional y otras operaciones como el mapeo de tecnología funcional.
Una ruta desde el nodo raíz hasta el terminal 1 representa una asignación de variable (posiblemente parcial) para la cual la función booleana representada es verdadera. A medida que la ruta desciende a un elemento secundario bajo (o alto) desde un nodo, la variable de ese nodo se asigna a 0 (respectivamente 1).
La siguiente figura de la izquierda muestra un árbol de decisión binario (no se aplican las reglas de reducción) y una tabla de verdad , cada una de las cuales representa la función . En el árbol de la izquierda, el valor de la función se puede determinar para una asignación de variable dada siguiendo un camino hacia abajo en el gráfico hasta una terminal. En las siguientes figuras, las líneas punteadas representan bordes para un niño bajo, mientras que las líneas continuas representan bordes para un niño alto. Por lo tanto, para encontrar , comience en x1, recorra la línea punteada hasta x2 (ya que x1 tiene una asignación de 0), luego baje dos líneas continuas (ya que x2 y x3 tienen cada una una asignación de uno). Esto lleva a la terminal 1, que es el valor de .
