在 Prolog 中进行量化的 ZDD

Posted 2023-03-28

【中文标题】在 Prolog 中进行量化的 ZDD

【英文标题】：ZDD with Quantification in Prolog

【发布时间】：2020-11-22 21:44:18

【问题描述】：

Prolog 中还提供量词的 ZDD 方法是什么。 存在量词的符号如下：

  X^F

其中 X 是绑定变量，F 是公式。它对应 如下公式：

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

如何编写一个需要 ZDD 的 Prolog 例程 对于 F 和变量 X 并为 X^F 生成 ZDD？

【问题讨论】：

世界上能够理解这一点的 12 个人中的一个很快就会回答！

和***.com/questions/63265943/… 一样，只适用于 Prolog。

【参考方案1】：

Daniel Pehoushek 发布了一些有趣的 C 代码，我将其翻译成 Prolog。它不是直接使用 ZDD，而是使用变量集，here 也对此进行了解释。但我猜该算法可以从变量集转换为 ZDD。

它只需要两个新操作，其余的与库（列表）中的操作一起使用。一种操作是 split/4，它为树根提供左右分支。另一个操作是 join/4 ，它执行相反的操作。主程序是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).

鲍勃是做什么的？它将公式 P 转换为公式 Q。原始公式 P 具有命题变量 x1,..,xn。得到的公式具有命题变量 x1',..,xn'，它们充当开关，其中 xi'=0 表示∀xi，xi'=1 表示∃xi。所以想要的量化结果可以在Q对应的真值表行中读出。

举个例子：

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

或者作为 Prolog 调用，从 P 计算 Q 以用于上述示例：

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

开源：

Daniel Pehoushek 的一些奇怪转变https://gist.github.com/jburse/928f060331ed7d5307a0d3fcd6d4aae9#file-bob-pl