[gecode-users] Watching Propagators

[Max Ostrowski]

At first, thanks for the answer.

> 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.
This shouldn't be a problem as it is an SMT system and therefore i will do lazy-clause generation. So i just need the reason for the whole (reified) constraint, not the single csp variables.


> 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.
The size in terms of memory isn't that big problem, but the size of the reason (as you have to add all constraints to the reason that have a pruned variable in it).
This is why i wanted to add the ordering, which means that a reified constraint that becomes true/false only depends on the changed constraints that propagated before.

 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.
That's right.

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

I'm building a SMT like system (with ASP instead of SAT, but just consider it to be a SAT system).
So i have proposition variables for the reified constraints. Each constraint is either true or false.
This is why i would like to add a reason, why a constraint became false.
With this reason i can add a new Boolean constraint to my SAT solver which then saves propagation in gecode, as it can already decide whether a certain constraint is true/false.
I think there was once a work implementing learning in Gecode, i will contact the author to find out what he did. (But i suppose that he extended Gecode or did wrote own propagators, which i want to avoid).

Best,
Max


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

-- 
NEU: FreePhone - kostenlos mobil telefonieren!			
Jetzt informieren: http://www.gmx.net/de/go/freephone