Attributed Variables: An Introduction

[Markus Triska]

Hi all,

I have uploaded an introduction to Attributed Variables:

https://www.metalevel.at/prolog/attributedvariables

This is part of a collection of texts that describe modern Prolog features.

This new section on attributed variables is mostly intended towards Prolog library authors, such as Kuniaki Mukai whose inquiries have recently spawned a discussion of these features. For application programmers, I recommend to use more declarative wrappers.

To Prolog implementors, I would like to point out a task I call Minato task in honor of MINATO Shin-ichi, the inventor of ZDDs:

https://www.metalevel.at/prolog/attributedvariables#minatotask

I hope that this task helps you to assess the generality of your Prolog system's interface predicates for attributed variables.

Please also see the mentioned papers and other resources.

Attributed variables are the basic building block for implementing declarative features such as constraints on top of Prolog, and I hope that this resource helps us to obtain more general, more convenient, and less error-prone interfaces in the future.

Thank you and all the best,

Markus

[Kuniaki Mukai]

Hi Markus,

Suppose c(x,y,z) is a boolean constraint over variables x,y,z.
I believe that it is a common sense that c(0,y,z) is
more easy to solve than c(x, y, z).
Against such common sense, you seem to claim that
there exists a constraint theory in which the reverse is often
the case, and ZDD is such an excellant theory, which is a reason
of your requirement on pre unification hook.

Pardon me if the above is my superficial reading your post.
I am curious enough so that I am searching my memory
for another theory which supports your “claim."

Kuniaki Mukai

> --
> You received this message because you are subscribed to the Google Groups "SWI-Prolog" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to swi-prolog+...@googlegroups.com.
> Visit this group at https://groups.google.com/group/swi-prolog.
> For more options, visit https://groups.google.com/d/optout.

[Jan Wielemaker]

On 08/31/2017 05:08 PM, Markus Triska wrote:
> Hi all,
>

> I have uploaded an introduction to *Attributed Variables*:

I'm not sure `introduction' is the right word :) It is a very clear
expression of the history, your concerns and a good test case. Thank
you! I think from here there are at least three possible outcomes:

- pre-unification is unavoidable
- there is a different hook possible on post unification to solve
such problems elegantly
- there is a structured approach using the current API to solve
problems like this

As we have seen with Douglas, pre-unification is far from trivial to get
right internally. I don't know how much time Douglas invested. I
invested about a month and it felt like a badly designed roller coaster.
That might be caused by design choices in SWI-Prolog. After all, attvars
where added late in the process when already a lot of other problems not
around in Prolog's of the eighties were resolved, each pushing the
system in some direction. As Bart makes similar claims though, it may be
hard in general. It surely comes at a price in the Prolog engine, both
in terms of complexity and performance.

As you state yourself: "The most important thing you need to know about
attributed variables is that Prolog application programmers normally
need not use them". This, to me, implies we can shift the border without
affecting "Prolog application programmers".

Thanks --- Jan

> https://www.metalevel.at/prolog/attributedvariables
>
> This is part of a collection of texts that describe modern Prolog features.
>
> This new section on attributed variables is mostly intended towards
> Prolog library authors, such as Kuniaki Mukai whose inquiries have
> recently spawned a discussion of these features. For application
> programmers, I recommend to use more declarative wrappers.
>

> To Prolog implementors, I would like to point out a task I call *Minato
> task* in honor of MINATO Shin-ichi, the inventor of ZDDs:

>
> https://www.metalevel.at/prolog/attributedvariables#minatotask
>
> I hope that this task helps you to assess the generality of your Prolog
> system's interface predicates for attributed variables.
>
> Please also see the mentioned papers and other resources.
>
> Attributed variables are the basic building block for implementing
> declarative features such as constraints on top of Prolog, and I hope
> that this resource helps us to obtain more general, more convenient, and
> less error-prone interfaces in the future.
>
> Thank you and all the best,
> Markus
>
>
>

> --
> You received this message because you are subscribed to the Google
> Groups "SWI-Prolog" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to swi-prolog+...@googlegroups.com

> <mailto:swi-prolog+...@googlegroups.com>.

[Kuniaki Mukai]

Dear Markus,

