Can CLPFD distribute things evenly into groups?

Question

This is a simplified example; say I want to distribute weights over tables such that the tables end up roughly equally loaded, e.g. (10 10 10 5 5) Kg can balance equally as (10 10) (10 5 5).

(10 9 8 7) can't balance so I prefer (10 7) (9 8) or (10 9) (8 7) to (10 9 8) (7). i.e. closer to a balanced weight distribution is the goal. NB. balancing total load on each table, not quantity of weights on each table (I think that rules out global_cardinality).

I have tried to sum the total input weights and constrain "each table must have #=< Total//2". Inputs won't balance exactly so if one has to have slightly more than half, that fails. Adding some wiggle room "#=< (Total//2) + Tolerance" and if the Tolerance is too small then no answers, if it's too large instead of balancing as equally as it can, it stops as soon as one is just under the cutoff - as unbalanced as it can get away with. Trying to label with Tolerance in 1..1000 and min(Tolerance) feels like it should work to get closest to balance, but I haven't got it to - mostly getting non-termination in minutes of waiting.

Here's my code for one trial, e.g. for answers weight(10)-2 is a 10Kg weight paired with table 2:

% weight(Kg)
weight(10).
weight(10).
weight(10).
weight(10).

% balance weight-table pairs, Table 1 total KG, Table 2 total Kg
balance([], 0, 0).

balance([weight(Kg)-1 | Ws], Table1Total, Table2Total) :-
    Table1Total #= T1_ + Kg,
    balance(Ws, T1_, Table2Total).

balance([weight(Kg)-2 | Ws], Table1Total, Table2Total) :-
    Table2Total #= T2_ + Kg,
    balance(Ws, Table1Total, T2_).


go(Pairs) :-
    findall(weight(Kg), weight(Kg), Weights),
    pairs_keys_values(Pairs, Weights, Tables),
    Tables ins 1..2,
    balance(Pairs, T1, T2),
    TableDiff #= abs(T2-T1),  % seek to minimise the difference, doesn't seem to do that?
    labeling([min(TableDiff)], [TableDiff|Tables]).

I expect to see it assign two weights to each table since these weights do have an even balance:

% expected / desired:
?- go(P).
P = [weight(10)-1, weight(10)-1, weight(10)-2, weight(10)-2]

% actual:
?- go(P).
P = [weight(10)-1, weight(10)-1, weight(10)-1, weight(10)-1]   % all on table 1

That actual result put all weights (40Kg) on Table1 and none on Table2. It doesn't seem to be seeking min(TableDiff) at all. https://www.swi-prolog.org/pldoc/man?predicate=labeling/2 says:

The order of solutions can be influenced with:

min(Expr)
max(Expr)

This generates solutions in ascending/descending order with respect to the evaluation of the arithmetic expression Expr.

I have tried with putting the equation in the min(abs(T2-T1)) as well with no change. How can I get good balanced solutions, use clpfd to seek a max or min? (related: the balance/3 predicate is ugly, is there a nicer way to use clpfd with aggregate or group_by groupings?)

Answer 1

Not a nice solution but it can be done this way:

:- use_module(library(clpz)).
:- use_module(library(lists)).
:- use_module(library(reif)).


tables(Ws, Ts) :-
    Ws ins 0..sup,
    same_length(Ts, Ts0),
    foldl(initialize, Ts0, 0, _),
    % Permute Ws to find better/all solution.
    foldl(distribute, Ws, Ts0, Ts1),
    maplist(arg(2), Ts1, Ts). % Extract.

initialize(s(N0,[],0), N0, N) :-
    N #= N0+1.

distribute(W, Ts0, Ts) :-
    minimum(Ts0, M),
    update(M, W, Ts0, Ts).

min(s(_,_,N), S0, S) :-
    S #= min(N,S0).

minimum([E0|Es], N) :-
    s(_,_,N0) = E0,
    foldl(min, Es, N0, N).

update(_, _, [], []).
update(M, W, [T0|Ts0], [T|Ts]) :-
    s(N,Ws0,S0) = T0,
    if_(
        S0 = M,
        (   Ws = [W|Ws0],
            S #= S0+W,
            T = s(N,Ws,S),
            Ts = Ts0
        ),
        (   T = T0,
            update(M, W, Ts0, Ts)
        )
    ).

