SWI-Prolog CLPFD

Question

I'm new to prolog for constraint programming. I have an issue with CLPFD not reducing a domain as I expect it to. This is probably really simple.

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

I expect it to reduce the domain of A and B to

1\/5

But it just gives

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

Any suggestions would be appreciated.

Answer 1

While this answer is tailored to clpfd as implemented in swi-prolog, the idea/method is portable.

:- use_module(library(clpfd)).

Here's how we can reduce domain sizes before starting full enumeration:

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
   ).

We use grammar dom_integers_//1, as defined on the 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).

Sample queries:

?- [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.