prolog - 在 Prolog 中通过 Quine 算法计算估值的数量

Question

我的逻辑老师顺便说，Quines算法 也可以用来计算估值。不幸的是，我无法理解在 Prolog 中这是如何完成的？

例如，该程序将使用
Quines 算法中答案的语法给出：

?- sat_count(X+Y, C).
C = 3

由于析取 X+Y 的真值表
有 3 行的值为真：

X   Y   X+Y
0   0   0
0   1   1
1   0   1
1   1   1

Answer 1

出发点是 Quines 算法，其核心谓词 eval/2 具有以下规范。可以在这里找到 Quine 算法的源代码和问题的解决方案。

/**
 * eval(A, R):
 * The predicate succeeds in R with a partial evaluated
 * Boolean formula. The predicate starts with the leaves
 * and calls simp after forming new nodes.
 */
% eval(+Formula, -Formula)

我们首先尝试了一个标签谓词，它将列出所有估值而不计算它们。谓词有一个快速失败的特性，如果部分评估的公式为假（0），则不需要进行标记，否则我们只需探测布尔值：

/**
 * labeling(L, A):
 * The predicate labels the variables from the list L in the formula A.
 */
% labeling(+List, +Formula)
labeling(_, A) :- A == 0, !, fail.
labeling([X|L], A) :- value(X), eval(A, B), labeling(L, B).
labeling([], A) :- A == 1.

这是一个示例运行：

?- labeling([X,Y], X+Y).
X = 0,
Y = 1 ;
X = 1,
Y = 0 ;
X = 1,
Y = 1

从标签谓词中，我们使用 ISO 核心标准中的 findall/3 导出了一个计数谓词。我们不是在最后成功返回 1，而是在两者之间对计数求和。这可以完成工作，也可以从快速失败中获益：

/**
 * count(L, A, N):
 * The predicate silently labels the variables from the list L in the
 * formula A and succeeds in N with the count of the solutions.
 */
% count(+List, +Formula, -Integer)
count(_, A, C) :- A == 0, !, C = 0.
count([X|L], A, D) :-
   findall(C, (value(X), eval(A, B), count(L, B, C)), R),
   sum(R, 0, D).
count([], A, 1) :- A == 1.

这是一个示例运行：

?- count([X,Y], X+Y, C).
C = 3

实现可能会受益于我们没有实现的一些优化。例如，将值分配给公式中不再出现的变量可以被优化掉。