[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:
> > > Mark Brown, Monday,  5 June 2006:
> > > > In other words, the analysis gets it exactly right!
> > > 
> > > I know that: but in this case the analysis is completely useless! :-)
> > 
> > An analysis that helps to verify the safety of existential quantification
> > is hardly going to be useful for an example that has no existential
> > quantifiers in it.  ;-)
> 
> Oh God!  :-)

I'm suddenly struck by the image of Basil Fawlty saying to Manuel:
"Please!  Try to understand before one of us dies."

> 
> An analysis that can't help even when I have got an existential
> quantification in there ain't much use to me either!

Que?  The analysis I described _can_ help.

Reviewing what has been said in the thread so far, it seems (correct me
if I'm wrong) you are proposing that we can ensure all variables get
labelled by:

	1)  Having each solver keep a reference to every variable it has
	ever created (possibly indexed by some kind of "solver id").

	2)  Having each solver provide an impure labelling procedure
	that doesn't take a list of variables, but instead labels _all_
	variables the solver has kept track of (or all variables
	associated with a particular solver id).

	3)  Requiring the user to promise that they have called this
	procedure, or labelled all the variables in some other way.

Is this a fair summary?

My proposal takes a different approach.  It doesn't require all solvers
to keep track of every variable they have created.  It doesn't require
any notion of a solver id.  It doesn't require the user to promise at the
top of solver code that they have called a generic labelling procedure.
However, there are cases when they will instead need to promise that a
variable does not need to be labelled in order for the program to be
complete.

I've already given one example (the min/max example) where, using my scheme,
a promise would be required.  Here's two more examples (again, for a finite
domain solver).

Consider this goal:

	some [Y] (
		X < Y,
		Y < Z
	)

Groundness analysis won't tell you that Y becomes ground here (indeed, in
general Y wouldn't become ground).  However, it is easy to show that if
there is no value that Y can take (that is, if X >= Z - 1), then the
domain of Y will become empty and failure will occur.  We know this
because the we know that the implementation of '<' is bounds consistent.

To make this compile, it will be necessary to promise that the existential
quantification is sound:

	promise_some [Y] (
		X < Y,
		Y < Z
	).

The promise here can be read literally: the user is promising that there
exists a value for Y that is consistent with the constraint store.  In this
case, the fact that a promise is required is a Good Thing, since the
reasoning required to prove completeness is non-trivial, and centers around
this exact point in the code.

Let me reiterate the point:

	- the problem with this example is that the existential
	quantification cannot be shown to be safe,

	- this is exactly the place where a promise is required, and

	- the promise itself has a direct literal meaning.

Consider now the following example (which comes from an already existing
test case we have for the finite domain solver).

        impure Is = n_new_fdvars(3, 1, 3),
        impure Xs = n_new_fdvars(3, 1, 3),
        impure Vs = n_new_fdvars(3, 1, 3),
        Is = [I1, I2, I3],
        Vs = [V1, V2, V3],
        element_var(I1, Xs, V1),
        element_var(I2, Xs, V2),
        element_var(I3, Xs, V3),
        all_different(Xs),
        all_different(Vs),
	Ls = append(Is, Vs)
        impure labeling(Ls)

The groundness information for the various calls is:

	As = n_new_fdvars(_, _, _)		true
	element_var(I, Xs, V)			(Xs /\ I -> V), (Xs /\ V -> I)
	all_different(As)			true
	labeling(Ls)				true -> Ls
	Ls = append(Is, Vs)			Ls <-> Is /\ Vs

(Here "true" means no information: none of the arguments are definitely
ground.)

Groundness analysis will determine that Is and Vs become ground, but can't
show that Xs does.  Xs does in fact become ground, but showing this requires
non-trivial reasoning (and, in particular, requires knowledge of the
semantics of element_var and all_different). Again, an explicit
`promise_some [Xs]' will be required, and again it is a Good Thing, IMHO.

In both cases, the promises required are very precise: they promise exactly
the fact that is necessary but non-trivial to show, and they don't promise
anything else.

Do you have any examples from SAT or LP which, like the three examples I
have given already, show that the groundness analysis is not precise
enough?  That is, can you back up with examples your intuition that a
promise will be required in "most, if not all, cases with other [non-FD]
solvers"?

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