[gecode-users] Watching Propagators

[Mikael Zayenz Lagerkvist]

First of all, just as was the case two years ago, nobody knows how to do
explanations for general propagators. The most interesting system for doing
explanations in a CP-like system at the moment is the lazy clause generation
research being done in the G12 project, where propagation is represented as
a SAT problem. This requires a completely different system and propagator
implementation though.

Remember, propagators in a CP system contain advanced algorithms that come
from many different fields of computer science (graph algorithms, numerics,
scheduling algorithms, ...), operating on variables that may have billions
of values. This is in contrast with SAT solving, where there is just a
single propagation rule over the simplest possible variable that needs to be
explained, and the propagation rule is in itself very simple.

What one could do without re-implementing all propagators is to simply
record all variables state before and after a propagator runs, and use that
as an explanation. Such a recording would in most cases be huge (making
anything but the simplest possible problem infeasible), and also would most
likely not be very useful. It simply doesn't say anything useful: it is very
common for many propagators to cover a large portion of the variables, and
many times not all the variables are relevant to the results. Also, it would
not suffice to just look at the most recently modified variables when a
propagator is run, the propagation performed might depend on all the
variables.

As a practical note, adding the kind of bookkeeping that you describe would
add quite a lot of overhead in many cases. As a comparison, simple
propagators for constraints such as <, !=, and so on take on the order of
ten to twenty machine instructions to execute in Gecode last time I
checked.

What is not clear to me is how you would like to use a hypothetical reason
that you would like to extract. Maybe there is something simpler that could
be used?

Cheers,
Mikael

On Mon, Jun 20, 2011 at 10:05 AM, Max Ostrowski <ChaosAngel at gmx.de> wrote:

> Sorry for reposting, i already asked this question 2 years ago, but now i
> managed to read more of the manual and my questions will be more refined.
>
> For each constraint that i post, i want to find out which variables are
> propagated by the corresponding propagator.
> Also the ordering would be interesting. I need this to build an SMT like
> System, to generate a "reason" why a certain reified constraint became
> true/false.
>
> So can i somehow "watch" the propagate function, testing if the subscribed
> variables are pruned?
>
> I first thought of "copying" the post functions of Gecode and implementing
> a "wrapper" propagator that wraps around the functions.
> But i think this will not do the work, as propagators can be disposed and
> replaced at runtime, right ?
>
>
> Do you have any other idea how i can find out which constraint is
> responsible for pruning the search space?
> I want to avoid to modify Gecode, as i want to stay up to date.
> This is also the reason why i do not simply want to copy all propagators to
> implement BookKeeping myself.
>
> Best,
> Max
> --
> Empfehlen Sie GMX DSL Ihren Freunden und Bekannten und wir
> belohnen Sie mit bis zu 50,- Euro! https://freundschaftswerbung.gmx.de
>
> _______________________________________________
> Gecode users mailing list
> users at gecode.org
> https://www.gecode.org/mailman/listinfo/gecode-users
>



-- 
Mikael Zayenz Lagerkvist, http://www.ict.kth.se/~zayenz/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gecode.org/pipermail/users/attachments/20110620/2dc954c1/attachment.htm>