Attributed Variables in Prolog



The most important thing you need to know about attributed variables is that Prolog application programmers normally need not use them. This chapter is intended mainly for Prolog library authors who want to improve or implement more declarative language constructs.

Attributed variables are a low-level mechanism for implementing declarative constructs. However, when considered in isolation, they have the potential to prevent and run counter to the declarative reading we want to apply to pure Prolog programs.

For this reason, attributed variables should only be used as a building block for higher-level mechanisms.

If you are a Prolog library author, your interest in this topic may be warranted. To application programmers, my recommendation is to use existing libraries that provide equivalent functionality under more declarative wrappers.

Prolog implementors may be interested in the Minato task and in the Equivalence task to assess the generality of their interface predicates.

How it started

Already the first Prolog system, sometimes called Prolog 0, supported the constraint dif/2.

To Prolog implementors and practitioners, the question soon became: By which general mechanism can we we implement further constraints conveniently, correctly and efficiently?

The first mechanism to solve this was proposed by Ulrich Neumerkel in his 1990 paper Extensible Unification by Metastructures.

Here is a salient quote from the paper:
When considering existing approaches of extensions to syntactic unification, we observe: highly specialized implementations, where the unification algorithm cannot be manipulated by the user (e.g. [Col87,JaLa87,vH89]), approaches too general to be implemented efficiently and too general to allow the reuse of existing Prolog programs [Ko84], or extensions allowing definitions in a procedural language [CLiST89] only.

Our approach focuses on a sufficient abstract yet efficient interface, which permits to write implementations of constraints in Prolog, neglecting the actual representation of the constrained variables. Metastructures are applicable, but not restricted to the following areas:

...
Among the projected use cases, stream-based side effect free I/O is already mentioned in the paper. This is now available in library(pio).

How it continued

Christian Holzbaur, who back then was a very close colleague of Ulrich Neumerkel, used metastructures in his 1990 dissertation, Specification of Constraint Based Inference Mechanism through Extended Unification, in which he implemented CLP(Q).

After this experience, and having observed some shortcomings of metastructures, Holzbaur proposed an alternative yet very strongly related mechanism called attributed variables.

Holzbaur later published a comparison paper, Metastructures vs. Attributed Variables in the Context of Extensible Unification.

The proposal by Christian Holzbaur was adopted in SICStus Prolog, one of the leading systems in the area of constraint programming.

To quote from the Attributed Variables section in the SICStus documentation:
This package implements attributed variables. It provides a means of associating with variables arbitrary attributes, i.e. named properties that can be used as storage locations as well as to extend the default unification algorithm when such variables are unified with other terms or with each other.

This facility was primarily designed as a clean interface between Prolog and constraint solvers, but has a number of other uses as well. The basic idea is due to Christian Holzbaur and he was actively involved in the final design. For background material, see the dissertation [Holzbaur 90].
If you are interested in more information about the origin of these developments, I recommend you ask the involved people in person.

The same interface is also implemented in other Prolog systems, such as Ciao.

How it was stymied

In 2002, Bart Demoen published a highly influential paper called Dynamic attributes, their hProlog implementation, and a first evaluation.

Bart Demoen is an extremely prolific and highly regarded member of the Prolog community, and several systems therefore adopted the approach he proposed.

The interface he proposed and implemented deliberately falls short in a critical respect. I quote from the paper and highlight the key passages:
4 Basic choice III: no pre_unify

The most profound difference between attributed variables in SICStus Prolog and ECLiPSe is the state of the variable at the moment the unifcation handler is called.

As an example: assume the attributed variable X has one attribute A (with module user) and X is unifed with the integer 666. In SICStus Prolog, verify_attributes is called with X still being unbound. In ECLiPSe, the unify handler is called with A as an argument - X has been bound to 666 already.

The SICStus Prolog behavior follows [6] which claims that it is important to have the variables as if not yet bound.

ECLiPSe people on the other hand (Joachim Schimpf) claim that this is not needed.

