让Prolog的CLPFD意识到排列组合和其他对称性。

Question

use_module(library(clpfd)).

中电联似乎还没有很快意识到，在这一问题上。

length(L, 9), L ins 1..9, all_distinct(L), foreach(label(L), sum(L, #=, X))
X=45.

(我试过了 length(L, 4), all_distinct(L), L ins 1..4, sum(L, #=, X), label([X]). 它试图告诉我 1 + 2 + 3 + 4 = 7所以我可能误解了什么）。)

length(L, 9), L ins 1..9, all_distinct(L), bagof(L, label(L), Ls), length(Ls, X).

这应该给 X = 362880. 有一个类似的问题。

两者似乎都是在O(N!)的情况下进行的。length(L, N)当然，这是因为我们正在列举每一种可能的排列组合，即 L 来得出我们的结论。

这些边缘情况当然可以用更简单的解决方案来代替，我们可以在使用它们的任何地方自己推导出它们.但例如，如果能够让CLPFD能够推理出在length(L, N - 1), L ins 1..N, all_distinct(L)我们可以计算 sum(L, #=, X) 具备 X in N (N - 1) / 2 - N..N (N - 1) / 2 - 1.

我是不是漏掉了CLPFD的某些方面，或者漏掉了一个不列举标签而计算标签的谓词，以及一个让CLPFD意识到鸽子洞原则+关联性+换位性的方法。sum还是要为这些特殊情况写谓词？

Answer 1

在SWI Prolog 8.1中。

我不太懂你的意思 你似乎太早或太急于 "贴标签 "了（"foreach of the labelings "闻起来有股腥味）

试试

?- length(L, 9), L ins 1..9, all_distinct(L), sum(L, #=, X), X = 45, label(L).

立即返回与

L = [1, 2, 3, 4, 5, 6, 7, 8, 9],
X = 45 

类似于

?- length(L, 4), all_distinct(L), L ins 1..4, sum(L, #=, X), label(L).

由此可见

L = [1, 2, 3, 4],
X = 10 ;

我不知道这里发生了什么，但再次 label([X]) 听起来不对。

?- length(L, 4), all_distinct(L), L ins 1..4, sum(L, #=, X), label([X]).
L = [_7950, _7956, _7962, _7968],
X = 7,
_7950 in 1..4,
_7950+_7956+_7962+_7968#=7,
all_distinct([_7950, _7956, _7962, _7968]),
_7956 in 1..4,
_7962 in 1..4,
_7968 in 1..4 ;

我确实认为CLP(FD)没有注意到上面的解决方案没有解，因为它只输出约束条件。

但可以试试

?- length(L, 4), all_distinct(L), L ins 1..4, sum(L, #=, X), label([X]), label(L).
L = [1, 2, 3, 4],
X = 10 

正确的，但是如果能让CLPFD能够推理出在length(L, N - 1, L ins 1...N, all_distinct(L)中，我们可以计算sum(L)

但比如能够让CLPFD能够推理出在length(L，N - 1)中，L ins 1...N，all_distinct(L)中，我们可以计算sum(L，#=，X)有X在N(N - 1) 2 - N...N (N - 1) 2 - 1中。

肯定是在整数算术上的一般定理证明，而不是约束传播。这很好，但我认为它没有走到那一步。