[gecode-users] reified linear sum of booleans

[Christian Schulte]

Hi Tias,

to comment on the reified linear Boolean: I believed that they were not that
useful. Clearly, you proved me wrong here. A watched literal based
implementation will be included in 3.0.

On a more general note: if we don't know whether something is useful we
leave it until demand for it arises.

Cheers
Christian

--
Christian Schulte, www.ict.kth.se/~cschulte/


-----Original Message-----
From: users-bounces at gecode.org [mailto:users-bounces at gecode.org] On Behalf
Of Guido Tack
Sent: Tuesday, July 29, 2008 8:59 AM
To: Tias Guns
Cc: users at gecode.org
Subject: Re: [gecode-users] reified linear sum of booleans

Hi Tias,

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.

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

Cheers,
        Guido


_______________________________________________
Gecode users mailing list
users at gecode.org
https://www.gecode.org/mailman/listinfo/gecode-users