25. Reification and rewriting

This chapter discusses how to implement propagators for reified constraints and how to optimize constraint propagation by propagator rewriting. Gecode does not offer any special support for reification but uses propagator rewriting as a more general technique.

Overview. Reified constraints and how they can be propagated is reviewed in Reification. The following section (A fully reified less or equal propagator) presents a reified less or equal propagator as an example. How to implement both half and full reification is discussed in the following section. General propagator rewriting during constraint propagation is discussed in Rewriting during propagation, whereas Rewriting during cloning presents how to rewrite propagators during cloning.

25.1. Reification

Before reading this section, please read about reification in Reified constraints and about half reification in Half reification.

A propagator for the reified constraint \(\mathtt{b}=\mathtt{1}\Leftrightarrow c\) for a Boolean control variable \(\mathtt{b}\) propagates as follows:

  1. If b is 1, propagate \(c\) (reification modes: RM_EQV \(\Leftrightarrow\), RM_IMP \(\Rightarrow\)).

  2. If b is 0, propagate \(\neg c\) (reification modes: RM_EQV \(\Leftrightarrow\), RM_PMI \(\Leftarrow\)). Not that it is not always easy to propagate the negation of a constraint \(c\) effectively and efficiently.

  3. If \(c\) is subsumed, propagate that b is 1 (reification modes: RM_EQV \(\Leftrightarrow\), RM_PMI \(\Leftarrow\)).

  4. If \(\neg c\) is subsumed, propagate that b is 0 (reification modes: RM_EQV \(\Leftrightarrow\), RM_IMP \(\Rightarrow\)).

The idea how to implement reification in Gecode is quite simple: if the first (or second) case is true, the reified propagator implementing the reified constraint rewrites itself into a propagator for \(c\) (or \(\neg c\)). The remaining two cases are nothing but testing criteria for subsumption.

The advantage of rewriting a reified propagator for \(\mathtt{b}=\mathtt{1}\Leftrightarrow c\) into a non-reified propagator for \(c\) or \(\neg c\) is that the propagators created by rewriting are typically available anyway, and that after rewriting no more overhead for reification is incurred.

25.2. A fully reified less or equal propagator

We will discuss a fully reified less or equal propagator \(\mathtt b=\mathtt{1}\Leftrightarrow \mathtt x \leq \mathtt y\) for integer variables x and y using full reification (that is, reification mode RM_EQV \(\Leftrightarrow\)) as an example. Taking the above propagation rules for a reified constraint, we obtain:

  1. If b is 1, propagate \(\mathtt x \leq \mathtt y\).

  2. If b is 0, propagate \(\mathtt x > \mathtt y\) (actually, we choose to propagate \(\mathtt y < \mathtt x\) instead).

  3. If \(\mathtt x \leq \mathtt y\) is subsumed, propagate that b is 1.

  4. If \(\mathtt x > \mathtt y\) is subsumed, propagate that b is 0.

  5. If none of the above rules apply, the propagator is at fixpoint.

Program 25.1 A constraint and propagator for fully reified less or equal
...
class Less 
  ...
};
class LeEq
  ...
};

class ReLeEq
  : public Int::ReBinaryPropagator<Int::IntView,Int::PC_INT_BND,
                                   Int::BoolView> {
...
  virtual ExecStatus propagate(Space& home, const ModEventDelta&)  {
    if (b.one())
      GECODE_REWRITE(*this,LeEq::post(home(*this),x0,x1));
    if (b.zero())
      GECODE_REWRITE(*this,Less::post(home(*this),x1,x0));
    switch (Int::rtest_lq(x0,x1)) {
    case Int::RT_TRUE:
      GECODE_ME_CHECK(b.one(home)); break;
    case Int::RT_FALSE:
      GECODE_ME_CHECK(b.zero(home)); break;
    case Int::RT_MAYBE:
       return ES_FIX;
    }
    return home.ES_SUBSUMED(*this);
  }
};