About boolean constriant I have noticed that I know only following basics.

1. SAT is NP complete in theory.

2. There are many “subclasses"of SAT problem which is solved easily, for
simplest example:
if a and b and c = true
then a=b=c= true (no need to check 8 = 2x2x2 cases).

2'. if (a-> false ) = true, then a=true. (no need to check “all" 2 cases).

I think clp(B) supports these special rules using ZDD, but
no more than my guessing.

I would appreciate if you add to your page on an explanation of
your requirement on pre unify_hook for those who have only
basics of Boolean constraints like me. So far I must be missing
your point between pre unify_hook and such basics.

Kuniaki Mukai

> To unsubscribe from this group and stop receiving emails from it, send an email to swi-prolog+...@googlegroups.com.

[Jan Wielemaker]

I've created a playground with a first try on SWISH:

https://swish.swi-prolog.org/p/Minato%20task.swinb

For this I extended SWISH to support attributed variables directly using
put_attr/2, which puts attributes for the current module. This provides
us with a nice forum for discussion and testing.

The solution is far from optimal wrt. performance but can most likely
be improved quite easily. I think it is also wrong (documented in the
notebook), but fixing that won't change the approach. I do think that
the solution is satisfies the required transparency. Once we agree it
can be solved this way we can discuss the efficiency.

Please shoot!

Cheers --- Jan

[Markus Triska]

Dear Kuniaki,

On Friday, September 1, 2017 at 12:58:20 PM UTC+2, Kuniaki Mukai wrote:

I would appreciate if you add to your page on an explanation of
your requirement on pre unify_hook for those who have only
basics of Boolean constraints like me. So far I must be missing
your point between pre unify_hook and such basics.

OK, I have added a solution of the Minato task, which is expressed in terms of the SICStus interface for attributed variables:

https://www.metalevel.at/prolog/attributedvariables#minatotask_sicstus

This is the interface that was implemented in SICStus Prolog in cooperation with Christian Holzbaur. You can download a free evaluation version of SICStus today, and try out the code I have included, to see how it works with SICStus.

The challenge is to make equivalent semantics possible in SWI-Prolog, so that this task can also be solved satisfactorily in SWI-Prolog.

Implementing the SICStus interface is one possible approach, which requires profound knowledge of Prolog implementation techniques and likely takes a lot of work. There are other, simpler approaches, that may be more suitable for SWI-Prolog and still allow to express such situations.

Please have a look at the sample code: You can express most of it in SWI-Prolog. In the SWI-Prolog git tree, there is a branch called verify-attributes, where Douglas Miles had added a prototype implementation of verify_attributes/3. You can use it to express this example, if you want to take a look at different variants of interface predicates. verify_attributes/3 is also available in a few other Prolog systems.

Please take a look at the code and the sample queries, and let me know if you want to discuss any aspect in detail.

[Markus Triska]

Hi Jan,

thank you for taking a look, and for providing this environment!

A variable may occur on both sides of a ZDD. For example, the formula X*Y + ~X*Y corresponds to the ZDD:

( X -> ( Y -> true ; false) ; ( Y -> true ; false ) )

Therefore, we generally must not set all variables occurring in the other branch to 0. The above example shows a case where Y must be 1 if X is 1, although Y occurs in the other branch too.

ZDDs are actually graphs, so in a real implementation of ZDDs, there would only be a single node for ( Y -> true ; false ), not two as in the case above. However, we need not consider such sharing for now.

Please compare your code with the SICStus reference implementation I posted.

There is also a (very limited) ZDD-based version of library(clpb) available:

https://github.com/triska/clpb/tree/master/zdd

You can use it to inspect the ZDDs of Boolean expressions. For example:

?- zdd_set_vars([X,Y]), 

   sat((X*Y) + (~X* Y)).

This yields the ZDD mentioned above, with sharing of isomorphic subgraphs:

node(4)-(X->node(3);node(3)),

node(3)-(Y->true;false),

All the best,

Markus

[Kuniaki Mukai]

Hi Jan,

Sorry for so basic questions about your examples:

?- ZDD = ( X -> b(true) ; ( Y -> b(true) ; b(false) ) ),
Vs = [X,Y],
variables_set_zdd(Vs, ZDD),
Vs = [1,1].

