Skip to first unread message

Aug 31, 2017, 11:08:05 AM8/31/17

to SWI-Prolog

Hi all,

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

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:

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

Sep 1, 2017, 1:41:54 AM9/1/17

to Markus Triska, SWI-Prolog

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.

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.

Sep 1, 2017, 3:20:14 AM9/1/17

to Markus Triska, SWI-Prolog

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

> Hi all,

>

> I have uploaded an introduction to *Attributed Variables*:
> Hi all,

>

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.

>

> 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

>

>

>

> 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>.
> 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

Sep 1, 2017, 6:58:20 AM9/1/17

to Markus Triska, SWI-Prolog, Jan Wielemaker

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.

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

Sep 1, 2017, 11:06:45 AM9/1/17

to Kuniaki Mukai, Markus Triska, SWI-Prolog

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

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

Sep 1, 2017, 11:14:07 AM9/1/17

to SWI-Prolog, tri...@logic.at, J.Wiel...@vu.nl

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:

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.

Sep 1, 2017, 11:40:36 AM9/1/17

to SWI-Prolog, kuniak...@gmail.com, tri...@logic.at

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:

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

Sep 1, 2017, 11:54:30 AM9/1/17

to Markus Triska, SWI-Prolog, J.Wiel...@vu.nl

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

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

Sep 1, 2017, 12:28:33 PM9/1/17

to SWI-Prolog, tri...@logic.at, J.Wiel...@vu.nl

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:

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

Sep 1, 2017, 12:34:00 PM9/1/17

to Jan Wielemaker, Markus Triska, SWI-Prolog

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

Sep 1, 2017, 12:51:10 PM9/1/17

to SWI-Prolog, J.Wiel...@vu.nl, tri...@logic.at

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

Sep 1, 2017, 12:53:52 PM9/1/17

to Markus Triska, SWI-Prolog, Jan Wielemaker

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

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

Sep 1, 2017, 2:03:35 PM9/1/17

to Kuniaki Mukai, Markus Triska, SWI-Prolog, Jan Wielemaker

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

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.

Sep 2, 2017, 3:47:27 AM9/2/17

to SWI-Prolog, tri...@logic.at, J.Wiel...@vu.nl

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

Sep 2, 2017, 4:33:08 AM9/2/17

to Markus Triska, SWI-Prolog, J.Wiel...@vu.nl

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

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

Sep 2, 2017, 7:07:29 AM9/2/17

to Markus Triska, SWI-Prolog, kuniak...@gmail.com

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
> Hi Jan,

>

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

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)).

>

>

>

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

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

>

>

> All the best,

> Markus

>

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

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

>

>

> All the best,

> Markus

>

Sep 2, 2017, 9:55:36 AM9/2/17

to Markus Triska, SWI-Prolog, J.Wiel...@vu.nl

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

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

Sep 2, 2017, 11:11:03 AM9/2/17

to SWI-Prolog

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:

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.

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.

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.

Sep 2, 2017, 11:20:04 AM9/2/17

to SWI-Prolog

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:

the unification might backtrack to give another answer."

goals of the continuation stack:

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."

Sep 2, 2017, 11:37:00 AM9/2/17

to SWI-Prolog

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:

result in non-deterministic behaviour. I am not 100% sure.

Here Ciao shows how to implement freeze via

it

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 variableVarthat might have attributes inModuleis about to be bound toValue(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, inGoals, a list of goals

to be calledafterVarhas been bound toValue.`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...

Sep 2, 2017, 11:38:25 PM9/2/17

to Markus Triska, SWI-Prolog, J.Wiel...@vu.nl

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

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.

Sep 3, 2017, 5:14:06 AM9/3/17

to Markus Triska, SWI-Prolog, kuniak...@gmail.com

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:

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

> 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)).

>

>

>

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

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

>

>

> All the best,

> Markus

>

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

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

>

>

> All the best,

> Markus

>

Sep 3, 2017, 6:09:21 AM9/3/17

to Markus Triska, SWI-Prolog, kuniak...@gmail.com

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

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

Sep 3, 2017, 7:36:52 AM9/3/17

to SWI-Prolog, tri...@logic.at, kuniak...@gmail.com

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>.

Sep 3, 2017, 7:42:26 AM9/3/17

to SWI-Prolog

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.

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.

Sep 3, 2017, 7:50:28 AM9/3/17

to SWI-Prolog

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:

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?

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?

Sep 3, 2017, 8:48:14 AM9/3/17

to Markus Triska, Jan Wielemaker, SWI-Prolog

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>.

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

> > Visit this group at https://groups.google.com/group/swi-prolog.

> > For more options, visit https://groups.google.com/d/optout.

>

>

> > 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.
> You received this message because you are subscribed to the Google Groups "SWI-Prolog" group.

Sep 3, 2017, 11:28:40 AM9/3/17