We do not want to take a stand in this issue: we had implemented at some point the full SICStus Prolog behavior (but on dynamic attributes of course) and were not convinced that the extra implementation complexity was worth the gain. However, we were not impressed by the manuals of SICStus Prolog and ECLiPSe, which claim that binding the X during a pre_unify yields unexpected results: in our opinion (and experience), it just shows that full support for pre_unify is too cumbersome to implement and maintain in a full system like SICStus Prolog or ECLiPSe. So we switched to the ECLiPSe model, but without the compromise to support pre_unify for compatibility reasons: Occam's razor is a blessing :-)
Unfortunately, despite the smiley, the above passage was taken seriously by Prolog implementors, and this limited interface is what for example SWI-Prolog now provides.

Occam's razor

Occam's razor, in its most popular version, states that "Entities are not to be multiplied without necessity".

I ask you, then, why do we have 3 different interfaces for attributed variables, two of which are clearly less general than the other?

A conservative approach, more than 20 years after the work of Neumerkel and Holzbaur, could look as follows:

Let us consider 4 widely used Prolog systems, such as SICStus, GNU-Prolog, ECLiPSe and SWI, and 4 widely used types of constraints: CLP(H), CLP(FD), CLP(B) and CLP(Q).

SICStus supports 4 of them. SWI supports 3 of them. ECLiPSe and GNU-Prolog support 2 of them. Of these systems, which has the most general interface for attributed variables? Take this system as the one we want to strive towards. By Occam's razor, chances are that they have only done what is needed to support the constraint solvers they provide.

What we have now

As we see from the above, the concrete features of attributed variables vary between Prolog systems. However, in all systems that provide attributed variables, we have essentially the following features at our disposal:
  1. We can attach information to logical variables.
  2. This information can be taken into account when a variable is being unified.
  3. This information can be displayed in answers on the Prolog toplevel.
In the following, we consider one specific implementation of these features in more detail.

Attributed variables in SWI-Prolog

Preliminaries

To illustrate the key concepts of attributed variables, we consider here SWI-Prolog because it is freely available. Therefore, you can easily gain experience with its interface for attributed variables.

I would like to stress again that attributed variables normally need not and also should not be used in typical Prolog applications. Instead, and also in SWI-Prolog, attributed variables are available to implement features from Constraint Logic Programming, and you should use these higher-level predicates instead in typical use cases.

When working with attributed variables, you need to know 3 kinds of interface predicates, in accordance with the features outlined above:
  1. Predicates for adding, changing and removing attributes.
  2. Predicates to reason about the unification of variables that have attributes attached.
  3. Predicates that let you display attributes on the toplevel in some form.
We now consider these kinds of predicates in turn. For more information, see especially 7.1 Attributed variables in the SWI-Prolog manual. Even though the details differ in other Prolog systems, the kinds of predicates are the same also in other systems.

Adding and changing attributes

In SWI-Prolog, an attributed variable is a relation between a variable, a module and a value.

Consequently, the predicate for adding and changing an attribute has three arguments:
put_attr(V, Module, Value):
Associate an arbitrary Prolog term Value with the logical variable V in module Module (a Prolog atom).

We can readily try out this predicate on the toplevel. For example:
?- put_attr(X, m, test).
put_attr(X, m, test).
    
We see that in response, the Prolog toplevel simply repeats what we said. Thus, the toplevel retains the important invariant that the answer is declaratively equivalent to the original query. In this concrete case, all there is to say is: The value test is associated with the variable X in module m, and that's exactly what this answer states. We call a variable that has an attribute attached an attributed variable.

We can attach arbitrary terms to arbitrary variables and modules:
?- put_attr(X, m1, test(Y)), put_attr(Y, m2, test(Z)).
put_attr(X, m1, test(Y)),
put_attr(Y, m2, test(Z)).
    
However, in typical cases, you will want to implement a single module (such as for example clpfd), and the predicates you provide will only reason about the attributes in that specific module.