...

Download: less-or-equal-reified-full.cpp

The propagator ReLeEq for reified less or equal relies on propagators Less for less and LeEq for less or equal (the propagators are not shown, see Using propagator patterns instead). The propagate() function as shown in Program 25.1 follows the propagation rules sketched above.

Propagator rewriting. The GECODE_REWRITE macro takes the propagator (here, *this) to be rewritten and an expression that posts the new propagator as arguments. It relies on the fact that the identifier home refers to the current home space (like the fail macros in Improving the Less propagator). The macro expands to something along the following lines:

size_t s = this->dispose(home);
GECODE_ES_CHECK(LeEq::post(home(*this),x0,x1));
return home.ES_SUBSUMED_DISPOSED(*this,s);

That is, the ReLeEq propagator is disposed, the new LeEq propagator is posted, and subsumption is reported. The order is essential for performance: by first disposing ReLeEq, the data structures that store the subscriptions for x0 and x1 will have at least one free slot for the subscriptions that are created by posting LeEq and hence avoid (rather inefficient and memory consuming) resizing. Note that it is important to understand that the old propagator is disposed before the new propagator is posted. In case that some data structures that are deleted during disposal are needed for posting, one either has to make sure that the data structures outlive the call to dispose() or that one does not use the GECODE_REWRITE macro but first posts the new propagator and only then reports subsumption.

Another essential part is that after calling ES_SUBSUMED(), a propagator is not allowed to do anything that can schedule propagators (such as performing modification operations or creating subscriptions). That is the reason that first dispose() is called and later the special variant ES_SUBSUMED_DISPOSED() is used for actually reporting subsumption. Do not use ES_SUBSUMED_DISPOSED() unless you really, really have to!

Adding information to Home. As has been discussed in Space& versus Home and Improving the Less propagator, posting uses a value of class Home instead of a reference to a Space. In the expansion of GECODE_REWRITE as shown above, the call operator () as in

home(*this)

returns a new value of type Home with the additional information added that the propagator to be posted is in fact a rewrite of the propagator *this. This information is important, for example, for inheriting the AFC (accumulated failure count, see Selection using accumulated failure count): the newly created propagator will inherit the number of accumulated failures from the propagator being rewritten. There will be other applications of Home in future versions of Gecode.

Testing relations between views. Rather than testing whether \(\mathtt{x0}\leq\mathtt{x1}\) or \(\mathtt{x0}>\mathtt{x1}\) hold individually, we use the function Int::rtest_lq() that tests whether two views are less or equal and returns whether the relation holds (Int::RT_TRUE), does not hold (Int::RT_FALSE), or might hold or not (Int::RT_MAYBE).

Relation tests are available for two views (integer or Boolean) or for a view (again, integer or Boolean) and an integer. Relation tests exist for all inequality relations: Int::rtest_le() (for \(<\)), Int::rtest_lq() (for \(\leq\)), Int::rtest_gr() (for \(>\)), and Int::rtest_gq() (for \(\geq\)). For equality, a bounds test (Int::rtest_eq_bnd()) as well as a domain test exists (Int::rtest_eq_dom()).

While Int::rtest_eq_bnd() only uses the bounds for testing the relation (with constant time complexity), Int::rtest_eq_dom() uses the full set of values in the domain of the views to determine the relation (having linear time complexity in the length of the range representation of the views’ domains, see Iterator-based modification operations for more information on range representations of view domains). The same holds true for disequality: Int::rtest_nq_bnd() performs the bounds-only test, whereas Int::rtest_nq_dom() performs the full domain test. For example, Int::rtest_eq_bnd(x,y) for \(\mathtt x\in\{0,2\}\) and \(\mathtt y\in\{1,3\}\) returns Int::RT_MAYBE, whereas Int::rtest_eq_dom() returns Int::RT_FALSE.