no

Is ZDD a just prolog term ? if so what is the semantics of the ZDD ?

Is ‘->’ a boolean implication ?
is ‘;’ the boolean ‘or’ (disjunction) ?
is 0 for false or true?

For me, result of the query depends on meanings of
these symbols; ((true -> true) or ((true->true) or false)) = true
in Boolean, isn’t it ? Surely I must be missing something.
I am far from before discussing details.

Kuniaki Mukai

[Markus Triska]

Dear Kuniaki,

On Friday, September 1, 2017 at 5:54:30 PM UTC+2, Kuniaki Mukai wrote:

Is ZDD a just prolog term ?  if so what is the semantics of the ZDD ?

Yes, in the sample code and also in the document, I represent a ZDD as a Prolog term.

There are two kinds of nodes in a ZDD:

- leaves, i.e., the Boolean truth values TRUE and FALSE

- inner nodes. Each inner node has exactly one branching variable and exactly 2 children.

There are many ways to represent a ZDD in Prolog, so you are free to use your own representation if it helps to solve the task.

For a start, I suggest the following representation, which I have used in the SICStus sample solution:

- b(T) represents the truth value T (true or false)

- the term ( X -> Then ; Else ) represents an inner node where X is the branching variable, and Then and Else are its children.

If the branching variable X is 1 (true), then the ZDD reduces to Then. If X is 0 (false), then the whole ZDD reduces to Else. Therefore, I have used if-then-else syntax, in analogy to Prolog (although it strictly speaking is "if-then" combined with "or").

You can also choose any other Prolog terms to represent truth values, such as true and false. I have used the integers 0 and 1 for compatibility with library(clpb) and library(clpfd). However, any representation is admissible.

To evaluate a ZDD under a given assignment of variables, you simply follow the inner nodes, taking the indicated branches, until you arrive at a leaf. The leaf where you arrive indicates the truth value of the whole formula.

Now the key characteristic of ZDDs: All variables that are not encountered in your traversal must be 0, however you represent it. Therefore, it is called Zero-suppressed decision diagram: All variables which are 0 are suppressed in the diagram if possible.

For example, if the ZDD is ( X -> true ; false ), and X is 1, then we arrive at true, so the formula is true, but only if all other variables are 0.

For example, this ZDD ( X -> true ; false ) represents the formula X * ~Y. You can use the ZDD-based library(clpb) to gather experience with ZDDs:

https://github.com/triska/clpb/tree/master/zdd

Please see the comments in the file for more information about its usage.

 

For me, result of the query depends on meanings of
these symbols;  ((true -> true) or ((true->true) or false))  = true
in Boolean, isn’t it ? Surely I must be missing something. 

Yes, true. The twist with ZDDs is that the variables you have not encountered in the branch you pursued must be set to 0. Only in that case does the whole formula evaluate to true (if you arrived at true at all).

To gather experience with ZDDs, I recommend to start with really simple examples, such as with one or two variables, and see how they are evaluated when you take these rules into account, maybe in connection with the CLP(B) system mentioned above.

Thank you for your interest in this topic, I really appreciate it!

All the best,

Markus

[Kuniaki Mukai]

I have seen reduce/2 in Jan’s SWISH page on ZDD. To me, it looks
like saying the following.

For a boolean expression L, there is a some data structure
by which there is an incremental algorithm to compute a set ZDD(L)
of assignment of the variables appearing in L such that

f in ZDD(L) if and only if f satisfies L

The algorithm above is not brute force but something smarter.

Kuniaki Mukai

[Markus Triska]

Dear Kuniaki,

yes, you are absolutely right. More precisely, once a ZDD is constructed, you can generate in time that is linear in the number of variables a solution to a Boolean formula. This is a major attraction of ZDDs, in addition to many other applications that you can also efficiently perform on them. Thus, if constructing the ZDD were in P, then P = NP. However, constructing a ZDD may take space (and hence time) that is exponential in the number of variables.

So, ZDDs and decision diagrams in general are simply one more tool in our toolbox, very useful for counting and some optimization tasks, as well as symbolic reasoning over circuits and several other interesting use cases.