Importantly, when you use put_attr/3 repeatedly with the same variable and module, then any previously attached value is simply overwritten. For example:
?- put_attr(X, m, hi),
   put_attr(X, m, ho).
put_attr(X, m, ho).
    
Thus, after these two calls, ho is the single remaining value that is attached to X in module m.

We say that put_attr/3 destructively modifies an attribute. For this reason, you can use put_attr/3 also as a somewhat more declarative and less error-prone alternative to setarg/3.

Note also that the effect of put_attr/3 is undone on backtracking. For example:
?- ( put_attr(X, m, hello)
   ; true
   ).
put_attr(X, m, hello) ;
true.
    
When the alternative is reported, we see from the absence of any goals besides true that no more attribute is attached to X. For this reason, assigning attributes to variables blends well with Prolog's built-in search strategy, and is similar to unification in that respect. We say that the modification is backtrackable.

An additional predicate called del_attr/2 lets you remove an attribute from a variable.

Unification of attributed variables

The key distinction between variables and attributed variables is what happens at the time of unification.

Attributed variables are special in that an extensible predicate is automatically invoked when they are unified. In SWI-Prolog, the particular predicate that is invoked is attr_unify_hook/2 residing in the module where the attribute is attached. You, the Prolog programmer, can provide a custom definition of this predicate, and it will be automatically invoked by the Prolog engine when a variable that has attributes attached is being unified.

For example, let us define a very rudimentary version of attr_unify_hook/2 in module m:
m:attr_unify_hook(X, Y) :- throw(cannot_unify(X,Y)).
    
With this definition, which simply throws an exception when it is invoked, we get for example:
?- put_attr(X, m, a),
   put_attr(Y, m, b),
   X = Y.
ERROR: Unhandled exception: cannot_unify(b,_612)
    
From the raised exception, we already see the asymmetry of this predicate: Contrary to what you may expect, attr_unify_hook/2 is not invoked with the arguments of the unification (which are the two variables X and Y), but rather with one attribute (namely b, which was the attribute of X), and one variable.

This happens because the hook is defined as follows:
M:attr_unify_hook(Attr, Value):
This hook is called after an attributed variable has been unified with Value, which may be another attributed variable. Attr is the attribute that was associated with the variable in the module M, and Value is the new value of the variable. If this predicate fails, the unification fails. If Value is another attributed variable, the hook often combines the two attributes and associates the combined attribute with Value, using put_attr/3.
The way in which this predicate works makes it insufficient to implement important classes of constraint solvers. We discuss this point below. For now, let us make do with what we have.

First, let us try out what the documentation states: For example, let us make the unification fail.
m:attr_unify_hook(_, _) :- false.
    
Example query and answer:
?- put_attr(X, m, n(1)),
   put_attr(Y, m, n(2)),
   X = Y.
false.
    
OK, this works as advertised. In this example and the following, we use compound terms of the form n(N) to represent the integer N. We could also use the integers directly instead. However, this would risk ending up with a defaulty representation, and also prevent us from symbolically distinguishing attributes from logical variables in the code below.

Second, let us modify the involved attributes upon unification. If a unification involves two (or more) logical variables, we must state how such a unification affects the involved variables.

Let us extend the example from above: In the above case, we have associated the Prolog terms n(1) and n(2) with the variables X and Y and module m. To gather experience with the interface, let us say that upon unification of two variables with respective attributes n(A) and n(B), where A and B are integers, we want to attach the new attribute n(C) to the resulting (single) variable, where C is the sum of A and B.

To accomplish this, we need a way to reason about existing attributes of variable. The predicate get_attr/3 is available for this purpose:
get_attr(V, Module, Value):
This predicate succeeds if and only if Value is the attribute of the variable V in module Module.

Thus, we shall now implement the following steps:
  1. Upon unification of two variables with attributes from module m, fetch these attributes.
  2. Compute the sum of these attributes, using integer arithmetic.
  3. Attach the sum as the new attribute to the variable. Note that we speak here about the variable because there is only a single variable remaining after the unification has taken place.
