【问题标题】：Count solutions in a CSP计算 CSP 中的解决方案
【发布时间】：2016-11-21 14:57:13
【问题描述】：

我正在使用 prolog，我有这个代码：

:- use_module(library(clpb)).

fun(A, B, C, D, E) :-
  sat(A + B + C + D),
  sat(E),
  labeling([A, B, C, D, E]).

如果我想计算所有解决方案，我该怎么做？我已经阅读了关于 clpb 中使用的 sat_count(+Expr, -Count) 但我无法在没有错误的情况下实现它

【问题讨论】：

据我所知，CLPB 中的 sat/2 不存在。此外，您的规则应以句点而不是分号结尾。
我编辑了代码。无论如何 sat_count(+Expr, -Count) 在 SWI-Prolog 手册中。 eu.swi-prolog.org/man/clpb.html
当然，但sat(A + B + C, D)，或更一般的sat(X, D) 不是。
哦，对不起，这是一个+。我忘记放了

【解决方案1】：

蛮力方法

计算解决方案数量的一种直接方法是生成它们，然后看看有多少。

例如，对于您发布的程序，我们可以使用findall/3 获取答案：

?- findall(., fun(A, B, C, D, E), Ls), 长度（Ls，L）。 Ls = ['.', '.', '.', '.', '.', '.', '.', '.', '.'|...], L = 15。

当然，这种扩展性相当糟糕，并且在更复杂的情况下很快变得不可行。不过，在这个例子中，这个策略就足够了。

备选：`sat_count/2`

对于 CLP(B)，我们有您已经发现的 sat_count/2。

sat_count/2 的主要优点是我们可以计算解决方案的数量而不用枚举它们。当有很多解决方案时，这当然非常方便。

使用sat_count/2 的技巧是避免 labeling/1，并以仅发布约束的方式编写您的核心关系。

例如：

有趣（A、B、C、D、E）：- 坐（A + B + C + D），饱和（E）。

这有几个优点。首先，我们现在可以查询：

?- 有趣（A、B、C、D、E）。 E = 1, 坐（A=\= ... # ... # B#B*C#B*C*D#B*D#C#C*D#D）。

这个答案表明E必然是 1！如果我们使用 labeling/1，这会有点难以看到。

此外，在发布相关约束后，我们可以使用sat_count/2，通过提供一个必须计算为真值的 CLP(B) 表达式作为第一个参数。

在我们的例子中，我们不想对解决方案施加进一步的限制，因此我们将包含我们感兴趣的变量的重言式指定为第一个参数。一个合适的习语是+[1|Vs].

所以，我们可以使用：

?- 有趣（A、B、C、D、E）， sat_count(+[1,A,B,C,D,E], 计数)。 E = 1, 计数 = 15, 坐（A=\= ... # ... # B#B*C#B*C*D#B*D#C#C*D#D）。

在这种特定情况下，解决方案的数量非常少，以至于两种方法之间几乎没有区别。

不过，我想在编写约束逻辑程序时强调一个重要的一般原则：

将核心关系从实际搜索中分离以寻找解决方案（labeling/1 和类似的谓词，内置的和手动编写的）是一种很好的做法。

如果您遵守此原则，您可以单独研究约束的终止和传播。

此外，这允许您在不重新编译程序的情况下尝试不同的搜索策略！

【讨论】：