use_module(library(clpfd)).
CLPFD seems to not be very quick in realizing that in
length(L, 9), L ins 1..9, all_distinct(L), foreach(label(L), sum(L, #=, X))
X=45.
(I tried length(L, 4), all_distinct(L), L ins 1..4, sum(L, #=, X), label([X]). which tries to inform me that 1 + 2 + 3 + 4 = 7, so I might be misunderstanding something).
length(L, 9), L ins 1..9, all_distinct(L), bagof(L, label(L), Ls), length(Ls, X).
Which should give X = 362880. has a similar problem.
Both seem to perform in O(N!) with length(L, N), which is of course because we are enumerating
every possible permutation of L to reach our conclusion.
These edge cases could of course be replaced with the simpler solutions we can derive ourself everywhere we use them.
But for example it would be nice to be able have CLPFD be able to reason that in
length(L, N - 1), L ins 1..N, all_distinct(L)
we can calculate sum(L, #=, X) to have X in N (N - 1) / 2 - N..N (N - 1) / 2 - 1.
Am I missing some aspect of CLPFD or a predicate that counts labellings without enumerating them,
and a way to make CLPFD aware of the pigeonhole principle + associativity + commutativity of sum,
or do I write predicates for these specific cases?
In SWI Prolog 8.1:
I'm not too knowledgeable you seem "label" too early or too eagerly ("foreach of the labelings" smells fishy)
Try
?- length(L, 9), L ins 1..9, all_distinct(L), sum(L, #=, X), X = 45, label(L).
Immediately returns with
L = [1, 2, 3, 4, 5, 6, 7, 8, 9],
X = 45
Similar with
?- length(L, 4), all_distinct(L), L ins 1..4, sum(L, #=, X), label(L).
which gives
L = [1, 2, 3, 4],
X = 10 ;
I'm not sure what happens here, but again label([X]) doesn't sound right.
?- 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 ;
I do think CLP(FD) has not noticed that the above solution has no solutions as it outputs the constraints only.
But try
?- length(L, 4), all_distinct(L), L ins 1..4, sum(L, #=, X), label([X]), label(L).
L = [1, 2, 3, 4],
X = 10
Correct.
But for example it would be nice to be able have CLPFD be able to reason that in length(L, N - 1), L ins 1..N, all_distinct(L) we can calculate sum(L, #=, X) to have X in N (N - 1) / 2 - N..N (N - 1) / 2 - 1.
Definitely general theorem proving over integer arithmetic, rather than constraint propagation. It would be nice but I don't think it goes that far.