In Prolog, this becomes:
m:attr_unify_hook(n(A), Var) :-
        get_attr(Var, m, n(B)),      % step (1)
        C #= A + B,                  % step (2)
        put_attr(Var, m, n(C)).      % step (3)
    
Note that at the time the hook is invoked, the attribute of one of the variables (we do not know which) is already available as an argument of attr_unify_hook/2, so we only have to use get_attr/3 once.

Now, let us try it out:
?- put_attr(X, m, n(1)),
   put_attr(Y, m, n(2)),
   X = Y.
X = Y,
put_attr(Y, m, n(3)).
    
And indeed this works: After the unification, n(3) is associated with the resulting single variable, which is X or, equivalentlyY, and 3 is the result of 1+2.

The following fails, simply because get_attr/3 fails if its first argument is not a variable:
?- put_attr(X, m, n(1)),
   X = a.
false.
    
In fact, with the above definition of attr_unify_hook/2, only very specific kinds of unifications will succeed. In particular, every unification with a ground value will fail. However, in actual constraint systems, we are very interested in ground terms, because they typically represent concrete solutions.

Let us therefore generalize the above definition of attr_unify_hook/2 (in module m) in such a way that it still illustrates a key feature of the whole interface, namely the ability to selectively veto unifications. For example, in our concrete case, let us allow unifications with a concrete integer iff that integer matches the associated integer value that is stored in the involved variable's attribute.

We hence must distinguish two different cases when two terms X and Y are unified. Let us consider it from the perspective of X, i.e., let us suppose that attr_unify_hook/2 is invoked with the attribute of X as the first argument. (Of course, the other case is completely symmetric, but we need to draw this distinction to discuss the cases.) Then, either Y is an integer k. In that case, we must veto the unification (i.e., fail) if k does not match the integer that is stored in the attribute of X. Or Y is an attributed variable. In that case, we proceed exactly as previously: We compute the sum of the two integers that are stored in the attributes of the involved variables, and associate that sum with the unified variable.

In Prolog, we can express this distinction with the built-in predicate integer/1:
m:attr_unify_hook(n(A), Other) :-
        (   integer(Other) ->
            Other = A
        ;   get_attr(Other, m, n(B)),
            C #= A + B,
            put_attr(Other, m, n(C))
        ).
    
Here are a few sample queries and their results:
?- put_attr(X, m, n(1)), X = 1.
X = 1.

?- put_attr(X, m, n(1)), X = 3.
false.

?- put_attr(X, m, n(1)),
   put_attr(Y, m, n(2)),
   X = Y,
   X = 3.
X = Y, Y = 3.
    
Thus, everything seems to work as intended. We have successfully created a simplistic constraint solver, which admittedly has quite peculiar semantics but implements what we have outlined. However, this concrete solver has a very severe declarative flaw, which becomes apparent if you eliminate the goal X = Y in the above conjunction:
?- put_attr(X, m, n(1)),
   put_attr(Y, m, n(2)),
   X = 3.
false.
    
In this case, generalizing a query (by removing a constraint) has created a more specific program (which is now equivalent to false). This violates elementary properties we expect from logic programs and prevents for example declarative debugging.

The key takeaway from this is that the interface for attributed variables does not by itself provide any guarantees of the resulting constraint solver. You, the programmer, must implement your system in such a way that desirable properties are preserved in resulting programs. We return to this point below.

For now, let us conclude this section with a more interesting and also more realistic example: The SWI-Prolog documentation contains an example of a simplistic constraint solver over finite domains, where the attribute of each involved variable (in the module called domain) is an ordered list of elements, representing the admissible domain of the variable.

A suitable unification hook for such a constraint solver could look like this:
domain:attr_unify_hook(Dom1, Other) :-
        (   get_attr(Other, domain, Dom2) ->
            ord_intersection(Dom1, Dom2, Dom),
            dif(Dom, []),
            (   Dom = [Value] ->
                Other = Value
            ;   put_attr(Other, domain, Dom)
            )
        ;   ord_memberchk(Other, Dom1)
        ).
    
