Intersección de BDD con supresión de ceros: implementación de polinomios utilizando ZDD

Question

Estoy intentando implementar polinomios univariados usando ZDD, como se sugiere en un comentario en un otra pregunta.

He leído el artículo de S.Minato (puedes descargarlo) aquí), pero no entiendo cómo implementar las operaciones en estos ZDD.

La idea en el artículo es que los polinomios se pueden representar usando x^(2^i) como variables.Por ejemplo x^5 + x^3 + x se puede reescribir como x^4x^1 + x^2x^1 + x^1, si crea nodos para cada uno x^(2^i) variable y conectar con las variables de "borde 1" que se multiplican y con las variables de "borde 0" que se suman puedes obtener fácilmente una gráfica que represente ese polinomio.Los ZDD son gráficos de este tipo que imponen alguna condición en el gráfico (para más información lea el artículo de Minato y el de wikipedia). página en BDD)

Los coeficientes se pueden representar de manera similar usando sumas de potencias de 2 (p. ej. 5 = 2^2 + 2^0 etc.Con todo 2^i siendo una variable y los nodos están conectados con los bordes 1 y 0 de la misma manera).

Ahora, mi problema es el algoritmo para la suma de dos ZDD.El algoritmo parece bastante simple:

Si F y G (ZDDS) no tienen combinaciones comunes, la adición (F + G) se puede completar simplemente fusionándolas.Cuando contienen algunas combinaciones comunes, calculamos las siguientes fórmulas:(F + g) = s + (cx2), donde c = f ∩ g, s = (fug) c.Al repetir este proceso, las combinaciones comunes finalmente se agotan y el procedimiento se completa.

El problema es:¿Cómo puedo encontrar "C" y "S" de manera eficiente?

El autor proporciona código para la multiplicación, pero el código en realidad es trivial una vez que tengas implementados los algoritmos anteriores.Y como estos algoritmos no se proporcionan, el de multiplicación es "inútil".

Además, la noción de "fusionar" ZDD no está bien explicada, aunque, considerando el hecho de que el orden de las variables debe ser consistente, sólo hay una manera de fusionar los gráficos, y las reglas para mantener este orden probablemente sean simples. suficientes (todavía no los he formalizado, pero tengo una idea aproximada de lo que son).

Answer 1

Con "fusionar" Minato significa unión. (algoritmo).También puedes ver esto en el ejemplo:

4 * y     = { { 2^2, y } }
x         = { { x } }
4 * y + x = { { 2^2, y }, { x } }

La idea es que los conjuntos internos representan productos y el ZDD completo representa la suma de esos productos, por lo que si simplemente realiza OR (también conocido como unión o fusión) en algunos conjuntos más, se agregan efectivamente.

El algoritmo de suma completo en realidad simplemente hace (A xor B) + 2 * (A and B) (recursivamente) que es equivalente al conocido algoritmo de suma bit a bit, pero el xor fue escrito como (A or B) without (A and B).

Eso también hace obvio por qué está bien simplemente tomar la unión cuando no hay combinaciones comunes - si A and B esta vacio, A xor B es lo mismo que A or B y el "carry" es cero.

Los algoritmos para OR, AND, XOR y BUTNOT se explican en detalle en The Art of Computer Programming volumen 4, sección 7.1.4 (La respuesta a la pregunta 199 es relevante).La idea general para todos ellos es que consideren los dos subgrafos que representan todos los conjuntos. con La variable v y todos los conjuntos sin La variable v por separado (que se encuentran trivialmente si v es la variable superior en uno o ambos argumentos, ya sea como hijos bajos y altos o como la entrada misma), y luego combina el resultado.

Union(F, G) =
  if (F = ∅) return G
  if (G = ∅) return F
  if (F = G) return F
  if (cache contains "F ∪ G" or "G ∪ F")
    return cached value

  if (F.v = G.v) result = MakeNode(F.v, F.lo ∪ G.lo, F.hi ∪ G.hi)
  if (F.v > G.v) result = MakeNode(G.v, F ∪ G.lo, G.hi)
  if (F.v < G.v) result = MakeNode(F.v, F.lo ∪ G, F.hi)

  cache result as "F ∪ G"
  return result

Intersect(F, G) =
  if (F = ∅ or G = ∅) return ∅
  if (F = G) return F
  if (cache contains "F ∩ G" or "G ∩ F")
    return cached value

  if (F.v = G.v) result = MakeNode(F.v, F.lo ∩ G.lo, F.hi ∩ G.hi)
  if (F.v > G.v) result = F ∩ G.lo
  if (F.v < G.v) result = F.lo ∩ G

  cache result as "F ∩ G"
  return result