You can think about ZDDs (and BDDs) as compressed truth tables, where "compression" is used in the sense that it may or may not compress significantly or even at all.

Many thanks again for your interest in this area!

All the best,

Markus

[Kuniaki Mukai]

Thank you for quick answer to my basic questions.

Now I feel I get touching the problem a little bit.

Is ZDD order free algorithm wrt unification of variables ?

[X = 1, Y =1] and [Y=1, X =1] may yield different results?

I am not sure on that, but you look anxious for that; it depends
on ZDD theory.

Kuniaki Mukai

[Fabrizio Riguzzi]

Hi Markus,

have you considered using the BDD form that are used by CUDD? They have a single leaf node, 1, and the else arcs can be complemented, see for example

http://cplint.ml.unife.it/example/multiple_paths.pl

where else arcs are dashed when regular and dotted when complemented.

Negation in this case is very cheap which is useful for highly nonmonotonic formulas.

Best

Fabrizio

> To unsubscribe from this group and stop receiving emails from it, send an email to swi-prolog+unsubscribe@googlegroups.com.

> Visit this group at https://groups.google.com/group/swi-prolog.
> For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "SWI-Prolog" group.

To unsubscribe from this group and stop receiving emails from it, send an email to swi-prolog+unsubscribe@googlegroups.com.

[Markus Triska]

Dear Kuniaki,

we are now swiftly getting to the core of the issue:

First, yes, unification ought to be commutative. ZDDs are in harmony with this requirement, since edge contraction on graphs is commutative, and making a decision in a ZDD corresponds to a contraction of one of its edges.

The sample code I posted for the so-called restriction of a ZDD preserves commutativity as well.

However, with the SWI interface, in a unification such as [X,Y] = [1,1], significant information is lost in comparison to, say, the conjunction of goals (X = 1, Y = 1).

In the case of a simultaneous unification such as [X,Y] = [1,1], when the unification hook is invoked for X, we have lost the information that Y was a variable, because it is now also instantiated to a concrete integer.

This information cannot be recovered from other branches of the ZDD. I have added an example to the task description to illustrate this.

Thank you for your interest!

Markus

[Kuniaki Mukai]

Dear Markus,

If ZDD maintains a list of uninstantiated variables,
then it seems to me that simultanous unification
should have no problem, provided that the cost of
the maintenance is low.

I am saying without reading ZDD papers. It should be
time for me to stop here to say more. However thanks to
Markus and Jan, I got to know that ZDD is interesting
in a similar way to "Grobner base" and "Knuth-Bendix";
they take high cost to build their “normal form",
but then the normal form are powerful and useful enough
to pay the cost.

Is there a definitive formal paper on ZDD available for downloading
for people interested ?

Kuniaki Mukai

[Jan Wielemaker]

On 09/01/2017 05:40 PM, Markus Triska wrote:
> Hi Jan,
>
> thank you for taking a look, and for providing this environment!