Reified propagator patterns. The integer module (as these patterns require Boolean views they are part of the integer module) provides reified propagator patterns for unary propagators (Int::ReUnaryPropagator) and binary propagators (Int::ReBinaryPropagator and Int::ReMixBinaryPropagator). In addition to views x0 (and x1 for the binary variants), they define a Boolean control variable b. Please note that in Program 25.1 a reified propagator pattern requires an additional template argument for the Boolean control view used (the mystery why this is useful is lifted in Views).

25.3. Supporting both full and half reification

There are two different options for implementing all different reification modes: either implement a single propagator that stores its reification mode, or implement three different propagators, one for each reification mode. Due to performance reasons we choose the latter variant here. That is, one needs one propagator for each reification mode: RM_EQV for equivalence (\(\Leftrightarrow\)), RM_IMP for implication (\(\Rightarrow\)), and RM_PMI for reverse implication (\(\Leftarrow\)). Instead of three different implementations it is better to have a single implementation that is parametric with respect to the reification mode.

Program 25.2 A constraint and propagator for full and half reified less or equal
...
template<ReifyMode rm>
class ReLeEq
  : public Int::ReBinaryPropagator<Int::IntView,Int::PC_INT_BND,
                                   Int::BoolView> {
...
  // [less or equal reified half:propagate function]
};

void leeq(Home home, IntVar x0, IntVar x1, Reify r) {
  GECODE_POST;
  switch (r.mode()) {
  case RM_EQV:
    GECODE_ES_FAIL(ReLeEq<RM_EQV>::post(home,x0,x1,r.var()));
    break;
  case RM_IMP:
    GECODE_ES_FAIL(ReLeEq<RM_IMP>::post(home,x0,x1,r.var()));
    break;
  case RM_PMI:
    GECODE_ES_FAIL(ReLeEq<RM_PMI>::post(home,x0,x1,r.var()));
    break;
  default:
    throw Int::UnknownReifyMode("leeq");
  }
}

Download: less-or-equal-reified-half.cpp

Program 25.2 shows the constraint post function leeq() for the reified less or equal propagator supporting all three reification modes. The class ReLeEq now is parametric with respect to the reification mode the propagator implements. The constraint post function now posts the propagator that corresponds to the reification mode (available via r.mode()) passed as argument r of type Reify. The Boolean control variable can be returned by r.var().

Program 25.3 Propagate function for full and half reified less or equal
  virtual ExecStatus propagate(Space& home, const ModEventDelta&)  {
    if (b.one()) {
      if (rm != RM_PMI)
        GECODE_REWRITE(*this,LeEq::post(home(*this),x0,x1));
    } else if (b.zero()) {
      if (rm != RM_IMP)
        GECODE_REWRITE(*this,Less::post(home(*this),x1,x0));
    } else {
      switch (Int::rtest_lq(x0,x1)) {
      case Int::RT_TRUE:
        if (rm != RM_IMP)
          GECODE_ME_CHECK(b.one(home)); 
        break;
      case Int::RT_FALSE:
        if (rm != RM_PMI)
          GECODE_ME_CHECK(b.zero(home)); 
        break;
      case Int::RT_MAYBE:
        return ES_FIX;
      }
    }
    return home.ES_SUBSUMED(*this);
  }

The idea for the reified propagator is straightforward, its propagate() function is shown in Program 25.3: the four different parts of the propagator are employed depending on the reification mode rm. Note that this is entirely schematic and any reified propagator can be programmed supporting all reification modes in that way.

25.4. Rewriting during propagation

Rewriting during propagation is a useful technique that is not limited to implementing reification. We consider a Max propagator that propagates \(\max(\mathtt{x}_0,\mathtt{x}_1)=\mathtt{x}_2\). The propagation rules (we are giving bounds propagation rules that achieve () consistency, see [11]) for Max are easy to understand when looking at an equivalent formulation of \(\max\) [50]:

