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.

Stepfather

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.

Ellerey

Answer 2

You are right that 1\/5 would be optimal pruning in this case.

However, for efficiency reasons, CLP(FD) systems typically maintain only so-called bounds consistency for arithmetic constraints, and in general do not remove interior elements from domains even when some of them cannot participate in solutions.

Bounds consistency, in the finite case, means that there are solutions where the variable assumes the lower and upper boundary of the domain. In this case, there are solutions for A=1 and A=5.

Notice that these are the only solutions in this concrete case, but in general, there are also solutions with interior points in analogous larger instances, for example:

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

The good news though is that the number of such solutions only grows logarithmically in the size of the domain:

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

This is in contrast to other cases, like X mod 2 #= 0, where the number of solutions grows linearly in the size of the domain of X (and thus exponentially in the length of its decimal representation), and it is thus not feasible to explicitly prune the domain.

Thus, as a feasible workaround, you can use label/1 to obtain concrete solutions, and then use in/2 constraints to restrict the operands to their concretely admissible domains:

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

Your example:

?- [A,B] ins 1..5, A*B#=5, stricter_domains([A,B]).
A in 1\/5,
A*B#=5,
B in 1\/5.

Menis

Why no mentioning of contracting/1? – Balk

Agree, but what about ruling out values one-by-one? Similar to contracting. – Balk

@false. We need a proper interface. Let clpfd export contracting/1, or maybe better contracting/2 :) The domain reductions are interesting for multiple reasons: First, they are an additional tool in the toolbox. clpfd-users may already have a similar idea like this (but struggle to realize a decent implementation). Second, it helps characterize problems: how many sudoku, nonogram, and other puzzles (that people solve for fun) are completely solvable by contracting/2 alone--- without ever using `labeling/2! Oh, and third, a perfect fit for multicores (no state needs to be shared!) – Ellerey

Why don't you write an answer? – Balk

Please also check out the literature: I think our "contracting" is called "shaving" in the CLP(FD) literature. – Menis