[gecode-users] Space entailment

[Mikael Zayenz Lagerkvist]

On 3/1/07, Gustavo Gutierrez <ggutierrez at cic.puj.edu.co> wrote:
> Hi all,
>
> I was wondering about the representation of the entailment relation in
> gecode. Suppose you have a space with variables and constraints. How
> can i verify if an extra constraint is already entailed by the store
> (space)?. In the mozart terminology this is the difference between a
> succeeded(entailed) and a succeeded(stuck) space. Of course, here we
> will not take threads into account since threads does not exist in
> gecode.
>
> At implementation level, if the relation implemented by a propagator
> to be posted in the space is already represented in terms of variables
> domains, the propagator is not posted at all. Then counting how many
> propagators are in the space before the posting of the new one and
> comparing it to the number of propagators after posting it, is enough
> to verify that property.
>
> Do you agree??


The short answer is no, this will not tell you if the posted
constraint was entailed.


In general, entailment for a constraint is a co-NP complete problem,
which means that it is a property that can only be approximated for
many common constraints.

For some constraints, posting will check for entailment (e.g., Boolean
or) and for some it will not (e.g., distinct). Furthermore, some
constraints there are good entailment checks (e.g. linear
in-equations) while others don't have any good ones (most global
constraints). As a simple example, try posting a distinct-constraint
on a collection of variables with non-overlapping ranges. The
constraint is trivially entailed, but the propagator is still not
subsumed.

A more specific reason why your technique won't work (not even as an
approximation), is that a newly created propagator will (in most
cases) be scheduled for propagation. To get a correct calculation of
the number of propagators, you would need to compute the fixpoint.
When you call status() for the space, the propagator will be run,
possibly resulting in some domain-reductions and more propagators
being run. One (or more) of the other propagators could in turn be
subsumed, leading to the count returned from propagators() to look
like the constraint was entailed.


If I recall correctly, Mozart/Oz is more strict than Gecode when it
comes to detecting entailment of propagators. But I am no expert in
the Mozart system. The common theme in Gecode is to try to delay
invocation of propagators until they can propagate.

A good example of possible approaches is the not-equals constraint
between two variables. If you only want to run the propagator when it
can propagate, it should only be run when one of the variables is
assigned. If we want to get early subsumption, it should listen to all
events to see if the domains are non-overlapping.


Hope this helps,
Mikael

-- 
Mikael Zayenz Lagerkvist, http://www.ict.kth.se/~zayenz/