\[\begin{aligned} \max(\mathtt{x}_0,\mathtt{x}_1)=\mathtt{x}_2 &\iff& (\mathtt{x}_0\leq\mathtt{x}_2)\wedge (\mathtt{x}_1\leq\mathtt{x}_2)\wedge \left( (\mathtt{x}_0=\mathtt{x}_2)\vee(\mathtt{x}_1=\mathtt{x}_2)\right)\\ &\iff& (\mathtt{x}_0\leq\mathtt{x}_2)\wedge (\mathtt{x}_1\leq\mathtt{x}_2)\wedge \left( (\mathtt{x}_0\geq\mathtt{x}_2)\vee(\mathtt{x}_1\geq\mathtt{x}_2)\right)\\ \end{aligned}\]

Then, the propagation rules can be turned into the following C++-code to be executed by the propagate() member function of Max:

GECODE_ME_CHECK(x2.lq(home,std::max(x0.max(),x1.max())));
GECODE_ME_CHECK(x2.gq(home,std::max(x0.min(),x1.min())));
GECODE_ME_CHECK(x0.lq(home,x2.max()));
GECODE_ME_CHECK(x1.lq(home,x2.max()));
if ((x1.max() <= x0.min()) || 
    (x1.max() < x2.min()))
  GECODE_ME_CHECK(x0.gq(home,x2.min()));
if ((x0.max() <= x1.min()) || 
    (x0.max() < x2.min()))
  GECODE_ME_CHECK(x1.gq(home,x2.min()));
Program 25.4 A maximum propagator using rewriting
...
class Equal : public BinaryPropagator<Int::IntView,Int::PC_INT_BND> {
...
};
class Max : public TernaryPropagator<Int::IntView,Int::PC_INT_BND> {
public:
  ...
  virtual ExecStatus propagate(Space& home, const ModEventDelta&) {
    GECODE_ME_CHECK(x2.lq(home,std::max(x0.max(),x1.max())));
    GECODE_ME_CHECK(x2.gq(home,std::max(x0.min(),x1.min())));
    GECODE_ME_CHECK(x0.lq(home,x2.max()));
    GECODE_ME_CHECK(x1.lq(home,x2.max()));
    if ((x1.max() <= x0.min()) || (x1.max() < x2.min()))
      GECODE_REWRITE(*this,Equal::post(home(*this),x0,x2));
    if ((x0.max() <= x1.min()) || (x0.max() < x2.min()))
      GECODE_REWRITE(*this,Equal::post(home(*this),x1,x2));
    if (x0.assigned() && x1.assigned() && x2.assigned())
      return home.ES_SUBSUMED(*this);
    else 
      return ES_NOFIX;
  }
};

...

Download: max-using-rewriting.cpp

Please take a second look: the condition of the first if-statement tests whether \(\mathtt{x}_1\) is less or equal than \(\mathtt{x}_0\), or whether \(\mathtt{x}_1\) is less than \(\mathtt{x}_2\). In both cases, \(\max(\mathtt{x}_0,\mathtt{x}_1)=\mathtt{x}_2\) simplifies to \(\mathtt{x}_0=\mathtt{x}_2\). Exactly this simplification can be implemented by propagator rewriting, please check Program 25.4. Note that the propagator is naive in that it does not implement the propagator to be idempotent (however, this can be done exactly as demonstrated in Fixpoint reasoning reconsidered).

Another idea would be to perform rewriting during cloning: the copy() function could return an Equal propagator rather than a Max propagator in the cases where rewriting is possible. However, this is illegal: it would create a propagator with only two views, hence one view would not be updated even though there is a subscription for it (violating obligation “update complete” from Propagator obligations). Also, canceling a subscription is illegal during cloning (violating obligation “cloning conservative” from Propagator obligations). The next section shows an example with opposite properties: rewriting during propagation makes no sense (even though it would be legal) whereas rewriting during cloning is legal and useful.

