En informática , un diagrama de decisión binario ( BDD ) o 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. Otras estructuras de datos utilizadas para representar funciones booleanas incluyen la forma normal de negación (NNF), polinomios de Zhegalkin ygráficos acíclicos dirigidos proposicionales (PDAG).
Definición
Una función booleana se puede representar como un gráfico acíclico, dirigido y enraizado , 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 niño bajo y niño alto. El borde del nodo a un niño 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 se 'reduce' si se han aplicado las siguientes dos reglas a su gráfico:
- Fusionar los subgrafos isomorfos .
- Elimine cualquier nodo cuyos dos hijos sean isomorfos.
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 los aspectos de ordenamiento y reducción necesitan ser enfatizados). La ventaja de un ROBDD es que es canónico (único) para una función particular y un 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 al 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 hijo bajo (o alto) de un nodo, la variable de ese nodo se asigna a 0 (respectivamente 1).
Ejemplo
La figura de la izquierda a continuación muestra un árbol de decisión binario (las reglas de reducción no se aplican) y una tabla de verdad , cada uno representando 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 una ruta hacia abajo en el gráfico hasta una terminal. En las figuras siguientes, las líneas de puntos representan los bordes de un niño bajo, mientras que las líneas continuas representan los bordes de 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 a 0), luego dos líneas continuas hacia abajo (ya que x2 y x3 tienen cada una una asignación a uno). Esto conduce a la terminal 1, que es el valor de.
El árbol de decisión binario de la figura de la izquierda se puede transformar en un diagrama de decisión binario reduciéndolo al máximo de acuerdo con las dos reglas de reducción. El BDD resultante se muestra en la figura de la derecha.
Otra notación para escribir esta función booleana es .
Bordes complementados
Un ROBDD se puede representar de forma aún más compacta, utilizando bordes complementados. [2] [3] Los bordes complementados se forman anotando los bordes bajos como complementados o no. Si se complementa una arista, entonces se refiere a la negación de la función booleana que corresponde al nodo al que apunta la arista (la función booleana representada por el BDD con raíz en ese nodo). Los bordes altos no se complementan para garantizar que la representación BDD resultante sea una forma canónica. En esta representación, los BDD tienen un solo nodo hoja, por las razones que se explican a continuación.
Dos ventajas de utilizar aristas complementadas al representar BDD son:
- calcular la negación de un BDD lleva un tiempo constante
- se reduce el uso de espacio (es decir, la memoria requerida)
Una referencia a un BDD en esta representación es un "borde" (posiblemente complementado) que apunta a la raíz del BDD. Esto contrasta con una referencia a un BDD en la representación sin el uso de bordes complementados, que es el nodo raíz del BDD. La razón por la que una referencia en esta representación debe ser un borde es que para cada función booleana, la función y su negación están representadas por un borde a la raíz de un BDD y un borde complementado a la raíz del mismo BDD. Por eso la negación requiere un tiempo constante. También explica por qué un solo nodo de hoja es suficiente: FALSO está representado por un borde complementado que apunta al nodo de hoja, y VERDADERO está representado por un borde ordinario (es decir, no complementado) que apunta al nodo de hoja.
Por ejemplo, suponga que una función booleana se representa con un BDD representado mediante aristas complementadas. Para encontrar el valor de la función booleana para una asignación dada de valores (booleanos) a las variables, comenzamos en el borde de referencia, que apunta a la raíz del BDD, y seguimos la ruta definida por los valores de variable dados (siguiendo un borde bajo si la variable que etiqueta un nodo es FALSO, y siguiendo el borde alto si la variable que etiqueta un nodo es VERDADERO), hasta llegar al nodo hoja. Mientras seguimos este camino, contamos cuántos bordes complementados hemos atravesado. Si al llegar al nodo hoja hemos cruzado un número impar de aristas complementadas, entonces el valor de la función booleana para la asignación de variable dada es FALSO, en caso contrario (si hemos cruzado un número par de aristas complementadas), entonces el valor de la función booleana para la asignación de variable dada es VERDADERA.
Un diagrama de ejemplo de un BDD en esta representación se muestra a la derecha y representa la misma expresión booleana que se muestra en los diagramas de arriba, es decir, . Los bordes bajos son discontinuos, los bordes altos son sólidos y los bordes complementados se indican con una etiqueta "-1". El nodo cuya etiqueta comienza con un símbolo @ representa la referencia al BDD, es decir, el borde de referencia es el borde que comienza desde este nodo.
Historia
La idea básica a partir de la cual se creó la estructura de datos es la expansión de Shannon . Una función de conmutación se divide en dos subfunciones (cofactores) asignando una variable (cf. forma normal if-then-else ). Si dicha subfunción se considera un subárbol, puede representarse mediante un árbol de decisión binario . Lee introdujo los diagramas de decisión binaria (BDD), [4] y Akers [5] y Boute los estudiaron más a fondo y los dieron a conocer . [6] Independientemente de estos autores, se realizó un BDD bajo el nombre de "forma canónica de corchetes" Mamrukov en un CAD para el análisis de circuitos independientes de la velocidad. [7] Randal Bryant en la Universidad Carnegie Mellon investigó todo el potencial de los algoritmos eficientes basados en la estructura de datos : sus extensiones clave eran usar un orden de variable fija (para representación canónica) y subgráficos compartidos (para compresión). La aplicación de estos dos conceptos da como resultado una estructura de datos y algoritmos eficientes para la representación de conjuntos y relaciones. [8] [9] Al extender la compartición a varios BDD, es decir, varios BDD utilizan un subgráfico, se define la estructura de datos del Diagrama de decisión binario ordenado reducido compartido . [2] La noción de un BDD ahora se usa generalmente para referirse a esa estructura de datos en particular.
En su video conferencia Fun With Binary Decision Diagrams (BDD) , [10] Donald Knuth llama a los BDD "una de las únicas estructuras de datos realmente fundamentales que surgieron en los últimos veinticinco años" y menciona que el artículo de Bryant de 1986 fue durante algún tiempo uno de los artículos más citados en informática.
Adnan Darwiche y sus colaboradores han demostrado que los BDD son una de varias formas normales de funciones booleanas, cada una inducida por una combinación diferente de requisitos. Otra forma normal importante identificada por Darwiche es la forma normal de negación descomponible o DNNF.
Aplicaciones
Los BDD se utilizan ampliamente en software CAD para sintetizar circuitos ( síntesis lógica ) y en verificación formal . Hay varias aplicaciones menos conocidas de BDD, incluido el análisis de árboles de fallas , el razonamiento bayesiano , la configuración del producto y la recuperación de información privada . [11] [12] [ cita requerida ]
Cada BDD arbitrario (incluso si no está reducido u ordenado) se puede implementar directamente en hardware reemplazando cada nodo con un multiplexor 2 a 1 ; cada multiplexor puede ser implementado directamente por un 4-LUT en un FPGA . No es tan simple convertir de una red arbitraria de puertas lógicas a un BDD [ cita requerida ] (a diferencia del gráfico e-inversor ).
Orden variable
El tamaño del BDD está determinado tanto por la función que se representa como por el orden elegido de las variables. Existen funciones booleanaspara lo cual, dependiendo del orden de las variables, terminaríamos obteniendo un gráfico cuyo número de nodos sería lineal (en n ) en el mejor de los casos y exponencial en el peor de los casos (por ejemplo, un sumador de acarreo de rizado ). Considere la función booleana Usando el orden de variables , el BDD necesita nodos para representar la función. Usando el pedido, el BDD consta de nodos.
Es de crucial importancia cuidar el orden de las variables al aplicar esta estructura de datos en la práctica. El problema de encontrar el mejor orden de variables es NP-difícil . [13] Para cualquier constante c > 1 es incluso NP-difícil calcular el orden de una variable que da como resultado un OBDD con un tamaño que es como máximo c veces mayor que el óptimo. [14] Sin embargo, existen heurísticas eficientes para abordar el problema. [15]
Hay funciones para las que el tamaño del gráfico es siempre exponencial, independientemente del orden de las variables. Esto es válido, por ejemplo, para la función de multiplicación. [1] De hecho, la función que calcula el bit medio del producto de dos-números de bits no tienen un OBDD menor que vértices. [16] (Si la función de multiplicación tuviera OBDD de tamaño polinomial, mostraría que la factorización de enteros está en P / poli , lo cual no se sabe si es cierto. [17] )
Los investigadores han sugerido refinamientos en la estructura de datos BDD dando paso a una serie de gráficos relacionados, como BMD ( diagramas de momento binario ), ZDD ( diagrama de decisión con supresión de cero ), FDD ( diagramas de decisión binarios libres ), PDD ( diagramas de decisión de paridad ) y MTBDD (BDD de múltiples terminales).
Operaciones lógicas en BDD
Muchas operaciones lógicas en BDD se pueden implementar mediante algoritmos de manipulación de gráficos de tiempo polinomial: [18] : 20
- conjunción
- disyunción
- negación
Sin embargo, repetir estas operaciones varias veces, por ejemplo, formando la conjunción o disyunción de un conjunto de BDD, puede en el peor de los casos dar como resultado un BDD exponencialmente grande. Esto se debe a que cualquiera de las operaciones anteriores para dos BDD puede dar como resultado un BDD con un tamaño proporcional al producto de los tamaños de los BDD y, en consecuencia, para varios BDD el tamaño puede ser exponencial. Además, dado que la construcción del BDD de una función booleana resuelve el problema de satisfacibilidad booleana NP-completo y el problema de tautología co-NP-completa , la construcción del BDD puede llevar un tiempo exponencial en el tamaño de la fórmula booleana incluso cuando el BDD resultante es pequeño.
Calcular la abstracción existencial sobre múltiples variables de BDD reducidos es NP-completo. [19]
El recuento de modelos, contando el número de asignaciones satisfactorias de una fórmula booleana, se puede realizar en tiempo polinómico para BDD. Para fórmulas proposicionales generales, el problema es ♯P -completo y los algoritmos más conocidos requieren un tiempo exponencial en el peor de los casos.
Ver también
- Problema de satisfacibilidad booleano , el problema computacional NP-completo canónico
- L / poly , una clase de complejidad que contiene estrictamente el conjunto de problemas con BDD de tamaño polinomial [ cita requerida ]
- Comprobación de modelo
- Árbol de radix
- Teorema de Barrington
- Aceleracion de hardware
- Mapa de Karnaugh , un método para simplificar expresiones de álgebra booleana
Referencias
- ^ a b Algoritmos basados en gráficos para la manipulación de funciones booleanas, Randal E. Bryant, 1986
- ^ a b Karl S. Brace, Richard L. Rudell y Randal E. Bryant. " Implementación eficiente de un paquete BDD" . En Proceedings of the 27th ACM / IEEE Design Automation Conference (DAC 1990), páginas 40–45. IEEE Computer Society Press, 1990.
- ^ Fabio Somenzi, " Diagramas de decisión binaria ", Diseño de sistemas de cálculo, Vol.173, Serie F de la ciencia de la OTAN: Ciencias de la computación y sistemas, págs. 303-366, IOS Press, 1999
- ^ CY Lee. "Representación de circuitos de conmutación mediante programas de decisión binaria". Bell System Technical Journal, 38: 985–999, 1959.
- ^ Sheldon B. Akers, Jr .. Diagramas de decisión binaria, IEEE Transactions on Computers, C-27 (6): 509–516, junio de 1978.
- ^ Raymond T. Boute, "La máquina de decisión binaria como controlador programable". Boletín EUROMICRO , Vol. 1 (2): 16-22, enero de 1976.
- ^ Yu. V. Mamrukov, Análisis de circuitos aperiódicos y procesos asincrónicos. Doctor. disertación. Instituto Electrotécnico de Leningrado, 1984, 219 p.
- ^ Randal E. Bryant. " Algoritmos basados en gráficos para la manipulación de funciones booleanas ". IEEE Transactions on Computers, C-35 (8): 677–691, 1986.
- ^ Randal E. Bryant, " Manipulación booleana simbólica con diagramas de decisión binarios ordenados" , Encuestas de computación de ACM, vol. 24, No. 3 (septiembre de 1992), págs. 293–318.
- ^ "Centro de Stanford para el desarrollo profesional" . scpd.stanford.edu . Archivado desde el original el 4 de junio de 2014 . Consultado el 23 de abril de 2018 .
- ^ RM Jensen. "CLab: una biblioteca C + + para una configuración de producto interactiva rápida y sin retrocesos" . Actas de la Décima Conferencia Internacional sobre Principios y Práctica de la Programación de Restricciones, 2004.
- ^ HL Lipmaa. "Primer protocolo CPIR con cálculo dependiente de datos" . ICISC 2009.
- ^ Beate Bollig, Ingo Wegener. La mejora del orden variable de los OBDD es NP-Complete , IEEE Transactions on Computers, 45 (9): 993–1002, septiembre de 1996.
- ^ Detlef Sieling. "La falta de aproximación de la minimización de OBDD". Información y computación 172, 103-138. 2002.
- ^ Rice, Michael. "Un estudio de la heurística de ordenamiento de variables estáticas para una construcción eficiente de BDD / MDD" (PDF) .
- ^ Philipp Woelfel. " Límites en el tamaño OBDD de la multiplicación de enteros a través de hash universal ". Revista de Ciencias de la Computación y Sistemas 71, págs. 520-534, 2005.
- ^ Richard J. Lipton . "BDD's y Factoring" . Letra perdida de Gödel y P = NP , 2009.
- ^ Andersen, HR (1999). "Introducción a los diagramas de decisión binarios" (PDF) . Notas de la conferencia . Universidad de TI de Copenhague.
- ^ Huth, Michael; Ryan, Mark (2004). Lógica en informática: modelado y razonamiento sobre sistemas (2 ed.). Cambridge [Reino Unido]: Cambridge University Press. págs. 380–. ISBN 978-0-52154310-1. OCLC 54960031 .
Otras lecturas
- R. Ubar, "Generación de pruebas para circuitos digitales utilizando gráficos alternativos (en ruso)", en Proc. Universidad Técnica de Tallin, 1976, Nº 409, Universidad Técnica de Tallin, Tallin, Estonia, págs. 75–81.
- DE Knuth, " El arte de la programación informática, volumen 4, fascículo 1: trucos y técnicas bit a bit; diagramas de decisión binaria" (Addison-Wesley Professional, 27 de marzo de 2009) viii + 260pp, ISBN 0-321-58050-8 . Borrador del Fascículo 1b disponible para descargar.
- Ch. Meinel, T. Theobald, " Algoritmos y estructuras de datos en VLSI-Design: OBDD - Fundamentos y aplicaciones" , Springer-Verlag, Berlín, Heidelberg, Nueva York, 1998. Libro de texto completo disponible para descargar.
- Ebendt, Rüdiger; Fey, Görschwin; Drechsler, Rolf (2005). Optimización avanzada de BDD . Saltador. ISBN 978-0-387-25453-1.
- Becker, Bernd; Drechsler, Rolf (1998). Diagramas de decisión binaria: teoría e implementación . Saltador. ISBN 978-1-4419-5047-5.
enlaces externos
- Diversión con diagramas de decisión binaria (BDD) , conferencia de Donald Knuth
- Lista de bibliotecas de software BDD para varios lenguajes de programación.