Informally, we can read this as:
  1. If Other is a variable that has an associated domain Dom2, then we build the intersection Dom = Dom1Dom2. This ordered list contains all elements that are admissible for both variables that have been unified.
  2. We only proceed if Dom is different (dif/2) from the empty list [], and hence there is at least one remaining domain element that is admissible for the resulting unified variable.
  3. If Dom has only a single remaining element, then that element must be equal to the unified variable (because there is no other choice).
  4. Otherwise, assign the intersection Dom as an attribute to the unified variable.
  5. If Other has no associated domain, then the unification is only admissible if Other is a member of the domain Dom1.
In addition, let us use the following definition to associate a variable with its domain:
domain(X, List) :-
        list_to_ord_set(List, Dom),
        put_attr(X, domain, Dom).
    
With these definitions in place, we can query:
?- domain(X, [a,b,c]),
   domain(Y, [c,d,e]),
   X = Y.
    
In response, we get the concrete solution:
X = Y, Y = c.
    
This works because upon unification, the hook is invoked, builds the intersection of the two domains, determines that they have only a single element in common, and hence unifies the resulting variable with that element. Note that X and Y have become completely indistinguishable. Unification has truly unified them.

Exercise (hard): The following property is highly desirable for a constraint solver. Prove that it holds in this case, or provide a counterexample:
For every Prolog query Q that consists only of domain/2 and (=)/2 goals, removing one of the goals makes the resulting query Q' at least as general as Q, in the sense that the set of solutions of Q is a subset of those of Q'.

Displaying attributes

In an actual constraint solver, we are not content with answers that look like put_attr(X, m, test). Instead, what we expect from a constraint solver is a representation of remaining attributes that is meaningful to humans. Thus, we expect a constraint solver to emit more high-level Prolog goals as answers, which have a well-defined meaning no matter how they are internally implemented.

For this purpose, there is the DCG nonterminal M:attribute_goals//1. In SWI-Prolog, you can define this nonterminal in a module M, and it is automatically invoked by the Prolog engine for each variable X that has an attribute in M. It is defined as follows:
M:attribute_goals(V):
This is a DCG nonterminal describing a list of Prolog goals which caused the presence of V's attributes in module M. This means that executing these goals should lead to equivalent attributes on X in module M.

For example, let us apply this feature to our simple finite domain constraint solver that we considered above. It only has a single interface predicate, called domain/2. Ideally, answers that are reported on the toplevel should only use public interface predicates, since their meaning is known to users.

Thus, it remains for us to translate attributes to so-called residual goals, using the above nonterminal. In the concrete case above, we can do it like this:
domain:attribute_goals(Var) -->
        { get_attr(Var, domain, Dom) },
        [domain(Var, Dom)].
    
This simply fetches the attribute from module domain, and describes a list with a single goal. Here is an example that illustrates that this predicate is automatically invoked by the toplevel when reporting answers:
?- domain(X, [a,b,c]).
domain(X, [a, b, c]).
    
It also works for more complex queries:
?- domain(X, [a,b,c]),
   domain(Y, [b,c,d]),
   X = Y.
X = Y,
domain(Y, [b, c]).
    
Using this mechanism, you can always translate internal attributes to Prolog goals that are more meaningful to users.

The toplevel provides this functionality by internally invoking the predicate copy_term/3. This predicate creates a copy of variables that may be involved in constraints, and uses attribute_goals//1 to create a list of goals that, when called, create equivalent attributes on the copy. You can use copy_term(X, X, Gs) to reason about the constraints Gs that X is involved in. Note that a list of goals is used, since this is a clean representation of goals that allows convenient further analysis.

Pitfalls

Working with attributed variables is extremely error-prone. I have considerable experience with such interfaces: I have contributed CLP(FD) to SWI-Prolog, and ported the whole system to SICStus Prolog as CLP(Z). I have contributed CLP(B) to SWI-Prolog, and created a port to SICStus Prolog. I have a doctoral degree in the area of constraints: My dissertation is called Correctness Considerations in CLP(FD) Systems and it deals with exactly such issues among others. Still, I find it extremely hard to work in particular with the SWI-Prolog interface.

