Una técnica basada en grafos para representar funciones booleanas como grafos acíclicos dirigidos (diagramas de decisión binaria, BDDs) junto con reglas de reducción (fusionar subgrafos isomorfos y eliminar pruebas redundantes) que pueden producir una forma canónica reducida y ordenada (ROBDD) para un orden de variables fijo, permitiendo comprobaciones eficientes de equivalencia y satisfacibilidad.

Principio

Representar la función como un grafo de decisión y aplicar dos reglas de reducción centrales: (1) fusionar subgrafos isomorfos (tabla única/compartición) y (2) eliminar nodos cuyos hijos low/high son idénticos; con un orden de variables fijo estas reducciones proporcionan una forma canónica de la función booleana.

Demostración

Dada la función booleana f sobre variables x1 < x2 < x3, construir su DAG de decisión completo y luego aplicar la reducción: fusionar subgrafos idénticos y eliminar nodos con sucesores low/high idénticos, obteniendo una ROBDD compacta que puede compararse por igualdad de punteros con otra función bajo el mismo orden para comprobar equivalencia.

Aplicación incorrecta

Asumir que la reducción de BDD siempre produce una representación compacta independiente del orden de variables — en realidad órdenes pobres pueden provocar un crecimiento exponencial; también usar BDDs para funciones que requieren estrategias de descomposición distintas (p. ej. cadenas de acarreo aritmético) sin considerar representaciones alternativas.

Consecuencia

Con un buen orden de variables, la reducción produce una forma canónica que permite prueba de equivalencia en tiempo polinómico y posibilita implementar operaciones booleanas simbólicas de forma eficiente; también sustenta model checking y herramientas de manipulación simbólica.

Inversión

En contraste con CNF-SAT o la enumeración explícita de tablas de verdad: esas técnicas enumeran asignaciones o cláusulas, mientras que BDDs reducidos ofrecen una representación estructurada y compartida; invertir el enfoque sugiere elegir algoritmos basados en enumeración cuando el tamaño del BDD se vuelve intratable.

Límite

Se aplica a funciones booleanas y depende críticamente de un orden de variables fijo; no evita el crecimiento exponencial en el peor caso para ciertas funciones y no es directamente una buena representación para objetos no booleanos o aritméticos de alta aridad sin descomposición.

Tensión semántica

Tensión entre OBDD (ordenado, reducido) y otras representaciones como FBDD (BDD libres), SDDs o codificaciones CNF: los compromisos incluyen canonicidad, sensibilidad al orden de variables y las clases de funciones que cada representación expresa de forma compacta.

Síntesis

La reducción de BDD convierte un proceso de decisión para una función booleana en un grafo compartido canónico al fusionar subgrafos isomorfos y eliminar redundancias bajo un orden de variables fijo; la ROBDD resultante, cuando es pequeña, soporta comprobaciones de equivalencia y operaciones simbólicas eficientes.