[gecode-users] reified linear sum of booleans

[Tias Guns]

On Tue, 29 Jul 2008 08:59:26 +0200, Guido Tack <tack at ps.uni-sb.de> wrote:

> Hi Tias,

Thank you for your answers,

> Tias Guns wrote:
>
>> Greetings,
>>
>> I'm using a model in which I rely heavily on reified linear sums of
>> booleans. Unfortunately the existing boolean reified linear sum
>> implementatiom is horribly slow for this ! To overcome this, I'm  
>> currently
>> channeling all boolean variables to integers, and posting the reified
>> linear sum over the integers. This gives incredibly faster runtimes.
>
> The reified Boolean sums are currently not implemented by special  
> propagators but using a decomposition that is not very efficient.
>
>> The first batch of constraints are regular reified linear sums, they are
>> constructed by reading a binary matrix and creating an IntArgs 'row'  
>> which
>> contains 0 or 1 (out or in). This 'row' is multiplied by an array of
>> decision variables, each representing one column. Doing so selects the
>> desired subset of those variables after which they are constrained and
>> reified to the variable representing that row:
>> for (int r = 0; r!=nr_r;r++ ) {
>>   // make row
>>   for (int c = 0; c!=nr_c;c++ ) {
>>     row[c] = (1-tdb[r][c]); // complement
>>   }
>>   // sum(row*col_vars) = 0 <=> row_vars[r]
>>   linear(this, row, col_vars, IRT_EQ, 0, row_varsBool[r]);
>> }
>>
>> here, the col_vars is an IntVarArgs that is channeled to corresponding
>> BoolVars.
>
> You may want to use Boolean disjunction here, although you'll have to  
> use another temporary Boolean variable.  Something like this:
>
> for (int r = 0; r != nr_r; r++) {
>    BoolVarArgs col(noOfZeroesIn_tdb_Row[r]);
>    for (int i = 0, int c = 0; c != nr_c; c++) {
>      if (tdb[r][c])
>      	col[i++] = col_varsBool[c];
>    }
>    BoolVar tmp(this, 0, 1);
>    rel(this, BOT_OR, col, tmp);
>    rel(this, tmp, IRT_NQ, row_varsBool[r]);
> }
>
> I'm not sure whether this is going to be more efficient, but the  
> specialized Boolean propagators should be better.

Unfortunately it's not more efficient. The number of propagations  
increases, probably because of the extra constraints. The runtime behaves  
worse and worse as the problem instances become larger and harder. I've  
looked into posting an NaryOr constraint with a BoolViewArray and a  
NegBoolView directly, but the current templating of NaryOr doesn't allow  
it. I'm hoping/thinking that a reified linear sum of booleans would be  
able to achieve equal propagation..

>> The second batch of constraints are imply-reified linear sums, having  
>> one
>> sided reification. Because one-sided reification is not implemented in
>> gecode directly, an extra auxiliary variable and constraint is used to
>> manage it:
>> for (int c = 0; c!=nr_c;c++ ) {
>>   // make col
>>   for (int r = 0; r!=nr_r;r++ ) {
>>     col[r] = tdb[r][c];
>>   }
>>   // sum(col*row_vars) >= X <=> col_aux[c]
>>   linear(this, col, row_vars, IRT_GQ, X, col_aux[c]);
>>   // col_aux[c] => col_varsBool[c] (one-sided reificiation,  
>> reformulation
>> is) col_aux[c] =< col_varsBool[c]
>>   rel(this, col_aux[c], IRT_LQ, col_varsBool[c]);
>> }
>> similarly as above, row_vars is an IntVarArgs channeled to corresponding
>> BoolVars.
>
> As suggested above, you could post the first linear constraint using  
> just the row_vars for which col[r] is 1, but in this case it probably  
> isn't more efficient (since the linear will immediately throw away all  
> the variables with 0 coefficients anyway).
>
>> This model works very well but still, I'm wondering if there would be a
>> better or cleaner way to model this, and if there are any plans to  
>> improve
>> the reified linear sum of boolean constraints.
>
> Yes, the reified linear Boolean sum is going to be reimplemented, but  
> not for the (upcoming) 2.2.0 release.

Excellent, thanks in advance.


Greetings,
Tias

> Cheers,
> 	Guido