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

[Ralph Becket]

Peter Schachte, Friday,  2 June 2006:
> On Thu, Jun 01, 2006 at 07:09:56PM +1000, Mark Brown wrote:
> > On 01-Jun-2006, Peter Schachte <schachte at csse.unimelb.edu.au> wrote:
> > > Since you need to indicate which solver(s) they are incomplete
> > > relative to, you'll need to list the incomplete ones anyway.
> > 
> > I don't understand this point.
> > 
> > Elsewhere in the thread, you explained:
> > > This property needs to be parametric in the solver id involved.  This
> > > is because a primitive may render a *particular* solver complete, but
> > > it can't possibly promise to render *all* solvers complete.
> > 
> > I'm not entirely sure what you mean by a solver id.
> 
> It doesn't mean anything by itself, it's just a way of insulating the
> incompleteness caused by some predicates from the incompleteness
> caused by others.  Typically, it'll just be a solver type name.  Eg,
> suppose fd.alldifferent/1 is incomplete and fd.label_everything/0 is
> "completing" (ie, it makes the computation complete), and that
> interval.whatever/N is incomplete, and you call fd.alldifferent/1
> followed by interval.whatever/N, then fd.label_everything/0 can't make
> the computation complete, it can only complete the fd part of it.
> You'll need to also call some completing predicate for the interval
> solver to make the computation complete.

The interval "solver" can never guarantee consistency: it reports where a
solution cannot be found, but not whether any solution exists.

On the other hand, local search solvers can never prove inconsistency,
but only report particular solutions (and they cannot guarantee to find
a solution even if one exists).

Interval solvers and local search can therefore never be solver
complete.

> So the completeness state at
> a program point must be the set of solvers for which the computation
> is incomplete.

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).

> Distinguishing this case from your example would require some kind of
> possible aliasing analysis, and could never be precise.  So ultimately
> we'll have to either sometimes force a variable to be ground even
> though it will have more constraints added later, or sometimes allow a
> variable to become inaccessible without ensuring that it has a
> satisfying value.  For performance reason, I think we have to choose
> the latter.

Agreed.

> Unfortunately, this means that solvers will always have to track all
> their variables.  But it does not mean that we can't, with a possible
> aliasing analysis, sometimes let a solver know when one of its
> variables is becoming dead.

You can let them know on backtracking.  Have you got any examples where
that wouldn't be sufficient?

> So I suspect with a rather simple test we could catch many cases where
> we could promise a solver that certain variables were dead.  Solvers
> could use this information to detect contradictions earlier than they
> otherwise might, as well as to possibly reclaim some internal data
> structures.  Of course, they would also have to be careful of
> backtracking forcing the recreation of that variable.

Can you explain this with an example or two?  (Sorry, I'm having trouble
picturing what you mean.)

> This is a lot more work than simply tracking possible incompleteness.
> I think we should do both, but I think possible incompleteness
> tracking will be necessary and easier, so we should do it first.

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!

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