ZDD with Quantification in Prolog

Question

What would be the ZDD approach in Prolog that also provides quantifiers.
Notation for existential quantifier would be as follows:

  X^F

where X is the bound variable and F is the formula. It corresponds
to the following formula:

  F[X/0] v F[X/1]

How would one go about and write a Prolog routine that takes a ZDD
for F and a variable X and produces the ZDD for X^F ?

Answer 1

Daniel Pehoushek posted some interesting C-code, which I translated to Prolog. Its not directly working with ZDD, but rather with sets of sets of variables, which is also explained here. But I guess the algorithm can be translated from sets of sets of variables to ZDD.

It only needs two new operations, the rest works with the operations from library(lists). One operation is split/4 which gives the left and right branch for a tree root. And the other operation is join/4 which does the inverse. The main routine is bob/3:

bob(_, [], []) :- !.
bob([], A, A).
bob([V|W], A, T) :-
   split(A, V, L, R),
   intersection(L, R, H),
   bob(W, H, P),
   union(L, R, J),
   bob(W, J, Q),
   join(V, P, Q, T).

What does bob do? It transforms a formula P into a formula Q. The original formula P has propositional variables x1,..,xn. The resulting formulas has propositional variables x1',..,xn' which act as switches, where xi'=0 means ∀xi and xi'=1 means ∃xi. So the desired quantification result can be read off in the corresponding truth table row of Q.

Lets make an example:

P = (- A v B) & (-B v C)
Q = (A' v B') & (B' v C') & (A' v C')

A'B'C' Q
000 0
001 0
010 0
011 1 eg: (All A)(Exists B)(Exists C) P
100 0
101 1
110 1
111 1

Or as a Prolog call, computing Q from P for the above example:

?- bob([c,b,a], [[],[c],[b,c],[a,b,c]], A).
A = [[b, a], [c, a], [c, b], [c, b, a]]

Open source:

Some curious transformation by Daniel Pehoushek
https://gist.github.com/jburse/928f060331ed7d5307a0d3fcd6d4aae9#file-bob-pl