[Oz] Filtering of values of constraint variables

[Denys Duchier]

I don't think I have answered your message earlier, in which case I
apologize for the belated response.

benko at iqsoft.hu (Benko Tamas) writes:

> Filtering is used in (or before) the labeling phase and it means that
> before committing to a possible value we try to exclude values by
> tentatively instantiating it to a value and watching if it fails.

In Mozart, filtering is constraint propagation.  This is a process of
deterministic inference which removes values from the domains of
variables.  This process is sound but incomplete which is why we also
need steps of distribution (aka. labeling).

> In Prolog it looks like this:
> 
> % Try to filter out value V from variable X.
> filter(X, V) :-
>         (   \+ X = V -> X #\= V
>         ;   true
>         ).

It seems to me that, for finite domain and finite set variables, what
you outline above is pointless since X=V fails precisely when V is no
longer a value in the domain of X.

In general, the Prolog approach is unsound because it uses negation as
failure which is unsound:  failure to prove G is not the same as
proving ~G (the negation of G).  The problem with Prolog's approach is
magnified in a concurrent system where what you need in order to prove
G may be in the process of being concurrently computed by other
threads.  Mozart offers a sound alternative:

        cond G1 then G2 else G3 end

blocks until G1 is entailed or becomes inconsistent, at which point it
proceeds accordingly with G2 or G3.  A related construct is:

        or G1 then H1
        [] G2 then H2
        ...
        [] Gn then Hn
        end

which blocks until only one clause remains that hasn't been defeated
yet.  Whenever Gi becomes inconsistent, clause `Gi then Hi' is
defeated and dropped.  When only one clause `Gk then Hk' remains, the
`or' construct unblocks and commits to it; i.e. it is now as if is
were executing `Gk Hk' in sequence.  The `then' part is optional, and
personally I always use it in the form:

        or G1 [] G2 [] ... [] Gn end

where, as far as possible, I try to write the (Gi) so that they are
mutually exclusive.  For example, when reasoning about non-empty sets
of nodes in a tree, I often need to state (1) either A is a subset of
B (2) or B is a subset of A (3) or they are disjoint.  I can express
this new constraint as follows:

        thread
           or {FS.subset A B}
           [] {FS.subset B A}
           [] {FS.disjoint A B}
           end
        end

As soon of 2 of these clauses are discovered to be inconsistent, the
`or' commits to the remaining one which then improves global
constraint propagation.  Notice that I wrapped the `or' in a `thread'
because, as stated earlier, `or' blocks until it can commit, and
typically I want to post such a constraint as a concurrent agent that
doesn't block my current thread (which is oftent the main thread,
where I will perform distribution - i.e. labeling).

> This kind of filtering is useful if the constraint system is unable infer
> that X can't have the value V, but it can detect the inconsistency if X is
> instantiated to V.

By using the constructs described above, you can soundly detect the
inconcistency of arbitrary constraints (in particular conjunctions of
simpler constraints - which cannot be achieved by reified
constraints).  For example, if it cannot be guaranteed that A and B
are non-empty, I might write the earlier constraint as follows:

        thread
           or {FS.card A}>:0 {FS.subset A B}
           [] {FS.card B}>:0 {FS.subset B A}
           [] {FS.disjoint A B}
           end
        end

If you cannot guarantee mutual exclusion, then you hould introduce a
control variable:

        X::1#3
        thread
          or X=1 G1
          [] X=2 G2
          [] X=3 G3
        end

So that at the end of labeling you can make sure that your disjunction
has been decided by labeling on X:

        {FD.distribute ff [... X ...]}

I wrote [... X ...] because your program might introduce many control
variables.  However, when you cannot guarantee mutual exclusion, you
can usually make weaker inferences, e.g. whenever Gi is inconsistent,
then it must be the case that Hi.  Then it is better to write your
constraint as:

        X::1#3
        thread or X=1 G1 [] X\=:1 H1 end end
        thread or X=2 G2 [] X\=:2 H2 end end
        thread or X=3 G3 [] X\=:3 H3 end end
        ...
        {FD.distribute ff [... X ...]}

This is in fact the best pattern because it guarantees a maximum of
propagation as early a possible (as soon as Gi is proven inconsistent,
you obtain additional propagation from Hi).  This is the pattern which
I use most often.  Note that it works both ways: if Hi is proven
inconsistent, then your program commits to Gi.

> In Mozart the constraint posting and the search phases are nicely
> separated, and I don't know to which phase filtering belongs.

As explained, filtering is constraint propagation.  However, using
Mozart's abstractions for encapsulation (e.g. the Space and Search
modules) you can use search within search.  This is a rather advanced
technique, and I believe that Christian Schulte, who, unlike me, has
actually tried it :-), would be in a better position to elaborate if
elaboration is desired.

> Another (completely unrelated) question: is it possible to program
> constraint propagators in Mozart without using the C++ interface?  For
> prototyping purposes it would be fast enough for me.

I outlined above the main technique for programming new constraints in
Mozart: use the `or' construct.  Once your prototype has achieved the
sort of propagation that your application requires, you can improve
performance by providing a C++ implementation as a drop-in
replacement.  There is nothing magic about the `or' construct: it is
in fact fully implemented in Oz using computation spaces.  If you need
a constraint whose semantics doesn't fit the mold of the `or'
construct, you can use the more powerful Space abstraction to build it
from scratch.  I believe this only happened once to me.

On the other hand, I use the C++ interface a lot.  In spite of some
quirks, the CPI is extremely well done and easy to use.  It is, of
course, daunting the first time, but then you notice that for every
constraint, you need similar code.  Just keep a skeleton
implementation handy, copy and fill in the blanks... hmmm... maybe we
should supply such a squeleton, although "The Mozart Constraint
Extensions Tutorial" contains examples.  Tobias and I are also working
on a compiler to automatically generate an implementation from a
logical specification, but this is for now only work in progress (we
have only made it so far as to be able to generate implementations for
the standard non-n-ary finite set constraints of Mozart).

Hope this helps.

Cheers,

-- 
Dr. Denys Duchier			Denys.Duchier at ps.uni-sb.de
Forschungsbereich Programmiersysteme	(Programming Systems Lab)
Universitaet des Saarlandes, Geb. 45	http://www.ps.uni-sb.de/~duchier
Postfach 15 11 50			Phone: +49 681 302 5618
66041 Saarbruecken, Germany		Fax:   +49 681 302 5615

-
Please send submissions to users at mozart-oz.org
and administriva mail to users-request at mozart-oz.org.
The Mozart Oz web site is at http://www.mozart-oz.org/.