Previous Up Next

15.3  Propia

Propia is an implementation of Generalised Propagation which is described in the paper [14].

15.3.1  How to Use Propia

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

15.3.2  Propia Implementation

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.

Most Specific Generalisation

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:
% Definition of logical conjunction

conjtest(X,Z) :-
    conj(X,Y,Z) infers most,
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.

The Propia Algorithm

We can now specify the Propia algorithm more precisely. The Propia constraint is
Goal infers Parameter 
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

15.3.3  Propia and Related Techniques

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.

Previous Up Next