listprologclpfdlexicographicb-prolog

Lexicographically order two lists of variables using constraints

I'm trying to implement a lexicographic ordering constraint in BProlog using its CLP(FD).

As far as I can see from the manual BProlog doesn't provide a built-in lexLeq constraints (though there exist efficient propagation algorithms for this global constraint), so I'm trying to write my own and express the ordering as the following set of binary constraints:

X1 #=< Y1, (X1 #= Y1) #=> (X2 #=< Y2), (X1 #= Y1 #/\ X2 #= Y2) #=> (X3 #=< Y3), ..., (X1 #= Y1 #/\ ... #/\ XN #= YN) #=> (XN+1 #=< #YN+1)

To express the (A1 #/\ A2 #/\ ... #/\ AN) => AN+1 constraint I think I should be able to reify the Ais, so:

domain(B, 0, 1),
(X1 #= Y1) #<=> B

I then collect the Bs and to check that the conjunction is valid I simply do:

(sum(Bs) #= N) #=> AN+1

The idea leads to the following (probably very ugly) code:

lexLeq(Xs, Ys) :-
    lexLeq(Xs, [], Ys, []).

lexLeq([X|Xs], [], [Y|Ys], []) :-
    X #=< Y,
    lexLeq(Xs, [X], Ys, [Y]).
lexLeq([X|Xs], [OldX|OldXs], [Y|Ys], [OldY|OldYs]) :-
    makeAndConstr([OldX|OldXs], [OldY|OldYs], X, Y),
    lexLeq(Xs, [X,OldX|OldXs], Ys, [Y, OldY|OldYs]).
lexLeq([], _, [], _).


makeAndConstr(Xs, Ys, X, Y) :-
    length(Xs, N),
    makeAndConstr(Xs, Ys, [], N, X, Y).

makeAndConstr([X|Xs], [Y|Ys], Bs, N, X, Y) :-
    domain(B, 0, 1),
    (X #= Y) #<=> B,
    makeAndConstr(Xs, Ys, [B|Bs], N, X, Y).
makeAndConstr([], [], Bs, N, X, Y) :-
    (sum(Bs) #= N) #=> (X #=< Y).

This partially works:

| ?- domain([A,B,C,D,E,F], 0, 1), lexLeq([A,B,C], [D, E, F]), labeling([A,B,C,$
A = 0
B = 0
C = 0
D = 0
E = 0
F = 0 ?;
A = 0
B = 0
C = 0
D = 1
E = 1
F = 1 ?;
A = 1
B = 1
C = 1
D = 1
E = 1
F = 1 ?;
no

as you can see all solutions produced do satisfy the constraint. The problem is that not all valid solutions are produced. It seems like the constraints I've describe also somehow imply that X1 #>= X2 #>= ... #>= XN or something like that, so that all variables are either 0 or 1, while the above query should return also solutions like [0,1,0] vs [0,1,0] or [0,0,0] vs [0,1,0].

So, is there something wrong with my reasoning or is there a bug in the above definitions?

Solution

  • In the first clause of makeAndConstr/6, you use X for two different purposes, which causes the extra failures (same for Y). This renamed code works:

    makeAndConstr([X1|Xs], [Y1|Ys], Bs, N, X, Y) :-
    domain(B, 0, 1),
    (X1 #= Y1) #<=> B,
    makeAndConstr(Xs, Ys, [B|Bs], N, X, Y).

    You could have found this by tracing a simple goal that you expected to succeed, e.g. lexLeq([0,1],[0,1]).

    Simpler formulation of the lexicographic ordering constraint

    I want to share with you an elegant solution that I was taught many years ago by my former colleague Warwick Harvey. It goes like this:

    lex_le(Xs, Ys) :-
    lex_le(Xs, Ys, 1).

lex_le([], [], 1).
lex_le([X|Xs], [Y|Ys], IsLe) :-
    IsLe #<=> (X #< Y+RestIsLe),
    lex_le(Xs, Ys, RestIsLe).

    which is explained by observing that IsLe is 1 if