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

Peter Stuckey pjs at cs.mu.OZ.AU
Fri Jun 2 14:31:05 AEST 2006


On 02/06/2006, at 2:18 PM, Ralph Becket wrote:

> Peter Schachte, Friday,  2 June 2006:
>> On Thu, Jun 01, 2006 at 07:09:56PM +1000, Mark Brown wrote:
>>> On 01-Jun-2006, Peter Schachte <schachte at csse.unimelb.edu.au> wrote:
>>>> Since you need to indicate which solver(s) they are incomplete
>>>> relative to, you'll need to list the incomplete ones anyway.
>>>
>>> I don't understand this point.
>>>
>>> Elsewhere in the thread, you explained:
>>>> This property needs to be parametric in the solver id involved.   
>>>> This
>>>> is because a primitive may render a *particular* solver  
>>>> complete, but
>>>> it can't possibly promise to render *all* solvers complete.
>>>
>>> I'm not entirely sure what you mean by a solver id.
>>
>> It doesn't mean anything by itself, it's just a way of insulating the
>> incompleteness caused by some predicates from the incompleteness
>> caused by others.  Typically, it'll just be a solver type name.  Eg,
>> suppose fd.alldifferent/1 is incomplete and fd.label_everything/0 is
>> "completing" (ie, it makes the computation complete), and that
>> interval.whatever/N is incomplete, and you call fd.alldifferent/1
>> followed by interval.whatever/N, then fd.label_everything/0 can't  
>> make
>> the computation complete, it can only complete the fd part of it.
>> You'll need to also call some completing predicate for the interval
>> solver to make the computation complete.
>
> The interval "solver" can never guarantee consistency: it reports  
> where a
> solution cannot be found, but not whether any solution exists.

It can if there are no equations!


> On the other hand, local search solvers can never prove inconsistency,
> but only report particular solutions (and they cannot guarantee to  
> find
> a solution even if one exists).
>
> Interval solvers and local search can therefore never be solver
> complete.

Almost true, a local search solver when it says something is a solution
is always correct.  It can just never fail!

>> So the completeness state at
>> a program point must be the set of solvers for which the computation
>> is incomplete.
>
> Where does the propagation engine fit into all this?
>
> Say I have a SAT variable B and an FD variable X and a
> propagator implementing B => X < 3.
>
> Now I assert B in the SAT solver and I assert X = 4 in the FD solver,
> but I do neither of these operations within the propagation framework.
>
> In this case the propagator will not be fired, but surely my program
> is still in an incomplete state (and will be so even if I call the
> make-everything-complete predicates for the SAT and FD solvers).

Adding X = 4 in must wake the propagator for X < 3 <=> B otherwise there
is something totally wrong. Simialarly adding B = true.

>
>> This is a lot more work than simply tracking possible incompleteness.
>> I think we should do both, but I think possible incompleteness
>> tracking will be necessary and easier, so we should do it first.
>
> I think that in practice possible incompleteness will be the norm and
> that detecting definite completeness will be very rare.  Although I'd
> love to be convinced otherwise!

Bascially you are almost always incomplete. only very special routines
lead to completeness (labelling). Tracking this for the user is  
difficult
since its only labelling on all variables which guaranteed completeness


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

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



More information about the developers mailing list