Propia is an implementation of Generalised Propagation which is described in the paper [14].
In principle Propia propagates information from an annotated goal by finding all solutions to the goal and extracting any information that is common to all the different solutions. (In practice, as we shall see later, Propia does not typically need to find all the solutions.)
The “common” information that can be extracted depends upon what constraint solvers are used when evaluating the underlying un-annotated ECLiPSe goal. To illustrate this, consider another simple example.
p(1,3). p(1,4). ?- p(X,Y) infers most.
If the ic library is not loaded when this query is
invoked, then the information propagated by Propia is that X=1.
If, on the other hand, ic is loaded, then more common
information is propagated. Not only does Propia propagate X=1 but
also the domain of Y is tightened from -inf..inf to
3..4. (In this case the additional common information is that
Y ≠ 0, Y ≠ 1, Y ≠ 2 and so on for all values except 3
and 4!)
Any goal Goal in an ECLiPSe program, can be transformed into a
constraint by annotating it thus: Goal infers Parameter.
Different behaviours can be specified with different parameters, viz:
Goal infers mostGoal infers uniqueGoal infers consistent
These behaviours are nicely illustrated by the crossword demonstration
program crossword in the examples code directory.
There are 72 ways to complete the crossword grid with words from the
accompanying directory.
For finding all 72 solutions,
the comparative performance of the different annotations is given in the
table Comparing Annotations.
Annotation CPU time (secs) consistent 13.3 unique 2.5 most 9.8 ac 0.3
Table 15.1: Comparing Annotations
The example program also illustrates the effect of specifying the waking
conditions for Propia. By only waking a Propia constraint when it
becomes instantiated, the time to solve the crossword problem can be
changed considerably. For example by changing the annotation from
Goal infers most to
suspend(Goal,4,Goal->inst) infers most
the time needed to find all solutions goes down from 10 seconds to
just one second.
For other problems, such as the square tiling problem in the example
directory, the fastest version is the
one using infers consistent. To find the best Propia
annotation it is necessary to experiment with the current problem
using realistic data sets.
Propia extracts information from a procedure which may be defined by multiple ECLiPSe clauses. The information to be extracted is controlled by the Propia annotation.
Figure 15.3: Transforming Procedures to Constraints
In this section we describe how Propia works.
When a goal is annotated as a Propia constraint, eg.
p(X,Y) infers most, first the goal p(X,Y) is in effect
evaluated in the normal way by ECLiPSe.
However Propia does not stop at the first solution, but continues to
find more and more solutions, each time combining the information from
the solutions retrieved.
When all the information has been accumulated, Propia propagates this
information (either by narrowing the domains of variables in the goal,
or partially instantiating them).
Propia then suspends the goal again, until the variables become further constrained, at which point it wakes, extracts information from solutions to the more constrained goal, propagates it, and suspends again.
If Propia detects that the goal is entailed (i.e. the goal would succeed whichever way the variables were instantiated), then after propagation it does not suspend any more.
Propia works by treating its input both as a goal to be called,
and as a term which can be manipulated as data.
As with any ECLiPSe goal, when executed its result is a further
instantiation of the term.
For example the first result of calling member(X,[a,b,c]) is
to further instantiate the term yielding member(a,[a,b,c]).
This instantiated term represents the (first) solution to the goal.
Propia combines information from the solutions to a goal using their most specific generalisation (MSG). The MSG of two terms is a term that can be instantiated (in different ways) to either of the two terms. For example p(a,f(Y)) is the MSG of p(a,f(b)) and p(a,f(c)). This is the meaning of generalisation. The meaning of most specific is that any other term that generalises the two terms, is more general than the MSG. For example, any other term that generalises p(a,f(b) and p(a,f(c)) can be instantiated to p(a,f(Y)). The MSG of two terms captures only information that is common to both terms (because it generalises the two terms), and it captures all the information possible in the two terms (because it is the most specific generalisation).
Some surprising information is caught by the MSG. For example the MSG of p(0,0) and p(1,1) is p(X,X). We can illustrate this being exploited by Propia in the following example:
|
The test succeeds, recognising that X must take the same truth value as Z. Running this in ECLiPSe yields:
[eclipse]: conjtest(X,Z).
X = X
Z = X
Delayed goals:
conj(X, X, X) infers most
Yes (0.00s cpu)
If the ic library is loaded more information can be extracted,
because the MSG of 0 and 1 is a variable with domain 0..1.
Thus the result of the above example is not only to equate X and Z
but to associate with them the domain 0..1.
The MSG of two terms depends upon what information is expressible in the MSG term. As the above example shows, if the term can employ variable domains the MSG is more precise.
By choosing the class of terms in which the MSG can be expressed, we can capture more or less information in the MSG. If, for example, we allow only terms of maximum depth 1 in the class, then MSG can only capture functor and arity. In this case the MSG of f(a,1) and f(a,2) is simply f(,), even though there is more shared information at the next depth.
In fact the class of terms can be extended to a lattice, by introducing a bottom ⊥ and a top ⊤. ⊥ is a term carrying no information; ⊤ is a term representing inconsistent information; the meet of two terms is the result of unifying them; and their join is their MSG.
We can now specify the Propia algorithm more precisely. The Propia constraint is
Goal infers Parameter
Parameter,
of OutTerm and S. Call it MSG
When infers most is being handled, the class of terms admitted
for the MSG is the biggest class expressible in terms of the currently
loaded solvers. In case ic is loaded, this includes variable
domain, but otherwise it includes any ECLiPSe term without variable
attributes.
The algorithm supports infers consistent by admitting only the
two terms ⊤ and ⊥ in the MSG class.
infers unique is a variation of the algorithm in which the
first step OutTerm := ⊤ is changed to finding a first solution
S to Goal and initialising OutTerm := S.
Propia’s termination is dramatically improved by the check that the next solution found is not an instance of OutTerm. In the absence of domains, there is no infinite sequence of terms that strictly generalise each other. Moreover, if the variables in Goal have finite domains, the same result holds. Thus, because of this check, Propia will terminate as long as each call of Goal terminates.
For example the Propia constraint
member(Var,List) infers Parameter will
always terminate, if each call of member(Var,List) does, even in
case
member(Var,List) has infinitely many solutions!
Propia computes the Most Specific Generalisation (MSG) of the set of solutions to a procedure. It does so without, necessarily, backtracking through all the solutions to the procedure. The MSG depends upon the annotation of the Propia call.
Figure 15.4: Most Specific Generalisation
If the finite domain solver is loaded then Goal infers most prunes
the variable domains so every value is supported by values in the
domains of the other variables. If every problem constraint was
annotated this way, then Propia would enforce arc consistency.
Propia generalises traditional arc consistency in two ways. Firstly
it admits n-ary constraints, and secondly it handles predicates
defined by rules, as well as ground facts. In the special case that
the goal can be “unfolded” into a finite set of ground solutions,
this can be exploited by using infers ac to make Propia run
more efficiently. When called with parameter infers ac,
Propia simply finds all solutions and
applies n-ary arc-consistency to the resulting tables.
Propia also generalises constructive disjunction. Constructive
disjunction could be applied in case the
predicate was unfolded into a finite set of solutions, where each
solution was expressed using ic constraints (such as equations,
inequations etc.).
Propia can also handle recursively defined predicates, like
member, exampled above, which may have an infinite number of
solutions.