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

[Peter Stuckey]

On 01/06/2006, at 5:10 PM, Peter Schachte wrote:

> On Thu, Jun 01, 2006 at 03:38:31PM +1000, Mark Brown wrote:
>> On 01-Jun-2006, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
>>> RECOMMENDATION: we (somehow, perhaps by annotation on mode  
>>> declarations)
>>> identify constraint posting predicates that may succeed, but  
>>> leave the
>>> solver state inconsistent.
>>
>> If we were to adopt such a scheme, then I'd suggest putting the  
>> explicit
>> annotation on the goals where success means consistent.
>
> Since you need to indicate which solver(s) they are incomplete
> relative to, you'll need to list the incomplete ones anyway.
>
>> However, I don't think that attaching this information to modes is
>> fine-grained enough.  Consider the goal `X = Y + Z' for FD  
>> variables X, Y
>> and Z.  A program will be solver complete for this goal if at  
>> least two of
>> the variables are ground at the time of the call (assuming a  
>> reasonable
>> implementation of '+'), but may not be if only one of them is ground.
>
> Hang on, I think that's exactly backward.  The constraint X = Y + Z
> with 2 or fewer ground variables is always satisfiable, so it's
> trivially complete.

Buuuuuhhhh thanks for playing.

	x + y = 10  (complete according to the above)
	x + z = 10  (complete according to the above)
         y != z          (ceratinly satisfiably given the current  
domains of y and z!)

The FD solve will certainly succeed at the moment

complete does not equal always satisfiable, since we are talking about
future unsatisfiability.  Rearrange the constraint in any order if  
the above
example is not convincing enough

> With 3 ground variables, it's pretty trivial to
> make it complete:  just calculate and do an equality check.  The
> incomplete case is if you've already got some funky constraints on all
> 3 variables that doesn't ground them, and you don't want to bother to
> check whether the relation holds.  If you don't mind checking, you're
> complete.  We want to define a goal as complete as long as it can't
> *introduce* failure without failing; it need not confirm the whole
> constraint store is satisfiable.  If the constraint store is already
> unsatisfiable, a goal for which the solver is solver complete can do
> anything it likes.  Ie, if S is the current constraint store and
> c(X,...) is a constraint, then we say the solver is solver complete
> for c iff
>
> 	forall S, X... : S /\ succeeds(c(X...)) => c(X...)

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