[Gecode] Interaction between shared variables and idempotency

[Christian Schulte]

Dear all,

initially, the tests for sharing and equality on views was meant to address
issues with shared variables for idempotent propagators.

As a reminder, a propagator returns ES_FIX if it is at a fixpoint and
ES_NOFIX if it is not at a fixpoint. For efficiency, the propagator should
try hard to tell ES_FIX most of the times when it is actually at fixpoint.
However, this is difficult for propagators computing on shared views:
performing an operation on a view also narrows the domain of the shared
view.

Here are three strategies for finding out whether a propagator is at
fixpoint with shared views.

1. Suppose a propagator that only performs at most one write operation to a
view. Typical examples are "smart" propagators such as distinct, regular,
etc. They work by first computing new domain information for each view and
then writing or posting this information back to the views. Here one can use
a trick to find out whether one has computed a fixpoint or not: a view x
provides an operation x.modified(). When a propagator starts execution
modified() is false for all views. Only after a modification has taken
place, it becomes true. So the following works: before the propagator posts
to the view x, it checks whether x is already modified. If yes, the
propagator might not be at a fixpoint. Otherwise, it is.

2. The propagator computes in a loop until a fixpoint is reached. The
propagator must make sure that this loop really computes a fixpoint! For
example, when the loop is based until no view changes this also must
consider that no shared view has been changed. Here the trick with modified
is not available.

3. Check for sharing once and for all. If none of the above works, just
check whether the propagator has shared views or not. If it has, ALWAYS
report ES_NOFIX! This can be achieved most efficiently by making the
propagator generic with respect to whether to return ES_FIX and ES_NOFIX
through a template.

Here comes also an example why this matters. Assume domain consistent
distinct and variables x with domain {1,2} and y both with domain {2,3} and
the following three views v1 := x+0, v2 := x+1, v3 := y. Propagation should
yield x=1 and y=3 directly! However, if the propagator does not detect that
v1 and v2 are shared it will only propagate that x=1 and y in {2,3}!

And yes, sharing sucks. And yes, almost all propagators are faulty (but
linear and bool!)...

Christian

--
Christian Schulte, http://www.imit.kth.se/~schulte/