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

[Ralph Becket]

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!

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.

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.

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