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

[Mark Brown]

On 06-Jun-2006, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> 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).

Right.  This is the kind of example I was looking for.

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

Ok, I accept that the right way to solve this problem is for the solver
to remember Z in some global data structure and label it later when a
consistency checking procedure is called.  But there is still no need
for the solver to remember _all_ variables, only Z in this case.

Note that the groundness analysis and a global labelling procedure can
happily coexist.  The SAT solver can provide the following predicate

	delayed_labelling(Xs)

where the groundness information is (true -> Xs), meaning that everything
in Xs becomes ground.  The implementation of delayed_labelling need only
record the variables in some global data structure, which will be labelled
later when the consistency check is called.  The goal would now become:

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

for which it is straightforward to show that the quantification is safe,
assuming that the consistency check is later called.  (Possibly both the
delayed_labelling predicate and the consistency_check procedure could take
a solver id as an extra argument, so that different parts of the problem
could be searched separately.)

Even given this case, I still think that groundness analysis would be
worthwhile.  When combined with an explicit `delayed_labelling' predicate:

	- It explicitly informs readers of the code that there is a
	  variable in this goal that will need to be labelled, which will
	  help them reason about the search that their application must
	  later do.

	- It would catch when the programmer hasn't realised that there is
	  an extra variable to be labelled, in cases like the above.

	- It minimises the number of variables that need to be saved for
	  later labelling.

	- It means that (for some solvers) no explicit consistency_check,
	  and likewise no facility for saving variables in a global, will
	  be required.

Also, in general the order in which variables is labelled will be very
important.  A simple mechanism of saving all variables and labelling them
all at once generally won't give the user enough control over search --
they will typically want to very carefully choose which variables to label
and in what order.  Groundness analysis will help them do this correctly.

Finally, here's an example that shows why using solver ids to distinguish
between different problems will be necessary.  Consider the following
predicate which solves some constraint problem:

	p(...) :-
		... post constraints on Xs ...,
		solve_some_unconnected_problem(...),
		... post more constraints on Xs ...,
		impure check_consistency.

The predicate solve_some_unconnected_problem shares no solver variables
with p and has no `any' insts in its mode.  If its implementation was:

	solve_some_unconnected_problem(...) :-
		... post constraints on Ys ...,
		impure check_consistency.

then the consistency check here would label all variables from this solver,
including those in Xs.  But we wouldn't want to label Xs here, as there
are still constraints yet to be posted.  Hence the consistency_check
approach will require Xs and Ys to be associated with distinct solver ids.
These would add a lot of complexity to the way you would need to reason
about completeness (and would also add complexity to the code itself).
And I don't see any way that the compiler can help with this complexity.

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