SWI-Prolog CLPFD

Question

我是限制性编程的新手.我有一个问题,CLPFD没有像我期望的那样减少域名.这可能很简单.

 [A,B] ins 1..5,A*B#=5.

我希望它能将A和B的域减少到

1\/5

但它只是给出了

A in 1..5,
A*B#=5,
B in 1..5.

任何建议,将不胜感激.

Answer 1

你是对的，1\/5在这种情况下这将是最佳修剪。

然而，出于效率原因，CLP（FD）系统通常仅维护算术约束的所谓边界一致性，并且通常不会从域中删除内部元素，即使其中一些元素无法参与解决方案。

在有限情况下，边界一致性意味着存在变量假定域的下边界和上边界的解。在这种情况下，有A=1和 的解决方案A=5。

请注意，这些是该具体情况下的唯一解决方案，但一般来说，在类似的较大实例中也存在具有内点的解决方案，例如：

?- [A,B] ins 1..10，A*B#=10，标签([A,B])。
A = 1,
B=10；
A = 2,
B=5；
A = 5,
B=2；
A = 10,
B = 1。

不过好消息是，此类解决方案的数量仅随着域的大小呈对数增长：

?- length(_, Exp), N #= 2^Exp, [A,B] ins 1..N,A*B#=N,
   findall(., label([A,B]), Ls), length(Ls, L),
   writeln(Exp-L), false.
0-1
1-2
2-3
3-4
4-5
5-6
6-7
7-8
etc.

这与其他情况相反，例如X mod 2 #= 0，解的数量随着 的域的大小线性X增长（因此其十进制表示的长度呈指数增长），因此显式修剪域是不可行的。

因此，作为一种可行的解决方法，您可以使用label/1来获得具体的解决方案，然后使用in/2约束将操作数限制在其具体允许的范围内：

:- use_module(library(clpfd)).

stricter_domains(Vs) :-
        findall(Vs, label(Vs), Sols0),
        transpose(Sols0, Sols),
        maplist(list_to_domain, Sols, Ds),
        maplist(in, Vs, Ds).

list_to_domain([L|Ls], Dom) :- foldl(dom_disj, Ls, L, Dom).

dom_disj(D0, I, D0\/I).

你的例子：

?- [A,B] ins 1..5，A*B#=5，更严格的域([A,B])。
A 的 1\/5，
A*B#=5,
B 为 1\/5。