[m-dev.] Solvers, negation, existential quantification, and so forth

[Ralph Becket]

Peter Stuckey, Friday,  2 June 2006:
> 
> On 02/06/2006, at 2:18 PM, Ralph Becket wrote:
> >Where does the propagation engine fit into all this?
> >
> >Say I have a SAT variable B and an FD variable X and a
> >propagator implementing B => X < 3.
> >
> >Now I assert B in the SAT solver and I assert X = 4 in the FD solver,
> >but I do neither of these operations within the propagation framework.
> >
> >In this case the propagator will not be fired, but surely my program
> >is still in an incomplete state (and will be so even if I call the
> >make-everything-complete predicates for the SAT and FD solvers).
> 
> Adding X = 4 in must wake the propagator for X < 3 <=> B otherwise there
> is something totally wrong. Simialarly adding B = true.

In the current arrangement it's only when constraints are posted in the
context of the propagation engine that propagation will occur.

I agree that this allows Bad Things to happen, but it looks to me like
an issue with solver completeness that couldn't be detected by PS'
proposal (at least, as I understand it).

> >I think that in practice possible incompleteness will be the norm and
> >that detecting definite completeness will be very rare.  Although I'd
> >love to be convinced otherwise!
> 
> Bascially you are almost always incomplete. only very special routines
> lead to completeness (labelling). Tracking this for the user is  
> difficult
> since its only labelling on all variables which guaranteed completeness

So are you also saying you think this analysis probably won't help in
most cases?
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------