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

[Ralph Becket]

Mark Brown, Tuesday,  6 June 2006:
> On 05-Jun-2006, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> >
> 
> 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?

Absolutely.

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

I follow what you are (and have been) saying.  It's very attractive.
But...

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

Agreed.  Now consider the following situation:

	some [Z] (
		add_clause([..., Z]),
		add_clause([..., Z]),
		add_clause([..., Z])
	)

For very good efficiency reasons I do not want to label Z at the end of
its scope.  Labelling the ... variables will not cause Z to be labelled
either (i.e., there's no groundness propagation here).  I can't use
promise_some [Z] here because there may be *no* solution for Z (i.e.,
adding these constraints may, in some circumstances, make the
constraint store unsatisfiable).

As far as I can see, the SAT solver will have to remember that Z was
introduced and check that it has a consistent labelling when the user
finally calls the impure sat_label_everything consistency checking
predicate.

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