En informática , un gráfico de decisión binario o diagrama de decisión binario (o BDD para Diagrama de decisión binario en inglés) es una estructura de datos que se utiliza para representar funciones booleanas o cuestionarios binarios. Los BDD se utilizan para representar conjuntos o relaciones de forma compacta / comprimida .
Los programas de diseño asistido por computadora (CAD / CAD) utilizan diagramas de decisión binarios para generar circuitos (síntesis lógica) y en verificación formal . Es una estructura de datos considerada compacta, en comparación, por ejemplo, con árboles de decisión . Los diagramas de decisión binarios se utilizan en la verificación simbólica del modelo CTL.
Un diagrama de decisión binaria (BDD) es un gráfico acíclico, como se muestra en la figura opuesta. Se compone de nodos no terminales que llevan preguntas (en el ejemplo, estos son los 5 nodos x1, x2, x2, x3, x3) y como máximo dos nodos terminales etiquetados con 0 y 1. Cada terminal no nodo tiene dos sucesores. , uno con un arco marcado con 1 para 'sí / verdadero' y el otro con un arco marcado con 0 para 'no / falso'. Un diagrama de decisión binario tiene solo un vértice inicial o raíz (en el ejemplo, este es el nodo x1).
Un camino desde la raíz a un nodo terminal representa una asignación de variables (parcial o no): a la variable que etiqueta un nodo se le asigna el valor 0 o 1 dependiendo de si se ha tomado el arco de salida marcado con 0 o 1.
Un BDD representa una función booleana f. Una ruta desde la raíz hasta la terminal 1 representa una asignación de variables (parciales o no) para las cuales la función booleana f mostrada es verdadera. Por ejemplo, para x1 es falso, x2 verdadero y x3 verdadero, entonces la función booleana f es verdadera. Una ruta desde la raíz hasta el terminal 0 representa una asignación de variables (parciales o no) para las que la función booleana f es falsa. Por ejemplo, para x1 es verdadero, x2 es falso, entonces la función booleana f es falsa (independientemente del valor de x3).
Podemos reducir el número de nodos de un BDD aplicando estas dos reglas tantas veces como sea posible:
Un BDD se reduce si ninguna de las dos reglas es aplicable. La figura de enfrente muestra un BDD que no se reduce. Al aplicar las dos reglas tanto como sea posible, nos encontramos con el ejemplo anterior, que se reduce.
Se ordena un BDD si todas las variables aparecen en el mismo orden en todas las rutas desde la raíz hasta los nodos terminales. En el uso común, el término diagrama de decisión binario generalmente se refiere a un diagrama de decisión binario reducido ordenado (ROBDD para diagrama de decisión binario ordenado reducido ).
La ventaja de un ROBDD es que es canónico (único) para una función booleana determinada. Esta propiedad la hace útil, por ejemplo, para la verificación de equivalencia funcional (que da como resultado la igualdad de los ROBDD asociados, que se pueden evaluar en tiempo constante).
El número de nodos en un ROBDD de una función depende del orden de las variables. Las siguientes dos figuras muestran dos ROBDD para la función ƒ ( x 1 , ..., x 8 ) = x 1 x 2 + x 3 x 4 + x 5 x 6 + x 7 x 8 pero uno tiene muchos nodos mientras el otro tiene poco.
Cualquier función booleana simétrica (es decir, cuyo valor no depende del orden de las variables, como la función de paridad o mayoría) admite ROBDD de tamaño O (n 2 ) donde n es el número de variables. Esto debe enfatizarse con el hecho de que la función de paridad y la función de mayoría solo admiten formas conjuntivas normales o formas disyuntivas normales de tamaño exponencial.
Por el contrario, existen funciones booleanas con FNC o DNC pequeño pero con ROBDD de tamaño exponencial, para cualquier orden en las variables, por ejemplo, la función bit ponderado oculto, f (x1, ..., xn) = x x1 + .. . + xn donde x0 = 0 por convención.
El problema de saber si un orden en variables proposicionales es óptimo (es decir, da el ROBDD más pequeño) es NP-difícil.
La construcción de un ROBDD a partir de una fórmula booleana se basa en la expansión de Shannon . La negación se obtiene intercambiando los nodos terminales. Podemos calcular la conjunción y la disyunción de dos ROBDD que tienen el mismo orden en las variables.
Los diagramas de decisión binarios se han extendido a valores arbitrarios en un álgebra finita. La estructura de datos resultante se llama ADD para diagramas de decisión algebraicos y fue introducida por Bahar et al. en 1993. También notamos los diagramas de decisión binarios de terminales múltiples.