It assumes the weights are non-negative and some solutions are missing without the permutation (it's greedy).

Example:

?- Ts = [_,_,_], tables([10,10,10,5,5], Ts).
   Ts = [[5,10],[5,10],[10]].

Answer 2

When working with CLPFD, it is generally advisable to decompose the program: Separate it into a core relation that sets up the CLPFD description of the problem, and a separate relation that does the labeling. This allows you to test the core relation in isolation. It makes no sense to try to label a bad description of a problem.

On a subtle note, note that I said "description of the problem". You are only solving one problem, right? Then it should have only one description. That is, the core relation should only have one answer. The one problem might have several solutions, but it is up to the labeling to enumerate those.

Let's take a look at the decomposition of your program:

% core relation
pairs_tablediff_tables_(Pairs, TableDiff, Tables) :-
    findall(weight(Kg), weight(Kg), Weights),
    pairs_keys_values(Pairs, Weights, Tables),
    Tables ins 1..2,
    balance(Pairs, T1, T2),
    TableDiff #= abs(T2-T1).

% full relation: core relation + labeling
go(Pairs) :-
    pairs_tablediff_tables_(Pairs, TableDiff, Tables),
    labeling([min(TableDiff)], [TableDiff|Tables]).

Let's test the core relation:

?- pairs_tablediff_tables_(Pairs, TableDiff, Tables).
Pairs = [weight(10)-1, weight(10)-1, weight(10)-1, weight(10)-1],
TableDiff = 40,
Tables = [1, 1, 1, 1] ;
Pairs = [weight(10)-1, weight(10)-1, weight(10)-1, weight(10)-2],
TableDiff = 20,
Tables = [1, 1, 1, 2] ;
Pairs = [weight(10)-1, weight(10)-1, weight(10)-2, weight(10)-1],
TableDiff = 20,
Tables = [1, 1, 2, 1] ;
Pairs = [weight(10)-1, weight(10)-1, weight(10)-2, weight(10)-2],
TableDiff = 0,
Tables = [1, 1, 2, 2] ;
Pairs = [weight(10)-1, weight(10)-2, weight(10)-1, weight(10)-1],
TableDiff = 20,
Tables = [1, 2, 1, 1] ;
Pairs = [weight(10)-1, weight(10)-2, weight(10)-1, weight(10)-2],
TableDiff = 0,
Tables = [1, 2, 1, 2] .  % etc.

As you can see, this has many answers. It shouldn't, since this is not describing a problem, but purported solutions to the problem. Also, there are no variables here. Labeling cannot do anything if it has no variables to work with.

The problem with your definition lies in your balance/3 predicate:

balance([], 0, 0).

balance([weight(Kg)-1 | Ws], Table1Total, Table2Total) :-
    Table1Total #= T1_ + Kg,
    balance(Ws, T1_, Table2Total).

balance([weight(Kg)-2 | Ws], Table1Total, Table2Total) :-
    Table2Total #= T2_ + Kg,
    balance(Ws, Table1Total, T2_).

This says, roughly, "the weight is in one of two bins, and the corresponding bin's total weight must account for it". This is good, but it involves a disjunction (the weight is in bin 1 or in bin 2), and that disjunction is not part of the CLPFD problem description but of the Prolog progam that tries to build that description. If this program has Prolog disjunctions, it will have Prolog backtracking, and this means that it will not build one CLPFD problem description but several distinct ones, that it will enumerate on backtracking.

So you need to bring the disjunction into CLPFD. There are several ways of doing this, all of them ugly. (Others are very welcome to prove me wrong on this!) Here is one way, expressed using reification (see https://www.swi-prolog.org/pldoc/man?section=clpfd-reification-predicates):

:- use_module(library(clpfd)).

% weight(Kg)
weight(10).
weight(10).
weight(10).
weight(10).

% balance weight-table pairs, Table 1 total KG, Table 2 total Kg
balance([], 0, 0).
balance([weight(Kg)-Assignment | Ws], Table1Total, Table2Total) :-
    Assignment in 1..2,
    Assignment #= 1  #==>  Table1Total #= T1_ + Kg,
    Assignment #= 1  #==>  Table2Total #= T2_,
    Assignment #= 2  #==>  Table2Total #= T2_ + Kg,
    Assignment #= 2  #==>  Table1Total #= T1_,
    balance(Ws, T1_, T2_).

totalweight(TotalWeight) :-
    findall(Kg, weight(Kg), Weights),
    sumlist(Weights, TotalWeight).

% core relation
pairs_tablediff_tables_(Pairs, TableDiff, Tables) :-
    findall(weight(Kg), weight(Kg), Weights),
    pairs_keys_values(Pairs, Weights, Tables),
    Tables ins 1..2,
    totalweight(TotalWeight),
    [T1, T2] ins 0..TotalWeight,
    balance(Pairs, T1, T2),
    TableDiff #= abs(T2-T1).

% full relation: core relation + labeling
go(Pairs) :-
    pairs_tablediff_tables_(Pairs, TableDiff, Tables),
    labeling([min(TableDiff)], [TableDiff|Tables]).

This uses the #==> implication operator to say things like "if the current element is in bin 1, its weight is added to bin 1's total weight, and bin 2's total weight remains the same".

We also need to compute the total weight of all items and use it to constrain the domains of T1 and T2, otherwise labeling complains that these are infinite.

Now, let's test this core relation:

?- pairs_tablediff_tables_(Pairs, TableDiff, Tables).
Pairs = [weight(10)-_5414, weight(10)-_5430, weight(10)-_5446, weight(10)-_5462],
Tables = [_5414, _5430, _5446, _5462],
_5414 in 1..2,
_5414#=2#<==>_5510,
_5414#=2#<==>_5522,
_5414#=1#<==>_5534,
_5414#=1#<==>_5546,
_5510 in 0..1,
_5510#==>_5570,
_5570 in 0..1,
% ...omitting a lot more constraints...
_5534 in 0..1,
_5682 in 0..1,
_5522#==>_5682,
_5522 in 0..1.

We can't really tell if these constraints are correct just by looking at them, but at least now we have one problem description, and it contains variables that can be labeled, which is what we want.

Let's look at the full relation, including labeling:

?- go(Pairs).
Pairs = [weight(10)-1, weight(10)-1, weight(10)-2, weight(10)-2] ;
Pairs = [weight(10)-1, weight(10)-2, weight(10)-1, weight(10)-2] ;
Pairs = [weight(10)-1, weight(10)-2, weight(10)-2, weight(10)-1] ;
Pairs = [weight(10)-2, weight(10)-1, weight(10)-1, weight(10)-2] ;
Pairs = [weight(10)-2, weight(10)-1, weight(10)-2, weight(10)-1] ;
Pairs = [weight(10)-2, weight(10)-2, weight(10)-1, weight(10)-1] ;
Pairs = [weight(10)-1, weight(10)-1, weight(10)-1, weight(10)-2] ;
Pairs = [weight(10)-1, weight(10)-1, weight(10)-2, weight(10)-1] ;
Pairs = [weight(10)-1, weight(10)-2, weight(10)-1, weight(10)-1] ;
Pairs = [weight(10)-1, weight(10)-2, weight(10)-2, weight(10)-2] ;
Pairs = [weight(10)-2, weight(10)-1, weight(10)-1, weight(10)-1] ;
Pairs = [weight(10)-2, weight(10)-1, weight(10)-2, weight(10)-2] ;
Pairs = [weight(10)-2, weight(10)-2, weight(10)-1, weight(10)-2] ;
Pairs = [weight(10)-2, weight(10)-2, weight(10)-2, weight(10)-1] ;
Pairs = [weight(10)-1, weight(10)-1, weight(10)-1, weight(10)-1] ;
Pairs = [weight(10)-2, weight(10)-2, weight(10)-2, weight(10)-2] ;
false.

Labeling enumerates all the solutions. Crucially, it enumerates the best (most balanced) ones first, which is good. Now you can go ahead and try to refine the labeling strategy, or strengthen the core relation to exclude the most extremely unbalanced solutions.