The core shortcoming of the SWI-Prolog interface for attributed variables is that attr_unify_hook/2 is only invoked after a variable has already been unified.

This may seem quite innocent at first: After all, the (previous) attribute of that variable is an argument of attr_unify_hook/2, so everything we need to know is available, right? Let us suppose that this is the case (although it isn't, as we discuss below). Even then, several variables may at once become instantiated, for example via a goal like [X,Y] = [0,1]. It is easy to see that if such a unification involves n variables, then there are at least 2n different kinds of possible instantiation patterns that may arise in a single unification. Nobody is able to think all cases through completely. An example of a situation that can arise due to simultaneous unifications is explained in commit 9c8ea20b7. A highly experienced expert in constraint programming ran into the same issue in his own constraint solver.

But still, maybe the interface is not to blame, right? Maybe we have only not tried hard enough to work with the interface. After all, only poor craftspeople blame their tools, right?

Wrong! If an interface not only makes possible but downright enforces such mistakes, then it is time to reconsider the interface. Normally, such issues should be reason enough to seriously rethink the interface. However, in the Prolog community, the error-prone nature of this interface is not by itself enough reason for change. Traditionally, it is performance that matters most, and who cares about correctness as long as your system is fast, right? Therefore, I give you a second argument:

The SWI-Prolog interface is not sufficient to express important classes of constraint solvers. Consider again the unification [X,Y] = [0,1]. This means that the attributes of both variables become unavailable at the same time. It is true: When attr_unify_hook/2 is run for X, you have access to its former attribute. But at that time, you can no longer access the former attribute of Y via get_attr/3, and in fact you can no longer even tell that Y was a variable. The next section shows an example where this is needed, but not possible.

Minato task

Let us now consider a specific task, which is easily encountered when implementing a CLP(B) system based on Zero-suppressed decision diagrams (ZDDs). ZDDs are a very important data structure, and Donald Knuth has called them "the most beautiful construct in computer science" in a talk.

I call this task Minato task, in honor of 湊 真一(みなと しんいち), MINATO Shin-ichi, the inventor of ZDDs (see Zero-Suppressed BDDs for Set Manipulation in Combinatorial Problems). We shall use this task to determine whether a Prolog system's interface predicates for attributed variables are general enough to naturally express a certain class of constraints that are of great practical importance.

A ZDD is a decision diagram. This means that we can simply follow the lines of the diagram to arrive at a truth value. The nodes of a ZDD are branching variables: If a variable is 1, then we take the plain line, and if a variable is 0, then we take the dotted line. In that respect, a ZDD is like a Binary Decision Diagram (BDD). However, a ZDD is interpreted with the following distinguishing twist: If a variable does not appear on a path that leads to true, then that variable must be equal to 0.

For example, here is a ZDD that represents the truth value of the Boolean function X xor Y:

We can represent a ZDD as a Prolog term. The truth values true and false can be represented as atoms, and an inner node can be represented as ( X → Then ; Else ), where: In analogy to Prolog syntax, Then is taken to mean that X is 1 (true), and Else means that X is 0 (false).

For example, the ZDD above can be represented as:
( X -> true ; ( Y -> true ; false ) )
    
Both variables, X and Y, participate in this decision diagram. Therefore, to reason about such constraints in Prolog, it is natural to attach this diagram as an attribute to both variables. Here is how we can do this with put_attr/3:
?- ZDD = ( X -> true ; ( Y -> true ; false ) ),
   put_attr(X, zdd, ZDD),
   put_attr(Y, zdd, ZDD).
    
We now consider a series of unifications, and you tell us how you use your system's interface predicates to arrive at the correct truth values for X and Y.
  1. As a start, consider the following unification: X = 0.

    You reply for example with: That's easy, I simply take a look at the decision diagram, which now is:
    ( 0 -> true ; ( Y -> true ; false ) )
        
    Since the first branching variable is now instantiated, it is clear which branch we must take, so we can replace the whole diagram with:
    ( Y -> true ; false )
        
    From there, further unifications are easy.

  2. Here is a slightly harder case: X = 1.

    This means that the ZDD could be reduced to:
    true
        
    But wait, that's not all! As we explained, a variable that does not appear in a path to true must be equal to 0. In this case, Y is such a variable, so we must set it to 0. But how? Well, one way to do this is to keep track of all variables that have so far appeared in constraints, and to represent the ZDD for example as a pair of terms, such as:
    ( X -> true ; ( Y -> true ; false ) )-[X,Y]
        
    This means that in the above case, we would end up with:
    true-[1,Y]
        
    and from there it is easy to state that Y = 0.
  3. Here is a third case: [X,Y] = [1,1].

    And you solve the Minato task by telling us how your interface predicates can be used to determine that this unification is not admissible due to the constraints the variables are involved in.

    For comparison, the unification must succeed if the ZDD is for example:
    ZDD = ( X -> Inner ; Inner ), Inner = ( Y -> true ; false )
            
    This illustrates that you cannot look into other branches of the ZDD to recover any information about Y.
Note especially the following: There is no doubt that this issue can be solved somehow, even with a very primitive interface for attributed variables. One example would be to duplicate all kinds of attributes so that they are available redundantly in all data structures that occur anywhere. However, an interface that demands such contortions cannot be taken seriously. In my view, the key questions are: In my opinion, we should strive for convenient and general interface predicates that make mistakes as unlikely as possible. People have suggested that I "want the SICStus interface". I would in fact prefer an interface that provides even stronger guarantees. However, from those interfaces that are currently available, I consider the SICStus interface the most desirable, and therefore recommend its emulation.

Solution with SICStus Prolog

For completeness, here is a possible solution of the Minato task, using SICStus Prolog and its very general interface for attributed variables.

First, of course, let us use a clean representation of nodes, such as: Note in particular that we can now symbolically distinguish leaves from inner nodes, thanks to the b/1 wrapper we use for concrete Boolean values.

As a warm-up, let us express the so-called restriction of a ZDD. This means the relation between one ZDD, and a new ZDD that arises when the variable Var is unified with the concrete Boolean truth value Value, which is either 0 or 1:
zdd_restriction(b(T), _, _, b(T)).
zdd_restriction(( Var0 -> Then0 ; Else0), Var, Value, ZDD) :-
        (   Var0 == Var ->
            (   Value =:= 0 -> ZDD = Else0
            ;   Value =:= 1 -> ZDD = Then0
            ;   throw(no_boolean)
            )
        ;   zdd_restriction(Then0, Var, Value, Then),
            zdd_restriction(Else0, Var, Value, Else),
            ZDD = ( Var0 -> Then ; Else )
        ).
    
Example query:
?- zdd_restriction((X -> b(true) ; b(false)), X, 1, ZDD).
ZDD = b(true).
    
Note that the above method is an extremely inefficient way to compute the restriction of a ZDD. Making it faster by using memoization is left as an exercise.

We need a single public predicate to demonstrate how our solution works: variables_set_zdd(Vs, ZDD) shall attach the given ZDD as an attribute to all variables in Vs. The attribute shall be of the form zdd_vs(ZDD, Vs) and store the ZDD as well as all variables we want to reason about.

In SICStus Prolog, we use library(atts) to declare and reason about attributes. For example:
:- use_module(library(atts)).

:- attribute zdd_vs/2.

variables_set_zdd(Vs, ZDD) :-
        maplist(set_zdd(ZDD, Vs), Vs).

set_zdd(ZDD, Vs, V) :-
        put_atts(V, +zdd_vs(ZDD, Vs)).
    
We are now ready to implement verify_attributes/3, which is a more general and more declarative form of attr_unify_hook/2. In SICStus Prolog, this hook is invoked before variables with attributes are unified. It lets us conveniently reason about all variables. When a ZDD is reduced to the leaf node b(true), then all variables that were not encountered in that branch must be 0. We enforce this with a DCG that describes a list of V=0 goals, one for each remaining variable:
verify_attributes(Var, Value, Goals) :-
        (   get_atts(Var, +zdd_vs(ZDD0,Vs)) ->
            (   integer(Value) ->
                zdd_restriction(ZDD0, Var, Value, ZDD)
            ;   throw(aliasing_not_implemented)
            ),
            phrase(remaining_vars_0(ZDD, Var, Vs), Goals)
        ;   Goals = []
        ).

remaining_vars_0(b(true), Var, Vs) --> all_others_0(Vs, Var).
remaining_vars_0((_;_), _, _) --> [].

all_others_0([], _) --> [].
all_others_0([V|Vs], Var) -->
        (   { var(V), V \== Var } -> [V=0]
        ;   []
        ),
        all_others_0(Vs, Var).
    
The full code is available from: minatotask.pl

A few sample queries are included. In particular, the Minato task works as desired:
?- ZDD = ( X -> b(true) ; ( Y -> b(true) ; b(false) ) ),
   Vs = [X,Y],
   variables_set_zdd(Vs, ZDD),
   Vs = [1,1].
no
    
It is clear that the general and declarative SICStus interface has some performance impact in comparison with more limited hooks. However, in addition to its generality, SICStus Prolog is also widely known as one of the most efficient Prolog systems. The argument that we should sacrifice correctness for efficiency, even if it were a sensible one, can therefore not be applied in this case.

Equivalence task

We now consider a second task, which I call Equivalence task, and which also arises in connection with CLP(B). I hope this task is useful for you to assess the generality and expressiveness of your system's interface predicates.

The SICStus documentation states for sat(Expression), which is true iff Expression is satisfiable:
If a variable X, occurring in the expression, is subsequently unified with some term T, this is treated as a shorthand for the constraint
| ?- sat(X=:=T).


To implement this in Prolog, an interface for attributed variables must have the ability to reason about a unification before it takes place. Again, a different implementation strategy necessitates highly unnatural and error-prone encodings.

Consider for example the query:
?- sat(X=:=Z), X = X+1.
    
and ask yourself how this could be handled in your system. According to the SICStus documentation, it should be equivalent to:
?- sat(X=:=Z), sat(X=:=X+1).
    
This is satisfiable and should therefore yield for example:
X = Z, Z = 1.
    
If your system cannot yield such an answer, think about what a suitable approximation may look like, and how it can be computed.

For example, with your interface predicates for attributed variables, can you at least somehow distinguish the above case from:
?- sat(X=:=Z), X = ~X.
    
which ought to be equivalent to:
?- sat(X=:=Z), sat(X =:= ~X).
    
and hence fail.

Further reading and future work

Attributed variables are typically used to implement constraint solvers on top of Prolog. This is their most important, but not their only use case.

Especially for Prolog programs that need destructive assignments or reason about graphs, attributed variables are often a good and convenient representation. Do not get carried away with destructive assignment though, because it destroys the relational nature of your code.

A good approach is to encapsulate the use of attributed variables behind more declarative interface predicates of your libraries. For example, consider the implementation of Tarjan's algorithm to find the so-called Strongly Connected Components of a graph: scc.pl. In that case, the use of attributed variables allows us to implement the algorithm with close to asymptotically optimal performance.

I have described some of the issues in the peer-reviewed publication The Boolean Constraint Solver of SWI-Prolog (2016), and in the extended journal version Boolean Constraints in SWI-Prolog: A comprehensive system description (2018).

To me, the current state of interface predicates for attributed variables can at best be considered as definitely deserving much additional work. For instance, what would be the best way to let different constraint solvers cooperate in the intersection of their domains?

If you have a good idea for new interface predicates, consider writing a meta-interpreter that lets you present the mechanism to the community by extending an existing Prolog system without the need for low-level changes. Alternatively, follow the example of Douglas Miles and extend an existing engine directly.


More about Prolog


Main page