Thanks for your explanation and example code. I think this is detailed
enough to chew on and see whether a clean solution is possible. Nice
puzzle! Not much time to work on it the coming days :(

Cheers --- Jan

> A variable may occur on both sides of a ZDD. For example, the formula
> X*Y + ~X*Y corresponds to the ZDD:
>
> ( X -> ( Y -> true ; false) ; ( Y -> true ; false ) )
>
>
> Therefore, we generally must not set all variables occurring in the
> other branch to 0. The above example shows a case where Y must be 1 if X
> is 1, although Y occurs in the other branch too.
>
> ZDDs are actually graphs, so in a real implementation of ZDDs, there
> would only be a single node for ( Y -> true ; false ), not two as in the
> case above. However, we need not consider such sharing for now.
>
> Please compare your code with the SICStus reference implementation I posted.
>
> There is also a (very limited) ZDD-based version of library(clpb) available:
>
> https://github.com/triska/clpb/tree/master/zdd
>
> You can use it to inspect the ZDDs of Boolean expressions. For example:
>
> ?- zdd_set_vars([X,Y]),
> sat((X*Y) + (~X* Y)).
>
>

> This yields the ZDD mentioned above, /with/ sharing of isomorphic subgraphs:

>
> node(4)-(X->node(3);node(3)),
> node(3)-(Y->true;false),
>
>
> All the best,
> Markus
>

[Kuniaki Mukai]

Hi Markus,

I have downloaded an article on Zero-Suppressed BDD (ZDD) by
Shin-ichi Minato via a link in your page. Thanks. My first
impression is that ZDD can be implemented also in a similar
technique that I did on open dicts using only
attribute_unify_hook API of SWI-Prolog, keeping the
commutativity of the ordinal unification.

A reason follows. ZDD provides set operations including
union, intersection, and difference. Since boolean unificaion x=y
is equivalent x=y=1 or x=y=0, then we can compute the
solutions for x=y as (set(x=1) \cap set(y=1))\cup
(set(x=0)\cap set(y=0)) using the ZDD set operations.

I was careful to implement open dicts in SWI so that open
dict itself and "region constraints" on them are kept always
as attriutes for not loosing the commutativity of the
standard unification which might happen on manipulating open
dicts on the way of the hook.

I am far from against new API for attributed variables, but
as far as skimming the ZDD paper, I think a sound
implemetation of ZDD on the current API of SWI-Prolog
is also possible as well as my open dicts.

Saying this, I am not sure on that; I may change my mind tomorrow
noticing something. In fact I do not understand yet how to build ZDD.
So please do not take serious my comment, and I am
sorry for possible missing something important.

Kuniaki Mukai

[Jan Burse]

One different criteria for an API, is whether the MGU computation,
directed via attribute variable hooks, should be deterministic or
non-deterministic.

I think attribute variables, such as in ECLiPSe allow non-determinism,
in Jekejeke Prolog this is also possible, but it only came 2 years
later after the intial version of attribute variable hooks.

You might defer non-determinism, until the attribute variable is
further instantiated, and a deterministic result is available. But
this lowers early pruning.

Non-determinism is sometimes observed in Hi-Ord unfication,
but it is also described here for freature terms:

Logical Foundations of Object-Oriented and Frame-Based Languages,
Michael Kifer, Georg Lausen and James Wu, 1995
http://www.cs.sunysb.edu/~kifer/TechReports/flogic.pdf
(See for example C Appendix: A Unification Algorithm for F-Molecules)

Here is a non-deterministic example:

   Welcome to SWI-Prolog (threaded, 64 bits, version 7.5.13)
   SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.

   ?- freeze(X, (X=f(a,_); X=f(_,b))).
   freeze(X,  (X=f(a, _5992);X=f(_6002, b))).

   ?- freeze(X, (X=f(a,_); X=f(_,b))), X=f(A,B).
   X = f(a, B),
   A = a ;
   X = f(A, b),
   B = b.

And the same in Jekejeke Prolog (requires Jekejeke Minlog):

   Jekejeke Prolog 2, Runtime Library 1.2.3
   (c) 1985-2017, XLOG Technologies GmbH, Switzerland

   ?- use_module(library(term/suspend)).
   % 5 consults and 0 unloads in 62 ms.
   Yes

   ?- freeze(X, (X=f(a,_); X=f(_,b))).
    freeze(X, (X = f(a,_B); X = f(_C,b)))

   ?- freeze(X, (X=f(a,_); X=f(_,b))), X=f(A,B).
   X = f(a,B),
   A = a ;
   X = f(A,b),
   B = b

The API for non-deterministic attribute variable hooks in Jekejeke
Prolog consist of injecting a goal between the head and the body
of the currently executed clause:

sys_assume_cont(G):

The predicate temporarily pushes the goal G on the continuation queue.

http://www.jekejeke.ch/idatab/doclet/prod/en/docs/15_min/10_docu/02_reference/07_theory/01_minimal/01_assume.html

I don't know the SWI-Prolog API for that. The above API can
be used inside a deterministic attribute variable hook, to cause
some non-deterministic behaviour later on.

[Jan Burse]

For example this SWI-Prolog API cannot push non-deterministically
goals of the continuation stack:

attr_unify_hook(+AttValue, +VarValue)
http://www.swi-prolog.org/pldoc/doc_for?object=attr_unify_hook/2

On the other hand this SICStus Prolog API explicity is able to do
it, it has even a goals output parameter:

Module:verify_attributes(-Var, +Value, -Goals)
https://sicstus.sics.se/sicstus/docs/3.7.1/html/sicstus_17.html

The SICStus documentation also says so:
"It may succeed non-deterministically, in which case
the unification might backtrack to give another answer."

[Jan Burse]

Oops, although it doesn't push anything, it might still be able to
result in non-deterministic behaviour. I am not 100% sure.

Here Ciao shows how to implement freeze via attr_unify_hook:
"In the following example we give an implementation of freeze/2. We name
it myfreeze/2 in order to avoid a name clash with the built-in predicate of the same name."
https://ciao-lang.org/docs/ciao/attr_doc.html

It does something along:

attr_unify_hook(_) :-
    ...
    call(Fa) 
    ...

But Markus Trisa writes:
"The way in which this hook currently works makes the implementation of 
important classes of constraint solvers impossible or at least extremely 
impractical. For increased generality and convenience, simultaneous 
unifications as in [X,Y]=[0,1] should be processed 
sequentially by the Prolog engine, or a more general hook should be 
provided in the future."

I am not sure whether SICStus Prolog solves the problem.
SICStus Prolog writes:

"This predicate is called whenever a variable Var that might have
attributes in Module is about to be bound to Value (it might
have none). The unification resumes after the call to
verify_attributes/3."

So although the hook is synchronous to the unification,
i.e. step by step. I am not sure what happens to the
goals. The specification only says:

"It is expected to return, in Goals, a list of goals 
to be called after Var has been bound to Value.

What is the meaning of after here? How much after? Are
we really save for what Markus Triska thinks a problem.
A possible workaround for Markus Triskas problem would

be to store the ZDD with different variables, and have
a map that shows which variables correspond to the
variables in the ZDD.

The in the SWI-Prolog hook, he could work step-by-step
through this map, although the map would have received
a "simultaneous" or better "multiple variable" instantiation.

Just some guesses what could be done...

[Kuniaki Mukai]

Hi Markus,

An additional comment to my previous post is here.

Assuming a special syntax of boole constant
e.g. '$boole'(true), '$boole'(false),
a 'parallel unification'

[X,X] =[Y,'$boole'(true)]

must be expanded to

[X, X] = [Y, B]

beforehand where B is a fresh varible with the
'$boole'(true) as an attribute. This is the way
I use in my experimetal open dicts using
only attr_unify_hook, for not going into possible
troubles on "parallel unificatin".

However this requires preprocessing by term_expansition
for every clause and query. In fact,
'$boole'(true) may appear even a head of a clause.
I agree that such a preprocessing may be unacceptable for
the constraint designer and developer.

> Kuniaki Mukai

[Jan Wielemaker]

Hi Markus,

Thanks. I have updated

https://swish.swi-prolog.org/p/Minato%20task.swinb

This actually starts looking like a principled way to deal with at least
a subclass of the cases for which you claim the SICStus interface is
required. The trick is that, if you have a structure where you need to
reason about the state of variables prior to unification you create a
copy of this structure (using copy_term/2) and then you merge the copy
with the original. In other words, you have

( X -> true ; ( Y -> true ; false ) )-[X,Y]

And I turn this into the term below:

z(X,Xc,true,z(Y,Yc,true,false))-[X-Xc,Y-Yc]

Now, we associate this structure using attvars to only the original
variables. When our hook is called, some part of the original variables
are bound, but our copies are all free and we can inspect them and
control when we bind them. We could also put shadow attributes on them,
but that is not needed for this case.

In our case, we restrict the ZDD using all known variables as below.
Note that we bind the shadow variables as we go along.

zdd_restriction(b(T), b(T)).
zdd_restriction(z(AV, V, Then0, Else0), ZDD) :-
( AV == 0
-> V = 0,
zdd_restriction(Else0, ZDD)
; AV == 1
-> V = 1,
zdd_restriction(Then0, ZDD)
; var(AV)
-> zdd_restriction(Then0, Then),
zdd_restriction(Else0, Else),
ZDD = z(AV, V, Then, Else)
; type_error(boolean, AV)
).

Now our final zero-binding becomes as below. The var(V) condition
tells me that the corresponding variable was not on the path to true
and must thus be 0. If V is nonvar, the value was on the true path
and thus already instantiated to an admissible value.

all_others_0([]).
all_others_0([AV-V|Vs]) :-
( var(V)
-> AV = 0
; true
),
all_others_0(Vs).

There is of course a lot to optimize. I do claim that I found a clean
solution for the ZDD problem that is not significantly different from
yours. I think this also implies that optimizations you can think of for
your implementation can be transferred to this one. There is a little
more work establishing the constraint, but the programming work is
straight forward (copy_term/2 and merge the structures). The runtime of
user code should be very compariable, while the runtime overhead in the
system is lower. Comparing space we use a little more in user space (the
variable copy) while we save on the system administration.

Cheers --- Jan

On 09/01/2017 05:40 PM, Markus Triska wrote:

> Hi Jan,
>
> thank you for taking a look, and for providing this environment!
>
> A variable may occur on both sides of a ZDD. For example, the formula
> X*Y + ~X*Y corresponds to the ZDD:
>
> ( X -> ( Y -> true ; false) ; ( Y -> true ; false ) )
>
>
> Therefore, we generally must not set all variables occurring in the
> other branch to 0. The above example shows a case where Y must be 1 if X
> is 1, although Y occurs in the other branch too.
>
> ZDDs are actually graphs, so in a real implementation of ZDDs, there
> would only be a single node for ( Y -> true ; false ), not two as in the
> case above. However, we need not consider such sharing for now.
>
> Please compare your code with the SICStus reference implementation I posted.
>
> There is also a (very limited) ZDD-based version of library(clpb) available:
>
> https://github.com/triska/clpb/tree/master/zdd
>
> You can use it to inspect the ZDDs of Boolean expressions. For example:
>
> ?- zdd_set_vars([X,Y]),
> sat((X*Y) + (~X* Y)).
>
>

> This yields the ZDD mentioned above, /with/ sharing of isomorphic subgraphs:

>
> node(4)-(X->node(3);node(3)),
> node(3)-(Y->true;false),
>
>
> All the best,
> Markus
>

[Jan Wielemaker]

Markus,

In your tradition, I can imagine you have code lying around that
generates ZDDs and both satisfying and non-satisfying sets of bindings
for their variables. Or, maybe even a complete testing suite, including
cases to test performance. If so, could you share that code? That would
allow creating a really nice, fast and robust zdd library.

Thanks --- Jan

[Markus Triska]

Hi Jan,

thank you! I would like to address a few points that I think are increasingly relevant to this discussion:

First, it is not my claim that the SICStus interface is necessary to solve this. It is not even my claim that this task cannot be solved with the SWI interface. In fact, both in the document and in the original Github issue from two years ago I mention that one can solve the task with SWI-Prolog by duplicating information, exactly as you are now doing in your solution. In my own implementation of ZDDs, I am using integer IDs for variables, which amounts to roughly the same approach (although I consider working on concrete integers less error-prone than on potentially aliased logical variables).

There are at least two major downsides to this approach though:

First, the primary bottleneck when reasoning over ZDDs is memory: ZDDs grow exponentially for some tasks, and I have several examples that take 10 GB of RAM and more. In my own implementation of ZDDs, each node takes 48 bytes of RAM. Adding a further cell to each node therefore amounts to an overhead of more than 15% of memory, and therefore prevents the solution of some tasks that can otherwise be (narrowly) solved with ZDDs on the machines I am using, some of which have 40 GB of RAM and more.

For this reason, solutions that duplicate information in each node are highly undesirable for this task in particular, even if they work from a theoretic perspective.

The second downside is the potential for further mistakes in libraries: The more redundancy and connections among variables all library authors have to keep track of in the implementation of their constraint solvers to make them work correctly, the higher the risk for implementation mistakes. For this reason, I consider it undesirable to work on copies of data instead of the involved variables themselves. The essence of the "redundancy" approach is to implement for ourselves the mechanism that we actually expect the Prolog engine to perform for us. This is a bit like the issue that Samer raised in connection with the delimited continuations interface: Is it desirable to impose the burden of such issues, over and over, on library authors instead of handling it once and for all, cleanly, in the engine?

These issues, to me, were sufficient to hinge further developments of ZDD-based solvers on less error-prone and more general interfaces that in addition also require less memory, which is always tight in this case to begin with.

For comparison, I point towards the SICStus interface as one of many possible approaches to solve this issue. Mostly because it is already available and able to solve the task in a way that I consider convenient and straight-forward, in addition to retaining the famously excellent performance characteristics of SICStus. Emulating the SICStus interface would have the added benefit that, in addition to its obvious generality, it would render the SWI interface for attributed variables compatible with SICStus and other systems that implement it, such as Ciao, YAP and others that may do so in the future, and hence simplify ports of important applications to SWI-Prolog which currently depend on SICStus. I am thinking especially about GUPU, cTI and others.

However, there are clearly other approaches to solve this concrete issue satisfactorily too. For example, you could decide to split unifications if attributed variables are involved: A unification such as [X,Y] = [1,1] could be handled internally as the conjunction (X = 1, Y = 1), and therefore trigger the hook for X when Y is not yet instantiated. This is only one possible solution that would also solve this, though it does not come with the other benefits I mentioned.

All the best,

Markus

> <mailto:swi-prolog+unsub...@googlegroups.com>.

[Jan Burse]

The copy is not really a duplication. You get a new skeleton, with different
variables in it. But the old skeleton is not anymore needed.

So the additional cost in memory is only O(n) number of variables. I am
referning to Jan W. solution of my mapping idea.

P.S.: Otherwise dont expect too much, it is still NP≠P.

[Jan Burse]

Nope, I see, Jan W is blowing up the structure a little bit. So its
not O(n) (and not my idea), its kind of duplicating the
storage consumption:

Jan W wrote:
>   ( X -> true ; ( Y -> true ; false ) )-[X,Y]
>
> And I turn this into the term below:
>
>   z(X,Xc,true,z(Y,Yc,true,false))-[X-Xc,Y-Yc]

Why not?

    z(Xc,true,z(Yc,true,false))-[X-Xc,Y-Yc]

And use some (@<)/2 in zdd_restriction to make
it faster. Is there no variable ordering in ZDD?

[Kuniaki Mukai]

Hi Jan and Markus,

It is good to observe that you are approaching together to a final solution.
Although it is hard enough for me to follow discussions, I would like
to leave a memo here on a naive API proposal, and on what I understand
about ZDD from the Minata's paper, though I haven’t read it through.

I think the following API is enough for SWI as API on ZDD.

My proposal on API to SWI

zdd_boole(X, 0) : put_attr(X, zdd, 0)
zdd_boole(X, 1) : put_attr(X, zdd, 1)


This proposal comes from what I understand
on ZDD constraint process below. I believe Markus and Jan
are working together on ZDD constraint, and I hope
it is clear that my simple proposal is derived from
this process model.

Let V be a set of variables. An (boolean) assignment is
a function f : V -> {0,1} on V. Let A(V) be
the set of assigments on V.

For x,y in V, the following three are commands
x=0, x=1, x=y.

For a subset D of A(V), define actions of a command on D

D[x = 0] := { f in D | f(x) =0 }
D[x = 1] := { f in D | f(x) =1 }
D[x = y] := { f in D | f(x) = f(y) }

Note that all three actions are provided in Minato’s ZDD theory .

For a subset ZDD of A(V), a ZDD process is a sequence
consisting of subsets Di of A(V), and commands ci:

c1 c2 cn
D0 -> D1 -> ... -> Dn

with D0 = ZDD, such that

Di = D(i-1)[ci] (i = 1,...n ).

I hope we share this process model as a bottom line,
and Markus and Jan are discussing at some high level
of implementation issue above this bottom line.

I have learned from Markus that ZDD is an efficient and beautiful (Knuth)
data structure for sets of possible boolean assignments,
which, I believe, is important information for us all.

Kuniaki Mukai

> > <mailto:swi-prolog+...@googlegroups.com>.

> > Visit this group at https://groups.google.com/group/swi-prolog.
> > For more options, visit https://groups.google.com/d/optout.
>
>

> --
> You received this message because you are subscribed to the Google Groups "SWI-Prolog" group.

> To unsubscribe from this group and stop receiving emails from it, send an email to swi-prolog+...@googlegroups.com.