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

[Mark Brown]

On 05-Jun-2006, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Mark Brown, Monday,  5 June 2006:
> > On 05-Jun-2006, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> > > 
> > > I have large problem cases: any programs using SAT solvers and most
> > > programs using LP :-)
> > 
> > That's like saying "I have a straight flush" but not showing anyone.
> > 
> > Would these be cases where projection is basically free (as it is for
> > ordinary Mercury variables)?
> 
> SAT solver example: add_clause([A, B, C])
> 
> Grounding any subset of A, B, C will not tell you anything about the
> implied groundness of the rest or whether the clause is even satisfied.
> So one has to ensure that all variables are eventually grounded to
> guarantee solver completeness.
> 
> Your groundness analysis will tell me I need to promise that everything
> is properly grounded at some point, but I knew that anyway!

In other words, the analysis gets it exactly right!

Note that the above goal will be transformed by the compiler into something
like:

	some [V0, V1, V2, V3] (
		V0 = [],
		V1 = [C | V0],
		V2 = [B | V1],
		V3 = [A | V2],
		add_clause(V3)
	)

The analysis will tell you that you don't have to label the introduced
variables, only A, B and C.

> 
> The crux of the debate, as I see it, is which of the two following
> options is best:
> 
> (A) supply groundness inference details where possible and perform
> groundness analysis in the compiler, requiring an explicit promise where
> the analysis cannot prove solver completeness;
> 
> (B) don't bother doing groundness analysis, always require an explicit
> promise.

If you're talking about an explicit promise for each existentially
quantified variable, then that's a lot of promises.  Particularly when
then compiler introduces lots of variables.

If you're talking about an explicit promise at the top level of your
constraint solving code, then this will provide no help whatsoever in
either verifying completeness or, if the program is incomplete, in
localising the problem.

> 
> My intuition is that the promise is going to be required in many cases
> with the FD solver and in most, if not all, cases with other solvers.

It will help with compiler introduced variables for all solvers, which
will be very common.

Cheers,
Mark.

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