25.5. Rewriting during cloning

In Dynamic subscriptions, the propagator OrTrue is simplified during copying by eliminating assigned views. Here we show that the propagator created as a copy during cloning can be optimized further by rewriting it during copying.

Copying.

The modified copy() function is as follows:

  virtual Propagator* copy(Space& home) {
    for (int i=x.size(); i--; )
      if (x[i].one()) {
        x[0]=x[i]; x.size(1);
        return new (home) SubsumedOrTrue(home,*this);
      } else if (x[i].zero()) {
        x.move_lst(i);
      }
    if (x.size() == 0)
      return new (home) BinaryOrTrue(home,*this);
    else
      return new (home) OrTrue(home,*this);
  }
Program 25.5 A Boolean disjunction propagator using rewriting
...
class BinaryOrTrue : 
  ...
  BinaryOrTrue(Space& home,
               BinaryPropagator<Int::BoolView,Int::PC_BOOL_VAL>& p)
    ...
  virtual ExecStatus propagate(Space& home, const ModEventDelta&) {
    if (x0.zero())
      GECODE_ME_CHECK(x1.one(home));
    if (x1.zero())
      GECODE_ME_CHECK(x0.one(home));
    return home.ES_SUBSUMED(*this);
  }
};
class SubsumedOrTrue : 
  ...
  SubsumedOrTrue(Space& home, 
                 BinaryPropagator<Int::BoolView,Int::PC_BOOL_VAL>& p)
    ...
  virtual ExecStatus propagate(Space& home, const ModEventDelta&) {
    return home.ES_SUBSUMED(*this);
  }
};
class OrTrue : 
  ...
  // [or true using rewriting:copy]
  ...
};

...

Download: or-true-using-rewriting.cpp

The copy() function takes advantage of two cases:

  1. If there is a view that is assigned to 1, the propagator is subsumed. However, during cloning a propagator cannot be deleted by subsumption. Reporting subsumption is only possible during propagation. The copy() function does the next best thing: it creates a propagator SubsumedOrTrue that next time it is executed will in fact report subsumption.

    Note that in this situation rewriting during cloning is preferable to rewriting during propagation. An important aspect of the OrTrue propagator is that it does not inspect all of its views during finding a view for resubscribing (as implemented by the resubscribe() member function). Instead, inspection stops as soon as the first unassigned view is found. That entails that a view that is assigned to 1 might be missed during propagation. In other words, rewriting during cloning also optimizes subsumption detection.

  2. If all views in the view array x are assigned to 0, the view array is actually not longer needed (it has no elements). In this case, the copy() function creates a propagator BinaryOrTrue that is a special variant of OrTrue limited to just two views. Note that the two views x0 and x1 are known to be not yet assigned: otherwise, the propagator would not be at fixpoint. This is impossible as only spaces that are at fixpoint (and hence all of its propagators must be at fixpoint) can be cloned (this invariant is discussed in Space-based search).

    Rewriting during propagation would be entirely pointless in this situation: the propagator (be it OrTrue or BinaryOrTrue) will be executed at most one more time and will become subsumed then (or, due to failure, it is not executed at all). As rewriting incurs the cost of creating and disposing propagators and subscriptions, rewriting in this case would actually slow down execution.

Constructors for copying. The relevant parts of the two special propagators for rewriting SubsumedOrTrue and BinaryOrTrue are shown in Program 25.5. Their propagate() functions are exactly as sketched above. The only other non-obvious aspect are the constructors used for copying during cloning: they are now called for a propagator of class OrTrue. In this example, it is sufficient to have a single constructor for copying as all the propagators OrTrue, SubsumedOrTrue, and BinaryOrTrue inherit from BinaryPropagator. In other cases, it might be necessary to have more than a single constructor for copying defined by a propagator class C: one for copying a propagator of class C and one for creating propagators as rewrites of other propagators.