SWI-Prolog CLPFD

Question

我是 prolog 约束编程的新手。我有一个 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

虽然这个答案是针对 clpfd 量身定制的，如在 swi-prolog 中实现的那样，但这个想法/方法是可移植的。

:- use_module(library(clpfd))。

以下是我们如何在开始完全枚举之前减小域大小：

shave_zs(Zs) :-
   maplist(flag_zs_shave_z(F,Zs), Zs),
   once((var(F) ; ground(Zs) ; shave_zs(Zs))).

flag_zs_shave_z(Flag, Zs, Z) :-
   (  fd_size(Z, sup)
   -> true                                    % never shave the infinite
   ;  fd_dom(Z, Z_dom),
      phrase(dom_integers_(Z_dom), Z_vals),
      maplist(flag_zs_z_val(Flag,Zs,Z), Z_vals)
   ).

flag_zs_z_val(Flag, Zs, Z, Z_val) :-
   (  \+ call_with_inference_limit((Z #= Z_val,labeling([],Zs)), 1000, _)
   -> Z #\= Z_val,
      Flag = true
   ;  true
   ).

我们使用语法 dom_integers_//1，正如 SWI-Prolog clpfd manual page 中定义的那样：

dom_integers_(I)      --> { integer(I) }, [I].
dom_integers_(L..U)   --> { numlist(L, U, Is) }, Is.
dom_integers_(D1\/D2) --> dom_integers_(D1), dom_integers_(D2).

示例查询：

?- [A,B] ins 1..5,  A*B #= 5,  (Shaved = false ; Shaved = true, shave_zs([A,B])).
Shaved = false, A*B #= 5, A in 1..5, B in 1..5 ;
Shaved =  true, A*B #= 5, A in 1\/5, B in 1\/5.

?- [A,B] ins 1..10, A*B #= 10, (Shaved = false ; Shaved = true, shave_zs([A,B])).
Shaved = false, A*B #= 10, A in 1..10      , B in 1..10 ;
Shaved =  true, A*B #= 10, A in 1..2\/5\/10, B in 1..2\/5\/10.

Answer 2

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

但是，出于效率原因，CLP(FD) 系统通常只为算术约束维护所谓的边界一致性，并且通常不会从域中删除内部元素，即使其中一些元素不能参与在解决方案中。

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

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

?- [A,B] ins 1..10, A*B#=10, label([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, stricter_domains([A,B])。 1/5 中的 A, A*B#=5, 1\/5 中的 B。