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.

[Jan Burse]

Your API somehow answers the wrong question, nevertheless
it can be used to illutstrate the problem of Markus Triska.
Your API is a call-in API, where user land would call a ZDD
data structure. But the problem is a call-out API, where

the Prolog (attribute-)system would call user land. call-out
API are recognizable that they are often marked "hook"
(although the name is not always used consistently for
call-out). The current "hook" is:

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

The problem is that when this hook gets call, since it gets
called after the instantiation, for a command X=1, that the
variable name is totally lost. Assume you use only zdd as
the attribute, you will only see:

   zdd   1

Because the variable is missing, you will not be able
to know what to do with the ZDD data structure. So what
is needed, what could be another way out of the troubles,
is to have attributes that are not only atoms,

but really carry more information, in that they are terms.
I dont know whats the SWI-Prolog definition, but the
Ciao Prolog definition of attribute is:

"It provides a way to associate to variables one or several
arbitrary terms called attributes."
https://ciao-lang.org/docs/ciao/attr_doc.html

So an attribute can be a compound. A simple idea would
be associate a ZDD variable index to a ZDD variable.
Lets assume we have this ZDD constraint:

    /* xor function */
    (X -> (Y -> 0;1); (Y -> 1;0))

Then we can encode the ZDD tree as follows
somewhere once:

   '#1' : ('$1' -> ('$2' -> 0;1); ('$2' -> 1;0))

And the variables get the following attributes:

    X : zdd('#1', '$1')

    Y : zdd('#1', '$2')

Now its easy to reduce the ZDD trees by the standard
SWI-Prolog "hooks", and its not that we use extra space.
   
Bye

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

[Kuniaki Mukai]

ZDD must have information of the list of variables, (V in my post).
which might be represented as a vector. What is needed for builtin action of ZDD
(in my note) is the current state of unification over V ("equivalence relation”
on V). Isn’t it ? So, I don’t see your point.

Kuniaki Mukai

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

[Jan Burse]

If you analyze the freeze Ciao example, you see also that
it uses "attributes" which are compounds.

In particular they don't wrap a lot what they put as
attribute, they put the freezed goal itself as attribute,
but somehow their system must use '$:'(A) compounds
for this purpose.
https://ciao-lang.org/docs/ciao/attr_doc.html

So their attribute is of the form '$:'(_), this is seen
when they replace an attribute value, in case subsequent
freeze invokations push more and more goals:

     ...

           ; get_attr_local(X, Fb) ->

	    meta_conj(Fb, Goal, C),
	    put_attr_local(X, C)   % rescue conjunction
     ...

% A (meta) conjunction of two goals
meta_conj('$:'(Fa), '$:'(Fb), '$:'('basiccontrol:,'(Fa, Fb))).

For ZDD variables, if they are allowed to occur in multiple
ZDD trees, you would need the same. So basically the best
for a ZDD attribute could be a list wrapped inside a zdd functor:

         X : zdd(['#1'-'$1', '#3'-'$2'])

The above would mean X occurs in ZDD tree '#1' as '$1' and
X occurs in ZDD tree '#3' as '$2'. This is the current state
of attributes I guess, that their outer functor is

the key of the attribute. So you can have multiple attributes,
but for a single key, the attribute is single value. In Jekejeke Prolog
I did approach the problem differently, and an attribute variable

can actually carry multiple attributes with the same outer functor.
The difference is seen here:

SWI-Prolog: Attributes are single valued per outer functor:

Welcome to SWI-Prolog (threaded, 64 bits, version 7.5.8)

SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.

?- freeze(X, write(foo)), freeze(X, write(bar)), get_attrs(X, A).

A = att(freeze, '$and'(user:write(foo), user:write(bar)), []),

Jekejeke Prolog: Attributes can be multi valued:

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

  ?- use_module(library(term/suspend)).

  ?- use_module(library(experiment/attr)).

  ?- use_module(library(experiment/trail)).

  ?- freeze(X, write(foo)), freeze(X, write(bar)),
     sys_clause_hook(X, sys_hook_freeze(A), _), sys_melt_var(A, sys_data_freeze(B)).
  B = write(foo) ;
  B = write(bar)

[Jan Burse]

The problem is before you change an API or create a new
API for some Prolog system, here attr_unify_hook/2

you must somehow demonstrate that it is not suitable
for your problem, and that there is really an issue.

The API attr_unify_hook/2 is quite an old and robust API.
You can also implement vanilla interpreters for it,

that is how everything started I guess, see for example:
Maybe its this paper here:

[Hol92] C. Holzbaur.

Metastructures vs. Attributed Variables in the Context of Extensible Unification.
In 1992 International Symposium on Programming Language Implementation and Logic Programming, pages 260--268. LNCS 631, Springer Verlag, August 1992.

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

[Jan Burse]

Here is a link to the paper:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.3893&rank=1

That paper basically tells a lot of the genesis of the
alternative API, not the SWI API attr_unify_hook/2
but the SICStus API _verify.

[Jan Burse]

Recall what the two APIs at stake are:
https://groups.google.com/d/msg/swi-prolog/PlHdBTX_I7I/61g3evo6FAAJ

[Kuniaki Mukai]

The proposed API is only to tell the unification state
to ZDD. It is too much to say it is a new API proposal.
I do not insist at all on this. What I want to know is
what is the real problem. Performance ?
I hope they make it clear without details of codes if possible.

Kuniaki Mukai

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

[Jan Burse]

Recall what the two APIs at stake are:
https://groups.google.com/d/msg/swi-prolog/PlHdBTX_I7I/61g3evo6FAAJ

There are very low chances that a special ZDD API
will be introduced. Especially a user land call-in API.

What is investigated is a call-out API, from the
Prolog attribute system to user land.

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

[Jan Burse]

In the SWI-Prolog API, for ZDD you would need:

     X : zdd(['#1'-'$1', '#3'-'$2'])

In the SICStus Prolog API, for ZDD you could go with:

     X : zdd(['#1', '#3'])

The later would work, if you can find your trees
somewhere, in SICStus Prolog, and if they
keep the original variables.

SICStus Prolog API could offer this, since the variable
is not instantiated during the call of the
API hook (its a pre-unify hook).

SWI Prolog API cannot offer this, since the variable
is already instantiated during the call of the
API hook (its a post-unify hook).

[Jan Burse]

Of course there are much more problems.
Take this decison tree here:

   /* xor function */
    (X -> (Y -> 0;1); (Y -> 1;0))

You agree this is XOR?
Now take on the other hand this one:

   /* not xor function */
    (X -> (Y -> 1;0); (Y -> 0;1))

You agree this is EQU?
So a decend solver, when we tell him:

    valid((X -> (Y -> 1;0); (Y -> 0;1)))

He should maybe come up with the answer:

    X = Y

Maybe Knuth was over reacting...

[Kuniaki Mukai]

Having a related question to Jan Burse’s on ZDD in his previous
post, I had asked Markus in this thread not so long time ago.
His answer in this thread not so long time ago was so clear
that I came to a conclusion in my mind that the ZDD theory
is a kind of algebra over sets, just like that so is
regular expressions over strings.

Thus ZDD looked like a domain constraint, such as
over intervals. So far I have’t hear any issues about the current SWI API
with respect to such good natured constraint suits. Even after skimming
the Minato’s paper, I got no information against my
interpretation, but only strengthen it.

To be honest, I am a little bit confused with recent Jan Wielemaker’s
reaction towards the API extension, because I had posted
a “proof” named "Jan’s lemma” which asserts that the SWI
current simple attr_unify_hook is sound, hoping so also for ZDD.

As I almost completely lack current API issues on attributed variables,
I am always afraid I must be missing something basic.

Kuniaki Mukai

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

[Jan Wielemaker]

On 09/03/2017 01:36 PM, Markus Triska wrote:
> 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).

As you have full control of these shadow variables and they are only
stashed away inside attributes the user is not supposed to inspect, I
see no problem. Variables have the advantage that the algorithm barely
changes.

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

You count 15%. That is already pretty little in a task that grows
exponentially. Yes, it does mean there are problems you can solve
without spending this overhead, but on pure statistical reasoning these
should be really few. That is the nice thing about exponential blowup:
the capacity doesn't matter that much. There are only problems to a
certain size you can tackle and getting even 10 times the resources
lifts this limit only a little. So, 15% less resources doesn't matter
too much.

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

As we have seen with Douglas' attempt, the verify_atributes/3 interface
was not only after all pretty hard to define correctly, but it was also
considerably slower. This may not be that big a problem for some
constraint problems, but it is for others, notably those that involve
simple constraints such as freeze/2, dif/2 or when/2. There are many
constraints that are obviously just as easily solved using the
hProlog/SWI-Prolog interface than using the SICStus interface.

If there is an important class of problems that cannot be solved, you
have a point. You wrote an article about the history of the attvar
interfaces, blaming Bart to have blocked progress by proposing an
interface that is way simpler than its predecessors but seriously
limited (your claim). You add a challenge, so I think "ok, now we
finally get to the bottom". I show you that this can be solved cleanly.
Costed one iteration to really get the problem clear, a day thinking
about it while doing other stuff and an hour writing it all up. The
result permits practically the same algorithm as the original, performs
equally and costs only 15% (your claim, also about my estimate) more
memory.

I'm not impressed and I think Bart is right: a simpler interface that
can solve most simple problems with less effort and better performance
and can solve the hard ones with only a little more thought is an
improvement in my view.

[Samer's comments on delimited continuations let to a change of the
interface that make the native interface more general. Samer wants a
layer on top of that, which can now perfectly well be supported in
Prolog. I think that is the good way: a low level interface that can be
used directly or can be used as the basis for a higher level interface.
That way of layering does not work for attributed variables. The SICStus
one can emulate the SWI-Prolog one and is in that sense more `low level'
but it requires more and complicated machinery and is slower by design.]

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

As it stands, it seems to work the other way around and libraries such
as CHR, clp(q,r) and your clp(fd) got their portability from the fact
that Bart's interface is so easy to support on any system. A simple
interface that is easily implemented in any system, can do simple things
easily and fast and hard things with a little more work is normally
considered the sweat spot in computer science. I recall from our
nightmare with verify_attributes/3 that test cases failed and we
couldn't get our heads around what was broken were. In any case
pre-unification comes with a price:

- You have to trail more to be able to properly undo the bindings
- Prior to calling the hooks you must examine the trail, undo
specific bindings and translate the stored assignment data to
prepare for calling verify_attributes/3. This all proved a
pretty delicate process, probably the thing Douglas and I never
got right.
- verify_attributes/3 creates a list of goals. Each element of
this list must be meta-called which is always slower and less
tracktable (code analysis) than direct calling.

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

I don't think that is feasible. If you unify two terms about which you
do not know anything you never know how many bindings it will create. In
general you want to do as many unifications as possible before calling
attribute hooks as a failing unification saves a lot of work. That is
why SWI-Prolog checks attvar unification wakeups after unifying the
entire head (and after completion of foreign predicates). As this is
also the point where normal body code execution starts we can cheaply
push the wakeup call.

I fear the result is that we disagree. Unless someone comes up with a
real use case that clearly demonstrates why pre-unification hooks are
needed I think it is also time to let it rest.

Cheers --- Jan

> > an email to swi-prolog+...@googlegroups.com <javascript:>
> > <mailto:swi-prolog+...@googlegroups.com <javascript:>>.

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

> <https://groups.google.com/group/swi-prolog>.

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

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

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

[Jan Burse]

Hi,

Did you read by any chance the intial post by Markus Triska? I doubt
that you can simple do some lemmas and hand waving, the proof
is in the pudding. Show us an implementation of ZDD via the current
SWI-Prolog API, and we are done.

The orignal post by Markus Triska is:
https://www.metalevel.at/prolog/attributedvariables#minatotask

It contains an implementation of ZDD, via the SICStus Prolog
API, if you scroll down you find it here in the Markus Triska post:
- As a warm-up, let us express the so-called restriction of a ZDD...
- In SICStus Prolog, we use library(atts) to declare and reason about attributes...
The full code is here: https://www.metalevel.at/prolog/minatotask.pl

Then in this thread Jan W. posted some fragments for SWI-Prolog,
I don't know whether he has uploaded somewhere a full .pl.

The ZDD problem is very atypical for attribute variables, respectively
we run into the following structure duplcation problem, that might
be the reason that Markus Triska reports horrendous memory usage.
Lets look at Kuniaki Mukai step-by-step characterization:

Kuniaki Mukai  wrote:
> For x,y in V, the following three are commands
>  x=0,  x=1,  x=y.

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

This is a nice model what happens. The D0, D1, ..., Dn states
will be somewhere attached to attribute variables as attributes.
Markus Triska does this in his code minatotask.pl via an
attrribute term zdd_vs. Now lets look at a further property
of attribute terms:

- Attribute Terms are trailed. Lets draw again on the
  Ciao Prolog documentation, which is pretty clear about
  it. Namely we find in the documentation of the freeze
  example I have already cited many times:

; put_attr_local(X, Goal)

https://ciao-lang.org/docs/ciao/attr_doc.html

   So the API there is put_attr_local/2 to change
   an attribute term of a attribute variable. If we
   lookup the docmentation of put_attr_local/2
   we find the trailing described:

         "If Var is a variable or attributed variable, set its
        attribute to Value. If an attribute is already associated
        with Var, the old value is replaced. Backtracking will
        restore the old value (i.e., an attribute is a mutable term.
        See also library mutables). This predicate raises a
        representation error if Var is not a variable and a type
        error if Module is not an atom."

   The trailing appears in that the old value must be kept
    somewhere so that during backtracking it is restored.
    This means for your sequence of D0, D1, ..., Dn states
    by the traditional attribute variables API, these states
    are all kept, also the intermediate states.

Now you can make an easy computation why the memory blows
up. Take for example as D0:

    /* xor */
    D0: (X -> (Y -> 0;1); (Y -> 1;0))

After a command "X=0", we get:

    D1: Y -> 1;0

After a command "X=1"; we get.

    D2: 1

But the traditional Prolog attribute system will not throw away
D0 or D1, its still in the memory, only after a fail things are
rolled back, and will be subject to garbage collection. This is
usually not considered a problem, since

for example in CLP(FD), the model size is not so much
considered a problem, since the model size is dominated
by the variable grounding space. If we have n variables each
over a domain of size m, we have an nxm search,

we will anyway backtrack over the CLP(FD) model, so
usually reclaiming models when deterministic variable
trajectories are chosen, is not really considered. I dunno
whether SWI-Prolog can do, and thats why CLP(FD) is

such a bad idea to use in ordinary programming. Now the
problem is aggravated for ZDD problems, because here
model size can matter, as Markus Triska has posted here.
If you want to participate in a SAT competition with

CLP(FD) Prolog attribute system, and implement on top
of it a SAT solver, based on some clause or decision tree
reduction, you will most likely loose. Especially for those
reduction where a value X=c is forward checked, and

this forward checkin is deterninistic, for those cases
where we know there is only X=c, and not X=c1;X=c2.
There are some tricks to for example in a chain
D0, D1, D2 to garbage collect D1.

Mecury Prolog has such a trailing API, that is connected
to choice points, and can potentially remove intermediate
states that are not really needed. The idea is to somehow
consume/merge events on the trail.

The API is here:
https://www.mercurylang.org/information/doc-latest/mercury_ref/Avoiding-redundant-trailing.html#Avoiding-redundant-trailing

I have not yet implemented such trailing in Jekejeke Prolog,
but it would be surely benefitial for the szenario I have
just sketched here in this thread,namely forward checking
X=c, where we know we don't have X=c1;X=c2.

Have a Nice day!

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

[Jan Burse]

Jan W. wrote:
>  - You have to trail more to be able to properly undo the bindings

Thats the unfication variable binding trail.
But there will be also a attribute term change trail.

[Jan Burse]

The former trail is usually GC-ed, the later trail can be also GC-ed,
but its a little harder. The problem is somehow ortogonal to the API,

I don't see a strong dependence on which variable "hook" API
(SWI or SICStus)  is used, but I see some relevance to ZDD.

> For more options, visit <a href="https://groups.google.com/d/optout" rel="nofollow" target="_blank" onmousedown="this.href='https://groups.

[Jan Wielemaker]

On 09/04/2017 11:58 AM, Jan Burse wrote:
>
> Then in this thread Jan W. posted some fragments for SWI-Prolog,
> I don't know whether he has uploaded somewhere a full .pl.

There is a link to a SWISH notebook in my post. That contains all
code and you can run it as well.

> The ZDD problem is very atypical for attribute variables, respectively
> we run into the following structure duplcation problem, that might
> be the reason that Markus Triska reports horrendous memory usage.

There is only one extra variable per non-terminal node. The list of
variables to be zeroed changes to a list of pairs. We can pretty easily
omit the entire list though. Why not just walk the ZDD itself? It is
just a little more work.

I'm sure you can optimize the whole thing a lot (as Markus also hints).
I doubt you really need the `shadow variables' to implement ZDDs. What I
wanted to show is that you can do an almost systematic transformation to
a problem where pre-unification seems necessary to make it work with
post-unification.

Cheers --- Jan

[Jan Burse]

When I wrote:
> The ZDD problem is very atypical for attribute variables, respectively
> we run into the following structure duplcation problem, that might
> be the reason that Markus Triska reports horrendous memory usage.

I didn't mean your, Jan W. realization, I was refering to both
Markus Triskas and Jan W. code in respect to ATTR TRAILING,

I doubt that Markus Triskas code runs well even in SICStus Prolog,
unless SICStus Prolog has good trailing GC of attribute term

changes. In the same way that some lemmas are handwaving,
the claim that in SICStus Prolog everthing is fine is also

handwaving. What are the tests and the results exactly?

[Jan Wielemaker]

On 09/04/2017 12:13 PM, Jan Burse wrote:
> The former trail is usually GC-ed, the later trail can be also GC-ed,
> but its a little harder. The problem is somehow ortogonal to the API,
>
> I don't see a strong dependence on which variable "hook" API
> (SWI or SICStus) is used, but I see some relevance to ZDD.
>
> Am Montag, 4. September 2017 12:06:53 UTC+2 schrieb Jan Burse:
>
> Jan W. wrote:
> > - You have to trail more to be able to properly undo the bindings
>
> Thats the unfication variable binding trail.
> But there will be also a attribute term change trail.

SWI-Prolog has only one trail stack. I thought that was normal ... It
has two types of cells. The one simply points at a location and undoing
simply resets that location to a variable. The other is a tagged pointer
to the same location and below the cell is a cell with the value. So we
have (where PTR* is the tagged pointer):

PTR
PTR*
VALUE

As I recall (might be wrong here), preparing the verify_attributes/3
call requires processing the trail stack where we need to make
assumptions on the precise order where things are trailed. GC indeed may
complicate things as it may remove some of these trail entries.

Relying on the trail is not unique. unifiable/3 does something very
similar, as does occurs check validation. From unifiable/3 you can learn
that undoing bindings is not easy. In unifiable/3 we avoid GC calls.
This can be done as the low-level unify() returns true, false or
out-of-stack. The high level one calls the low level one and on
out-of-stack, runs GC and retries. unifiable/3 exploits the same trick.
Head unification however may imply multiple unifications and may run GC
somewhere during the process. If that was only problem we probably could
call the low-level unify and on out-of-stack GC and retry the entire
clause.

Cheers --- Jan

[Jan Wielemaker]

On 09/04/2017 12:26 PM, Jan Burse wrote:
> Markus Triskas and Jan W. code in respect to ATTR TRAILING,

I don't know what is special about attribute trailing. It is simply
destructive assignment trailing that is also used for setarg/3 and
b_setval/2, etc. It needs GC. In partular GC checks for multiple
assignments on the same location between two choice points. If this
happens we must discard all but the last. I assume SICStus has something
similar as without the joy of mutable structures is over very quickly.

Cheers --- Jan

[Jan Burse]

Hi,

The GC problem is not the usual GC problem. See Mercury
API. Its not about whether an attribute variable is reacheable or not.
Reachability would be  the usuaö attribute variable GC problem.
Ulrich Neumerkel has paper somehere where he more or less tests:

test :- free(X, true).

Since X is nowhere used, it will never be woken up, and we
can reclaim X including its attribute terms. But here the problem is
thinning the attribute term history. Maybe this one could be
a nice testcase:

- A nice test case could be the "boolean pigeon hole problem".
I have a DPLL solver and a CLP(FD) fomulation for the problem.
Its not yet on GitHub, but its already here:
http://www.jekejeke.ch/idatab/doclet/prod/en/docs/15_min/15_stdy/06_bench/09_programs/07_pigeon/01_pigeon.p.html
http://www.jekejeke.ch/idatab/doclet/prod/en/docs/15_min/15_stdy/06_bench/09_programs/07_pigeon/02_pigeon3.p.html
- The DPLL solver sometimes reduces the problem deterministically
and sometimes non-deterministically. I just see that my DPLL code
doesnt realy capitalize on that, I should rewrite it slightly.
- DPLL implementation could be compared with a ZDD implementation
(I don't have such a one), again more empirical comparison material.
- The history thinning could be maybe also applied to CLP(FD),
this could be a spill over result.

Have a Nice day!

[Jan Burse]

Jan W.:

> I don't know what is special about attribute trailing. It is simply
> destructive assignment trailing that is also used for setarg/3 and
> b_setval/2, etc. It needs GC. In partular GC checks for multiple
> assignments on the same location between two choice points. If this
> happens we must discard all but the last. I assume SICStus has something
> similar as without the joy of mutable structures is over very quickly.

Ok, maybe its just a programming problem. That some choice points
are left somewhere, so that the attribute trailing doesn't work correctly.
Again the proof is in the pudding. Sweating hands.

[Jan Burse]

In DPLL the deterministic forward checking happens in the
unit propagation step. See also here:

function DPLL(Φ)

   ...
   for every unit clause l in Φ
      Φ ← unit-propagate(l, Φ);

   ...
   

https://en.wikipedia.org/wiki/DPLL_algorithm

I just see that my sat/2 predicate, a pure Prolog implementation
in pigeon.p, no use of attribute variable, might have a choice
point too much, not sure.

The pure Prolog implementation is helpful in timing comparisons,
in the pure Prolog implementation we just carry around the
constraint store,

it is helpful, since it will use the normal term/variable GC, so
we can already see a lot, for exampl the NP/P divide of some
SAT problems, very funny...

[Jan Burse]

In a solver setting ZDD might also lead to unit propagation, we have
the same initial cases as in DPLL:

      valid(X -> 1;1)        /* in  ZDD just 1 */       don't care X succeed
      valid(X -> 1;0)                                            X = 1 forward checking
      valid(X -> 0;1)                                            X = 0 forward checking
      valid(X -> 0;0)        /* in ZDD just 0 */        fail

Or build one large ZDD from all the ZDD constraints via ZDD operation
"join", and then check whether ZDD \== 0 (Probably this is what Knuth likes),

the later would be also a way to use ZDD. The dichotomy would be:
- Solution that has somewhere backtracking
- Solution that is fully algebraic

[Jan Burse]

Concerning the joind ZDD, for
- General validity, check ZDD==1
- Satisifiability, check ZDD\==0

[Kuniaki Mukai]

Dear Markus,

Please take time to pursue the current issue yourself. I would not like
to bother you, but my question has taken a more clear form below.
I hope it may be useful for you to know where I have been lost and strayed
in the forest of the API issues:

With symbols as same as in my previous post.

1. ZDD relation: Let E be an equivalence relation on
V \cup {0, 1} such that 0 is not related to 1 in E.
here we call E a ZDD relation.

2. ZDD operations: ZDD theoy provides union', intersection',
diffrence' on ZDD expressions (not on sets but on terms).
(Minato's paper).


3. ZDD operations are set theoretical: for instance,
the extension of intersection' of D1 and D2
is equal to the set theoretical intersecion of
the extension of D1 and that of D2.
(relying on Minato’s theory.)

4. For ZDD relation E and a ZDD expression (term) D,
there is a *symbolic* operation written E*D which
preserves the set theoretical meaning as follows,

|E*D| = {f in |D| | f(x)=(y) for all (x,y) in E },

where |S| denotes the extension of the expression S.


I think such "reduction" E*D of D is possible. In fact
it may be what you have been working with different sets of API.
If I understand so far correctly, then ZDD is a good
natured kind of domain constraints, which is the reason why I don't see
needs of pre-post unification, aside performance or GC issues.

I have to repeat. I may be wrong, and I have no doubt
on your many contributions including ZDD. Rather I hope
I am wrong missing something simple.

Kuniaki Mukai

[Jan Wielemaker]

On 09/04/2017 12:41 PM, Jan Burse wrote:
>
> test :- free(X, true).
>
> Since X is nowhere used, it will never be woken up, and we
> can reclaim X including its attribute terms. But here the problem is
> thinning the attribute term history.

I guess you are hinting at call_residue_vars/2. GC of attributed
variables is nothing special, except call_residue_vars/2 must prevent it
from happening and be able to find orphaned attributed variables. This
was pretty nasty to get right :(

[Jan Burse]

Thank you Kuniaki Mukai, for pointing again to the
Minato, Shin-ichi paper.

My examples marked with ZDD are wrong, they are
actually OBDD. Here is a correction:

     X -> 1;1 == X -> 1;1
     X -> 1;0 == X -> 1;0
     X -> 0;1 == 1
     X -> 0;0 == 0

As can be seen it still holds:

- Satisifiability, check ZDD\==0  /* works */

But the following doesn't work anymore:

- General validity, check ZDD==1 /* doesn't work */

[Markus Triska]

Hi Jan,

it is indeed not my intention to pursue this further. I only want to complement a few of the things you mentioned:

First, you call this a "nice puzzle", then after a day of thinking and working on other stuff, you arrive at the same solution that I already explained in the document itself: Duplicating variables. I do not consider this a clean solution, because it forces users to reify the reasoning that one would reasonably expect to be performed by the underlying engine, assuming they even think about the situation that can occur with this interface at all (which they provably don't). I - now - know that you do consider this a clean solution, which surprises me, though maybe it shouldn't.

Everyone I know who has worked with the interface of SWI has raised the same concerns, with which I agree 100% after having spent more than 10 years working with it and having seen the exact same issues arise in all of the constraint libraries I know, including dif/2, CLP(FD), CLP(B) and the partially correct CLP(Q): The interface of SWI is too error-prone to work with. It makes easy things extremely hard, and forces you to perform acrobatic contortions to implement slightly harder things. That's definitely not what I would call a "sweet spot". I have linked to two serious flaws in constraint libraries to illustrate this (there are also more). Both happened to highly experienced experts in this area. This kind of mistakes could be avoided with the SICStus interface. SICStus is also widely known as one of the fastest Prolog systems available. Take from this what you will.

In any case, if an implementor is reading this and is interested in providing a robust and useful interface predicate for attributed variables, I recommend you emulate that of SICStus. As the long list of issues in constraint libraries illustrates, the SWI interface is unsuitable for library implementors who take correctness seriously.

Thank you and all the best,

Markus

[Jan Wielemaker]

Hi Markus,

On 09/05/2017 08:14 PM, Markus Triska wrote:
> Hi Jan,
>
> it is indeed not my intention to pursue this further. I only want to
> complement a few of the things you mentioned:
>
> First, you call this a "nice puzzle", then after a day of thinking and
> working on other stuff, you arrive at the same solution that I already
> explained in the document itself: Duplicating variables. I do not
> consider this a clean solution, because it forces users to reify the
> reasoning that one would reasonably expect to be performed by the
> underlying engine, assuming they even think about the situation that can
> occur with this interface at all (which they provably don't). I - now -
> know that you do consider this a clean solution, which surprises me,
> though maybe it shouldn't.

You say "One example would be to duplicate all kinds of attributes so
that they are available redundantly in all data structures that occur
anywhere". I merely read that as `you can hack'. There isn't that much
to duplicate, just the attvar needs a shadow variable. If you build the
ZDD with exactly one node per variable it is trivial to add that extra
variable. Also Jan Burse considers ZDDs a "rather atypical case", so
this very modest rewrite seems all fine to me.

You make some more claims in
https://www.metalevel.at/prolog/attributedvariables about code that is
mostly asking for trouble.

m:attr_unify_hook(X, Y) :- throw(cannot_unify(X,Y)).

?- put_attr(X, m, a),
put_attr(Y, m, b),
X = Y.
ERROR: Unhandled exception: cannot_unify(b,_612)

What does this say? `put_attr(X, m, a)` says that X cannot be anything,
but must be, according to the semantics of `m`, compatible with `a`.
Same for `b` in the next call. So, `X=Y` either fails if there is no
value that is compatible with both `a` and `b` or succeeds, creating the
unified say `XY` with a constraint that is the intersection of `a` and
`b` or the single concrete value that is compatible with `a` and `b`.
The unification hook nicely is presented with `a` and a XY with the
attribute `b` (or the other way around, but unification is commutative,
so the hook should have equal semantics).

I do not see what this exception shows. It can access both attribute
values, but just doesn't while one can doubt about the logical purity of
exceptions.

Then summing attributes in a constraint. This just can't be right and
always will give you weird results somehow. Just consider
`copy_term(X,Y), X=Y`. You'd expect this to do nothing in any well
behaved logical theory, but in yours X is associated with double the
value it had before. Sure you can get weird results using that. Just
using setof/3 suffices to get the effect of the above.

So yes, post-unification can only deal with proper _constraints_ on
commutative unification and C = C1 /\ C2, C = v, means the same as C1 =
v, C2 = v. That seems pretty much a basic assuption one should make
about variables exposed to the user anyway. Possibly there are cases
where you have internal data that does not satisfy these rules, but then
you have full internal control and can make all data is properly
accessible and processed in the right order. ZDDs could be considered
an example.

> Everyone I know who has worked with the interface of SWI has raised the
> same concerns, with which I agree 100% after having spent more than 10

Well, not Tom Schrijvers and Leslie de Koninck. Douglas Miles, yes. That
was mostly about misusing attvars though as he didn't even want to do
the unification for one of his use cases, e.g., X=Y -> X == Y; true
would not always be true anymore ... If you really need something for
such non-logical purposes it is surely possible to think of some hack in
C. It has little relation to what attributes are intended to do though.
Kuniaki is not yet complaining either :)

> years working with it and having seen the exact same issues arise in all
> of the constraint libraries I know, including dif/2, CLP(FD), CLP(B) and
> the partially correct CLP(Q): The interface of SWI is too error-prone to

AFAIK, the dif/2 issue had nothing to do with pre-unification. According
to Fred Mesnard SWI-Prolog's clp(Q) seems to be more or less bug
compatible with SICStus, so it doesn't seem the work by Leslie
introduced many bugs. Would be interesting to compare the code. A quick
search in Google Scolar doesn't come up with a publication about the
port.

> work with. It makes easy things extremely hard, and forces you to
> perform acrobatic contortions to implement slightly harder things.
> That's definitely not what I would call a "sweet spot". I have linked to
> two serious flaws in constraint libraries to illustrate this (there are
> also more). Both happened to highly experienced experts in this area.

I probably qualify as `highly experienced', but I make enough mistakes
:) Some could definitely have been avoided by better languages and
interfaces. Most, probably not. A language where it is completely
clear what happens is a pre. That is satisfied.

> This kind of mistakes could be avoided with the SICStus interface.
> SICStus is also widely known as one of the fastest Prolog systems
> available. Take from this what you will.

It probably would be even faster when it adopted the SWI-Prolog attvar
interface as, however you look at it, post-unification hooks simply have
to do less work and have less impact on the rest of the system.

> In any case, if an implementor is reading this and is interested in
> providing a robust and useful interface predicate for attributed
> variables, I recommend you emulate that of SICStus. As the long list of
> issues in constraint libraries illustrates, the SWI interface is
> unsuitable for library implementors who take correctness seriously.

I consider you a highly competent programmer, surely in the top-very-few
Prolog programmers on this planet. That makes me think that somehow you
most likely have a point. Your story doesn't provide me with a backup
for that though. My 0.02$ is still that the post unification approach is
way simpler, faster and solves 95% of the attvar problems quite
naturally while this experience shows that at least a big category of
the other 5% can be solved using a mostly mechanical transformation. And
yes, pre-unification hooks allow you to write things that logically make
no sense, something which is really hard using post-unification as the
unification happened and we can only veto it but we cannot change the
unification.

What I hoped for is that clear use case that cannot be solved this
easily. ZDDs would have been an such a case if it wasn't easily solved.
If that use case doesn't exist we are done. If it does, we are faced
with the question whether post unification hooks can be fixed or they
are really broken by design. I'm far from convinced. So far, past
experience did convince me of the disadvantages of pre-unification.

Cheers --- Jan

> Thank you and all the best,
> Markus
>

[Jan Burse]

I have one problem with your blog post, it seems to me the
most confused I have ever seen.

For example I don't see why this should make any sense:

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

If a ZDD is zero suppressed then the above ZDD is equivalent
to this OBDD, namely:

    OBDD =  ( X -> (Y -> b(false); b(true)) ; (Y -> b(true) ; b(false))),

Which in my optinion can be only satisfied by:

    [X,Y] = [1,0] ;
    [X,Y] = [0,1]

I dont see how you would ever get [X,Y]=[1,1].

Do I miss something?

[Jan Burse]

I think your reception of ZDD is wrong, you start yourself with
"For example, here is a ZDD that represents the truth value of
the Boolean function X xor Y:"

But then things go wrong when you write: "If a variable does not
appear on a path that leads to true, then that variable
must be equal to 0."     /* not correct red. Jan Burse */

Which is not ZDD.

ZDD means:

    a path where X1=1,X2=1,..,Xn=1 leads to 0 can be omitted

You can check yourself there is PDF of the ZDD paper on the
internet. The PDF link is here:
https://eprints.lib.hokudai.ac.jp/dspace/bitstream/2115/16895/1/IJSTTT3-2.pdf

The ZDD compression rule, is explained in Figure 4,
with the title "New reduction rule for ZBDDs", you see
where clearly that the condition is:

     (X -> 0; T)     --> T

This means if X=1 and the terminating node in the BDD is
zero, the we can omit the current node, we do not need to
talk about X=1. This is a kind of Closed World Assumption.

You see the benefit of this rule Fig 5, you can easily add
a new variable when X=1 implies false. Go study Fig 5 and
you will see that my claim is true.

[Jan Burse]

I dont say that this voids your critic of some attribute variable
API, but it lowers a little bit the credibility. You have different
choices. There was recently Norbert Blum

who published a proof about NP≠P, which he needed to
retract, and he did so very gracefully, by "The proof is wrong.
I shall elaborate precisely what the mistake is."

There might be still a confusion somewhere that you have
another interpretation of the "Minato Task", but I was just
looking at your verbalization of ZDD,

and I think its wrong. I had the same problem. I was only
reviewing the definition after Kuniaki Mukai last post,
which somehow suggested to read the f****** paper.

[Jan Burse]

Or do a little algebra first and then a little backtracking.
Like maybe here:

Symmetry-breaking Answer Set Solving - Drescher, Tifrea, Walsh 2010
https://arxiv.org/abs/1008.1809

Am Montag, 4. September 2017 13:02:53 UTC+2 schrieb Jan Burse:

[Jan Burse]

As a test case, the paper also contains the

7.1 Pigeon Hole Problems

[Kuniaki Mukai]

Hi All,

I am a hobbyist of Prolog programming. I have written codes
of predicate zdd/3 to support my observations on ZDD in this thread.
The complete codes is below for those interested people.
The pred/3 sample queries are like this:

1. ?- X=true, Y=false, zdd([X,Y], (X, Y), R).
2. ?- zdd([X,Y], (X;Y), R).
3. ?- zdd([X], (\+ X), R).
4. ?- zdd([X], (\+ X, X), R).
5. ?- zdd([X,Y], (\+ (X;Y)), R).
6. ?- zdd([X,Y], true, R).
7. ?- zdd([X,Y], false, R).
8. ?- zdd([X,Y], (X->Y, Y->X), R), X=true, zdd([X,Y], R, R0).
%@ X = true,
%@ R = (true->Y->true),
%@ R0 = (Y->true).

Query 8 is intended to be a symptom to support that
the current SWI API is enough for ZDD implementation
on attributed variables. No need to pre-post unifications.

Main source of of this codes is no doubt Markus's valuable comment to us
that ZDD is a data structure ( in my case as a prolog codes with
negation as failure builtin (Jan Burse's observation)) to encode the set
of possible assignments as solutions for a given boolean expression.
The efficiency of my codes is no doubt the planet widely bad
because of my ignorance and incompetence of that, even let alone its correctness.

%%%% begin of codes %%%%
:- module(zdd, []).
% ?- module(zdd).

% ?- module(zdd).
% ?- X=true, Y=false, zdd([X,Y], (X, Y), R).
% ?- zdd([X,Y], (X;Y), R).
% ?- zdd([X], (\+ X), R).
% ?- zdd([X], (\+ X, X), R).
% ?- zdd([X,Y], (\+ (X;Y)), R).
% ?- zdd([X,Y], true, R).
% ?- zdd([X,Y], false, R).
% ?- zdd([X,Y], (X->Y, Y->X), R), X=true, zdd([X,Y], R, R0).
%@ X = true,
%@ R = (true->Y->true),
%@ R0 = (Y->true).

zdd(Vars, BooleExp, ZDD):- zdd_slim(Vars, BooleExp, ZDD0),
zdd_slim(ZDD0, ZDD).

%
zdd_slim([], Z, Z0):- zdd_slim(Z, Z0).
zdd_slim([X|Xs], Z, ZDD):- atom(X), !, zdd_slim(Xs, Z, ZDD).
zdd_slim([X|Xs], Z, ZDD):- subst([X-true], (Xs, Z), (Us, Then0)),
subst([X-false], (Xs, Z), (Vs, Else0)),
zdd_slim(Us, Then0, Then),
zdd_slim(Vs, Else0, Else),
Z0 = (X -> Then; Else),
zdd_slim(Z0, ZDD).

%
zdd_slim(X, Y):- zdd_slim_rule(X, X0), !,
zdd_slim(X0, Y).
zdd_slim(X, X).

%
zdd_slim_rule(X, _) :- var(X), !, fail.
zdd_slim_rule((A, B), (A0, B)) :- zdd_slim_rule(A, A0).
zdd_slim_rule((A, B), (A, B0)) :- zdd_slim_rule(B, B0).
zdd_slim_rule((X, A), A) :- X==true.
zdd_slim_rule((A, X), A) :- X==true.
zdd_slim_rule((X, _), false) :- X==false.
zdd_slim_rule((_, X), false) :- X==false.
zdd_slim_rule((A; B), (A0; B)) :- zdd_slim_rule(A, A0).
zdd_slim_rule((A; B), (A; B0)) :- zdd_slim_rule(B, B0).
zdd_slim_rule((X; _), X) :- X==true.
zdd_slim_rule((_; X), X) :- X==true.
zdd_slim_rule((X; A), A) :- X==false.
zdd_slim_rule((A; X), A) :- X==false.
zdd_slim_rule(A -> B, A0->B) :- zdd_slim_rule(A, A0).
zdd_slim_rule(A -> B, A->B0) :- zdd_slim_rule(B, B0).
zdd_slim_rule(X -> _, X) :- X==false.
zdd_slim_rule(_ -> X, X) :- X==false.
zdd_slim_rule(X -> A, A) :- X==true.
zdd_slim_rule(\+(A), \+(A0)) :- zdd_slim_rule(A, A0).
zdd_slim_rule(\+(X), true) :- X==false.
zdd_slim_rule(\+(X), false) :- X==true.

% Some tiny.
% ?- subst([X-b], f(X,Z), Y).
%@ Y = f(b, Z).

subst(M, X, Y):- var(X), !,
(member(A-V, M), A==X
-> Y=V
; Y=X
).
subst(_, X, X):- atomic(X),!.
subst(M, X, Y):-
functor(X,F,N),
functor(Y,F,N),
subst_args(N,M,X,Y).

%
subst_args(0,_,_,_):-!.
subst_args(J,M,X,Y):-
arg(J,X,A),
subst(M,A,B),
arg(J,Y,B),
K is J-1,
subst_args(K,M,X,Y).

%
memq(X,[X0|_]):- X==X0, !.
memq(X,[_|Y]):- memq(X, Y).

Kuniaki Mukai

[Kuniaki Mukai]

I have improved a little bit codes zdd/2 in the previous post.
Now a zdd is a prolog goal that enumerates the all solutions.
An example is included below.
The previous codes included confusion of declarative
boolean reading against prolog procedural reading of zdd,
in ; and ->. ( negation as failure) Be careful not take
declarative reading the zdd. The other part is a rather
straightforward.

There may be a lot of problems in the codes, and I only hope
I have made a little contribution if any to current argument on the
API for attributed variables. I have no plan to go further.

%% zdd(+E, +Z, -Z0) is det.
%
% E: a list of variables, true, and false, representing.
% E is a multiset that represents a unification sate.
%
% Z: a zdd
% Z0: a zdd.
% a zdd is a prolog goal consisting -> ; , \+ variables in E, true, false.
%
% zdd(E, Z, Z0) is true if Z0 is unified with a prolog goal which
% enumerates exactly all assingments that satisies the given zdd Z as
% a boolen expression in backtracking.

% Example:
% ?- zdd:zdd([X,Y], ((X->Y;\+ X),(Y->X;\+ Y)), R), boole(X), boole(Y), once(R).
%@ X = Y, Y = true,
%@ R = (true->(true->true;false);true->false;true) ;
%@ X = Y, Y = false,
%@ R = (false->(false->true;false);false->false;true).

boole(true).
boole(false).

%
zdd(Vars, ZDD, ZDD0):-zdd_slim(Vars, ZDD, ZDD0).

%
zdd_slim([], Z, true):- zdd_slim(Z, Z0), Z0 = true,!.
zdd_slim([], _, false).

zdd_slim([X|Xs], Z, ZDD):- atom(X), !, zdd_slim(Xs, Z, ZDD).
zdd_slim([X|Xs], Z, ZDD):- subst([X-true], (Xs, Z), (Us, Then0)),
subst([X-false], (Xs, Z), (Vs, Else0)),
zdd_slim(Us, Then0, Then),
zdd_slim(Vs, Else0, Else),

ZDD = (X -> Then; Else).

%
zdd_slim(X, Y):- zdd_slim_rule(X, X0), !,
zdd_slim(X0, Y).
zdd_slim(X, X).

%
zdd_slim_rule(X, _) :- var(X), !, fail.
zdd_slim_rule((A, B), (A0, B)) :- zdd_slim_rule(A, A0).
zdd_slim_rule((A, B), (A, B0)) :- zdd_slim_rule(B, B0).
zdd_slim_rule((X, A), A) :- X==true.
zdd_slim_rule((A, X), A) :- X==true.
zdd_slim_rule((X, _), false) :- X==false.
zdd_slim_rule((_, X), false) :- X==false.

zdd_slim_rule(A -> B, A0 -> B) :- zdd_slim_rule(A, A0).
zdd_slim_rule(X -> _, false) :- X==false.

zdd_slim_rule(X -> A, A) :- X==true.
zdd_slim_rule(\+(A), \+(A0)) :- zdd_slim_rule(A, A0).
zdd_slim_rule(\+(X), true) :- X==false.
zdd_slim_rule(\+(X), false) :- X==true.

zdd_slim_rule((A; B), (A0; B)) :- zdd_slim_rule(A, A0).
zdd_slim_rule((A; B), (A; B0)) :- zdd_slim_rule(B, B0).

zdd_slim_rule((X; _), true) :- X==true.
zdd_slim_rule((X; B), B) :- X==false.


Kuniaki Mukai

[Jan Burse]

What is your result for:

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

[Kuniaki Mukai]

For ZDD = ( X -> true ; ( Y -> true ; false ) ), the result is this:

% ?- ZDD = ( X -> true ; ( Y -> true ; false ) ),
% zdd_con(ZDD, H), zdd_label(H).

%@ ZDD = (true->true;true->true;false),

%@ X = Y, Y = true,

%@ put_attr(H, zlink, zdd([true, true], true)) ;
%@ ZDD = (true->true;false->true;false),
%@ X = true,
%@ Y = false,
%@ put_attr(H, zlink, zdd([true, false], true)) ;
%@ ZDD = (false->true;true->true;false),
%@ X = false,
%@ Y = true,
%@ put_attr(H, zlink, zdd([false, true], true)) ;
%@ ZDD = (false->true;false->true;false),

%@ X = Y, Y = false,

%@ put_attr(H, zlink, zdd([false, false], true)).;

Kuniaki Mukai

p.s. Codes for my zdd had a bug on order of zdd_slim_rule/2 wrt if-then-else (A->B; C).
This rule must be of higher priority.

p.s. Now I have changed boolean constraint for user to be declarative via a macro expansion,
(not that on prolog ). That is, A->B <===> (not A) or B (material implication)
but (A->B;C) internally behaves as in Prolog.

p.s. Now zdd constraints directly works on `atrributed_unify_hook/2’. the interface is
so simple and transparent I was surprised a little bit.

attr_unify_hook(V, Y):-
( get_attr(Y, zdd, A)
-> zdd_update(A)
; zdd_update(V)
).

p.s. Although there may remain many bugs, I am satisfied with this toy program.

[Jan Burse]

I still dont understand why Markus Triskas code gives [X,Y]=[1,1]
for XOR. Maybe there is somewhere a programming bug.

His ideas are not totally wrong, in practice when implementing ZDD,
we need to assign X=0, since X=1 would anyway lead to false.

Here are some comparison of OBDD, ROBDD and ZDD.

ROBDD can compress OR but ZDD cannot compress OR.
ZDD can compress XOR but ROBDD cannot compress XOR.

/* test case OR */

% ?- OR = (X -> (Y -> true; true); (Y -> true; false)),

%    solve_obdd(OR), write(X-Y), nl, fail.

% 0-1

% 1-0

% 1-1



% ?- OR = (X -> true; (Y -> true; false)),

%    solve_robdd(OR, [X,Y]), write(X-Y), nl, fail.

% 0-1

% 1-0

% 1-1



% ?- OR = (X -> (Y -> true; true); (Y -> true; false)),

%    solve_zdd(OR, [X,Y]), write(X-Y), nl, fail.

% 0-1

% 1-0

% 1-1



/* test case XOR */

% ?- XOR = (X -> (Y -> false; true); (Y -> true; false)),

%    solve_obdd(XOR), write(X-Y), nl, fail.

% 0-1

% 1-0



% ?- XOR = (X -> (Y -> false; true); (Y -> true; false)),

%    solve_robdd(XOR, [X,Y]), write(X-Y), nl, fail.

% 0-1

% 1-0



% ?- XOR = (X -> true; (Y -> true; false)),

%    solve_zdd(XOR, [X,Y]), write(X-Y), nl, fail.

% 0-1

% 1-0

The code is straight forward and on gist:
https://gist.github.com/jburse/347bb01354782ef58cf796910de28b69#file-zdd-p

[Jan Burse]

Compress means, we can supply a tree which is not
a complete tree (which would have 2^n-1 nodes where n is
the number of variables). Note the syntax for trees is:

tree --> true
          | false
          | (variable -> tree; tree)

There is no such nonsense as (\+)/1. BDD trees are based
on a ternary operator (_-> _;_). I was using the idea of CWA to
explain the compression that is used in ZDD.

[Jan Burse]

Maybe there is somewhere a confusion with the ternary
operator (_ -> _;_). I still take it as if-then-else, so
the first branch is taken if the variable is true, and the
second branch is taken if the variable is false.

This gives for a complete tree of an OBDD this simple code:

solve_obdd(true).

solve_obdd((X -> _;B)) :- X=0, solve_obdd(B).

solve_obdd((X -> A;_)) :- X=1, solve_obdd(A).

See also here for code of ROBDD and ZDD:
https://gist.github.com/jburse/347bb01354782ef58cf796910de28b69#file-zdd-p

[Jan Burse]

XOR should maximally succeed twice. It seems you show
something else than XOR, I cannot clearly detect the result
of XOR in what you posted Kuniaki Mukai.

[Jan Burse]

In sat based on boolean ring, you might succeed once with
a constraint X br= Y+1. Where + is the boolean ring add (=xor).

[Kuniaki Mukai]

Assuming the ZDD is for XOR:

% ?- ZDD = ((X;Y), \+ (X, Y)),
% zdd_con(ZDD, H), zdd_label(H).

%@ ZDD = ((true;false), \+ (true, false)),

%@ X = true,
%@ Y = false,
%@ put_attr(H, zlink, zdd([true, false], true)) ;

%@ ZDD = ((false;true), \+ (false, true)),

%@ X = false,
%@ Y = true,
%@ put_attr(H, zlink, zdd([false, true], true)) ;

%@ false.

Kuniaki Mukai

[Jan Burse]

Now this is getting a little bit absurd, I guess you are trolling
now. You write ZDD = Expr, but your Expr is just a boolean
expression, and not a binary decision diagram.

Here is a definition of both ROBDD and ZDD on wiki:

A zero-suppressed decision diagram (ZSDD or ZDD) is
a type of binary decision diagram (BDD) where instead of
nodes being introduced when the positive and the negative
part are different, they are introduced when positive
part is different from constant 0.
https://en.wikipedia.org/wiki/Zero-suppressed_decision_diagram

The above paragraph explains both compression rules,
the rule present in ROBDD an the rule present in ZDD.
You can view them as:

ROBDD compression:
      (X -> A;A) ==  A

ZDD compression:
      (X -> false; A)  ==  A

You find the ZDD compression also very nicely explained
in the MINATO Shin-ichi paper. So ZDD deals with OBDD
compressed according to the ZDD compression rule.

It doesn't deal with boolean expressions, at least at
some place we should see a ZDD tree. You can also
define boolean expresions over ZDD.

But in your post below, I neither see a ZDD input nor a
ZDD output (there is (->)/2 nowhere). Can you show
something where we have ZDD input or output?

[Jan Burse]

When I want to solve boolean expressions, I simply might use:

?- member(X,[true,false]), member(Y,[true,false]), (X;Y), \+ (X,Y).
X = true,
Y = false ;
X = false,
Y = true ;

Am Donnerstag, 7. September 2017 11:26:17 UTC+2 schrieb Kuniaki Mukai:

[Kuniaki Mukai]

The binary decision tree is used internally, whose form is faithful
to that used in my post. For the XOR:

% ?- ZDD = ((X;Y), \+ (X, Y)),

% zdd_con(ZDD, H), get_attr(H, zlink, Z), writeln(Z).
%@ zdd([_8118,_8132],(_8118->(_8132->false;true);_8132->true;false))
%@ Z = zdd([X, Y], (X->(Y->false;true);Y->true;false)),
%@ put_attr(X, zdd, H),
%@ put_attr(H, zlink, zdd([X, Y], (X->(Y->false;true);Y->true;false))),
%@ put_attr(Y, zdd, H).

However this toy program does not go deep to the structure sharing,
though I see no difficulty to do so.

Bye

Kuniaki Mukai

[Douglas Miles]

​​

Sure, I have plenty of mischievousness use cases for attvars.  I can achieve same mischievousness in many ways even with post-unify. (That is for a different thread, if at all)    

If an attvar is a term in which you which to preserve information with, it only ever makes sense to allow unification with another attvar.  Not with terms of a different place in the "standard order" of terms.    So due to this, in *some* of my uses I make sure I throw a programming error if I accidently unify with an anything atomic or compound.    Unless I plan on manipulating that other terms such as a FOL skolemization (compound)  to store that information on.  My complaint here is i have to reconstruct all of the same skolem attributes ( which are missing since I only get to see one attribute at a time)  So this forces all my attributes to be stored under the one module key.  Really to keep it simple.. I use a "proxy attvar" as an attribute of a attvar I know will be lost during unification.

Main issue in post-unification phase the attvar's identity is now missing. So if the attvar occurred in other terms this can no longer be detected using ==/2 against other variables.   Also this throws off occurs checking for programmers not relying on the C-ified version to have done the occurs checking "before".   Does this complicate things?   Will leave that to Markus to explain why.    

This kind of mistakes could be avoided with the SICStus interface.
SICStus is also widely known as one of the fastest Prolog systems
available. Take from this what you will.

It probably would be even faster when it adopted the SWI-Prolog attvar
interface as, however you look at it, post-unification hooks simply have
to do less work and have less impact on the rest of the system.

​Sicstus attvar system is not faster (or nesc slower) and if it was, would it matter since CLP(FD) is written purely in C​ ?

[Jan Burse]

But:

(_8118->(_8132->false;true);_8132->true;false))

Is not a ZDD. 

You didn't compress according to this rule:

Jan Burse wrote:
> ZDD compression:
>      (X -> false; A)  ==  A

Check for yourself the Wiki phrasing:

A zero-suppressed decision diagram (ZSDD or ZDD) is
a type of binary decision diagram (BDD) where instead of

nodes being introduced .., they are introduced when positive

part is different from constant 0.
https://en.wikipedia.org/wiki/Zero-suppressed_decision_diagram

In your example a positive part is

_8132->false
And it is constant 0 (same as false).

But you didn't supress it, so its not ZDD.

[Jan Burse]

To understand ZDD compression, have a very close look at:

The MINATO Shin-ichi paper itself. You can check yourself there is

PDF of the ZDD paper on the internet. The PDF link is here:
https://eprints.lib.hokudai.ac.jp/dspace/bitstream/2115/16895/1/IJSTTT3-2.pdf

The ZDD compression rule, is explained in Figure 4,

with the title "New reduction rule for ZBDDs".

[Jan Burse]

If you don't want to download the full PDF, I have uploaded Fig 4 here:
https://gist.github.com/jburse/347bb01354782ef58cf796910de28b69#gistcomment-2196147

The zero in a box, is a leaf node, Markus Triska uses b(false),
you and I we used simply false I guess.

The x in a circle is the tertiary if-then-else, you see we go from:

   (X -> false; F)

To simply:

    F

Thats the ZDD compression.

[Kuniaki Mukai]

I was not aware ZDD rule at all. Thanks.
For the ZDD rule, I have introduced if-then-else term if(B, T, E)
instead of B->T; E of Prolog. if/3 seems work. I have to
look more close, tomorrow. I will check Minato’s paper closely
if necessary. I hope not so.

Thanks.

Kuniaki Mukai

[Jan Burse]

I noticed the difference when I tried to consult this nice
book about Minato, but didn't find anything:

Propositional Logic: Deduction and Algorithms

(Cambridge Tracts in Theoretical Computer Science, Band 48) 

(Englisch) Gebundene Ausgabe – 28. August 1999

von Hans Kleine Büning (Autor), Theodor Lettmann (Autor)

https://www.amazon.de/Propositional-Logic-Deduction-Algorithms-Theoretical/dp/0521630177

So I guess its overpriced and/or already old.

[Jan Burse]

sympy can generate POS or SOP:

The SOPform function uses simplified_pairs and a redundant group- eliminating algorithm to convert the list of all input combos that generate ‘1’ (the minterms) into the smallest Sum of Products form.

http://docs.sympy.org/latest/modules/logic.html

https://en.wikipedia.org/wiki/Quine%E2%80%93McCluskey_algorithm

[Jan Burse]

XSB Prolog has also a SICStus like interface, but
without the third argument the continuation goals:

"verify_attributes(-Var, +Value)

This predicate is called whenever an attributed variable Var (which has at least one attribute) is about to be bound to Value (a non-variable term or another attributed variable). When Var is to be bound to Value, a special interrupt called attributed variable interrupt is triggered, and then XSB's interrupt handler (written in Prolog) calls verify_attributes/2. If it fails, the unification is deemed to have failed. It may succeed non-deterministically, in which case the unification might backtrack to give another answer."

http://xsb.sourceforge.net/shadow_site/manual2/node4.html

But it also allowws non-deterministically to succeed, which
I think is superflous. Assume you have a PL_unify foreign
function implementation helper. Should this PL_unify suddently
become non-deterministic, what would be the API.

If you have such foreign function implementations helpers,
that are not able to provide non-deterministic unification,
will they break attribute variables, or will the hook (in
XSB called interrupt), be called much later?

[Jan Burse]

How can it be called latter, if PL_unify returned already,
and some variable was already bound. The SICStus API
and the XSB API variant, are very foreign function unfriendly,

because they require that a unification, that is usually viewed
deterministic, as suddently non-deterministic. It should go
without saying that I prefer my own Jekejeke Prolog solution,

where the hook is required to be deterministic, but it is
allowed to inject goals between the head and body of
the current clause. The picture is very simple, if a clause

is invoked, without any attribute variables usually the
following happens: head and goal are determinsitically
unified, indicated by the = sign:

head :- body
   =
goal

In Jekejeke Prolog the unification hooks are still considered
to be deterministically, but they are allowed to push new
goals between the head and the body, lets call them agoals:

head :-  agoals, body
  =
goal

Its now easy to see that we can move any non-deterministic
handling of an attribute variable into the agoals and execute
there. So there is no loss by the Jekejeke Prolog variant

of a verification hook. We can even define a meta interpreter
for it. Lets look at the usual meta interpreter, the vanilla
interpreter, it reads as follows, I made the unification explicit:

solve(true).
solve((A,B)) :- solve(A), solve(B).
solve(P) :- clause(Q,B), unify(P,Q), solve(B).

unify(H,H).

Now assume this unification returns some goals, so
basically it modifies the current body B, and returns a new
body C, which is then executed, the new solve reads as follows:

solve(true).
solve((A,B)) :- solve(A), solve(B).
solve(P) :- clause(Q,B), unify(P,Q,B,C), solve(C).

unify(....) :- /* if attribute variables are there verify
                      via hooks and allow them to push
                      new agoals */
unify(H,H,B,B). /* if no attribute variables are there */

On the foreign function front, in Jekejeke Prolog, the progammer
doesn't see much. So to speak he can still use PL_unify as
before, there is not really a new set of arguments. But there

is a new PL_push_agoal . This API can orient itself, and
detect the current clause context, and push agoals. Actually
its implemented similarly like an interrupt, the XSB idea

is not bad. Signals are kind of polled by the interpreter. We
do not only poll signals, but also an agoal queue. If a PL_unify
fails and variables are unbound the agoal queue is also

cleared, so it cannot happen that some agoals are injected
to the wrong clause. But it is clearly seen that the agoal
execution is asynchronous to the verify hooks, it happens

eventually but not always later. All veriy hooks must succeed,
and the whole PL_unify must return true, only then the interpreter
gets a chance to poll the agoal queue. If PL_unify returns false

the agoal queue gets rolled back similar like the variable
instantiations MUST BE rolled back in some way, and the
interpreter will just poll an empty agoal queue, for example

during backtracking, etc..

[Jan Burse]

I think in SWI-Prolog an agoal queue already exists. Not like
in Jekejeke Prolog where we have separately a signal slot
and an agoal queue,

Signal handling is basically already a queue. I am not talking
anout on_signal/3 which is for some POSIX signals. I am more
talking about thread_signal/2,

according to the docu there is already a kind of queue:
The predicate thread_signal/2 itself places Goal into the signalled
thread's signal queue and returns immediately.
http://www.swi-prolog.org/pldoc/doc_for?object=thread_signal/2

Now allow the same for agoals, preferably on a different queue
with a slightly different policy, and you are done...(Well there
some more to do, the rollback, etc.., but you got the idea).

[Kuniaki Mukai]

In order to make the zdd_slim_rule definition,
I have introduced if(A, B, C) terms for (A->B; C).

Added rules for this term:

1. if(A, B, B) ==> B
2. if(true, A, B) ==> A
3. if(false, A, B) ==> B

My construction on 'ZDD' term is based on
a simple recursive definition on the number of
variables.

For example:

- a variable, 'true', and 'false' are a ZDD.
- if(_, false, false) is NOT a ZDD.
- If B, C are ZDD and X is a fresh variable
then so is if(X,B,C).

Relying on such like recursion rules, I think
my algorithm constructs ZDDs for a given boolean
expression, aside quality of the obtained ZDD.

Kuniaki Mukai


> I was not aware ZDD rule at all. Thanks.
> For the ZDD rule, I have introduced if-then-else term if(B, T, E)
> instead of B->T; E of Prolog. if/3 seems work. I have to
> look more close, tomorrow. I will check Minato’s paper closely
> if necessary. I hope not so.
>
> Thanks.
>

> Kuniaki Mukai
>
>

>> On Sep 7, 2017, at 20:45, Jan Burse <burs...@gmail.com> wrote:
>>

[Jan Burse]

Thats still not ZDD. If you have a rule:

      if(A, B, B)                ==> B

Thats simply the usual ORBDD. But it gives you wrong
ZDD results. For example if you start with:

       if(X, true, true)

Then you reduce this to:

       true

But in ZDD this is the same as:

        if(X, false, true)

Just apply Fig 4 here backwards:
https://gist.github.com/jburse/347bb01354782ef58cf796910de28b69#gistcomment-2196147

[Jan Burse]

The small f in Fig 4 is a whole subtree and not false.
false would be 0 in Fig 4 of MINATO Shin-ichi.

[Kuniaki Mukai]

I thought zdd means semantically an encoding of solutions (truth tables),
and suppressing nodes going “zero” (empty set of solutions).
This is the all what I know about zdd.

Kuniaki Mukai

[Jan Burse]

I have uploaded a picture of the rule if(A,B,B)==>B as well.
Its also found in the motivation introduction part of the

MINATO Shin-ichi paper. Before MINATO Shin-ichi introduces
his ZDD, he describes the usual O(R)BDD (ordered (reduced) BDD).

You see the newly added picture here:
https://gist.github.com/jburse/347bb01354782ef58cf796910de28b69#gistcomment-2196147

[Jan Burse]

Hi,

I don't know whether you can mix ZDD and ORBDD in the
same tree. You would need two have two different jumps,

jump_1 and jump_2. But usually a jump is just that
a node is missing, that a variable is not found along a path.

Have a Nice day!

[Jan Burse]

Since ZDD are little bit complex, why not discuss the API issue
on the basis of CNF. Here is a nice paper, with a SICStus
solution. Can this be done in SWI-Prolog. If yes, how? If no, why?

A Pearl on SAT Solving in Prolog
Jacob M. Howe and Andy King, 2010
http://www.staff.city.ac.uk/~jacob/solver/flops.pdf

[Carlo Capelli]

2017-09-08 12:48 GMT+02:00 Jan Burse <burs...@gmail.com>:

Since ZDD are little bit complex, why not discuss the API issue
on the basis of CNF. Here is a nice paper, with a SICStus
solution. Can this be done in SWI-Prolog. If yes, how? If no, why?

A Pearl on SAT Solving in Prolog
Jacob M. Howe and Andy King, 2010
http://www.staff.city.ac.uk/~jacob/solver/flops.pdf

Jan, thanks so much. It's really a pearl !

I simply copied the ~20 lines into SWI-Prolog IDE, commented out the :- block (is it important ?), and tried:

?- L = [[false-X, true-Y], [false-X,false-Z]], sat(L, [X,Y,Z]), writeln(L).
[[false-false,true-true],[false-false,false-true]]
L = [[false-false, true-true], [false-false, false-true]],
X = false,
Y = Z, Z = true ;
...

<snip>

[Carlo Capelli]

2017-09-08 17:15 GMT+02:00 Carlo Capelli <cc.car...@gmail.com>:

2017-09-08 12:48 GMT+02:00 Jan Burse <burs...@gmail.com>:

Since ZDD are little bit complex, why not discuss the API issue
on the basis of CNF. Here is a nice paper, with a SICStus
solution. Can this be done in SWI-Prolog. If yes, how? If no, why?

A Pearl on SAT Solving in Prolog
Jacob M. Howe and Andy King, 2010
http://www.staff.city.ac.uk/~jacob/solver/flops.pdf

Jan, thanks so much. It's really a pearl !

Albeit not related to this thread, I'd like to 'reply' with a pearl - of different color - proposed by Paul Tarau.

A Hitchhiker’s Guide to Reinventing a Prolog Machine

( btw, I've started a (lazy) attempt to port from Java to Javascript )

[Martin]

Hi Carlo,

There's an implementation of block in swi prolog's
library/dialect/sicstus directory. I'm always confused by the module
syntax, but it's possible to consult the file directly. Then the :-
block statement is accepted. If I understand the paper/code correctly,
without blocking, unit propagation is applied too eagerly (because the
watches are not sufficiently delayed).

cheers, Martin

On 09/08/2017 05:15 PM, Carlo Capelli wrote:
>
>
> 2017-09-08 12:48 GMT+02:00 Jan Burse <burs...@gmail.com

> <mailto:burs...@gmail.com>>:

>
> Since ZDD are little bit complex, why not discuss the API issue
> on the basis of CNF. Here is a nice paper, with a SICStus
> solution. Can this be done in SWI-Prolog. If yes, how? If no, why?
>
> A Pearl on SAT Solving in Prolog
> Jacob M. Howe and Andy King, 2010
> http://www.staff.city.ac.uk/~jacob/solver/flops.pdf

> <http://www.staff.city.ac.uk/%7Ejacob/solver/flops.pdf>

>
>
> Jan, thanks so much. It's really a pearl !
> I simply copied the ~20 lines into SWI-Prolog IDE, commented out the :-
> block (is it important ?), and tried:
>
> ?- L = [[false-X, true-Y], [false-X,false-Z]], sat(L, [X,Y,Z]), writeln(L).
> [[false-false,true-true],[false-false,false-true]]
> L = [[false-false, true-true], [false-false, false-true]],
> X = false,
> Y = Z, Z = true ;
> ...
>
> <snip>
>

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

[Jan Burse]

Yes, oldie but goldie. SLD resolution can be seen as goal list
rewriting. Lets stick to the Peano example, instead of cls

write ~~> for input to a rewriting system, and dont use difference
lists but assume main input is a closed goal list (easier to detect stop):

/* rewriting rules ~~>/2, for clauses */
:- op(700,xfx,~~>).

[add(0,X,X)|Y] ~~> Y.
[add(s(X),Y,s(Z))|T] ~~> [add(X,Y,Z)|T].

now the meta interpreter will look a little different as in the paper,
namely we will have reduce is just the transitive closure of ~~>:

/* transitive closure of ~~>/2 */
reduce([]).
reduce(L) :- L ~~> R, reduce(R).

Now lets compute 2+2=4:

Welcome to SWI-Prolog (threaded, 64 bits, version 7.5.8)

SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.

?- reduce([add(s(s(0)),s(s(0)),X)]).

X = s(s(s(s(0)))) .

Why I am telling all this? Well as it happens Jekejeke Prolog is
implemented this way, heap only. But what I want to explore,

is whether we can sneak in the agoals queue (attribute variable
pushed goals) idea in this model. Lets first make the unification

explicit, namely as follows:

/* transitive closure with explicit unify */
reduce([]).
reduce(L) :- M ~~> R, unify(L,M), reduce(R).

unify(H,H).

Now assume that the attribute variables push some goal, so
basically an attribute variable goal push, is also a rewriting,
namely pushing goal is call(G), where G is a new goal (hint
that is the usual ISO call/1 predicate) :

/* rewriting rules ~~>/2, for goal pushing*/
[call(G)|X] ~~> [G'|X]        /* G' is the body conversion of G */

So attribute variables would trigger such call(G), before
reduce can continue. Without going into two much details
lets only sketch it as follows:

/* transitive closure with explicit unify and attribute variable hooks */
reduce([]).
reduce(L) :- M ~~> R, unify(L,M,R,N), reduce(N).

unify(H,H,B,[call(G1),..,call(Gn)|B]) :-
     /* all the attribute variable pushes G1,..,Gn */
unify(H,H,B,B).
    /* if no attribute variable happens */

So we execute the pushed goals by the attribute variable hooks
inside call/1 wrappers, so that a malicious end-user cannot push
a cut (!)/0 or somesuch.

[Jan Burse]

If I show the measurements in the paper in percentage I get (only queens 11):

System	Abs	Rel SWI
our interpreter	5.710	311%
Lean Prolog	3.991	217%
Styla	13.164	717%
SWI-Prolog	1.835	100%

Now if I do new measurements on my machine, I get:

   Welcome to SWI-Prolog (threaded, 64 bits, version 7.5.13)

   SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.

  ?- time((queens, fail; true)).
  % 7,717,186 inferences, 0.578 CPU in 0.578 seconds (100% CPU, 13348646 Lips)
  true.

And also another Java Prolog:

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

   ?- time((queens, fail; true)).
   % Up 905 ms, GC 10 ms, Thread Cpu 875 ms (Current 09/08/17 18:37:17)
   Yes

So if I show percentage again I get:

System	Abs	Rel SWI
Jekejeke	0.905	157%
SWI-Prolog	0.578	100%

So maybe the paper should be renamed Hitchhikers Guide to a slow Prolog.

Am Freitag, 8. September 2017 17:39:40 UTC+2 schrieb cc.carlo.cap:

[Carlo Capelli]

2017-09-08 18:03 GMT+02:00 'Martin' via SWI-Prolog <swi-p...@googlegroups.com>:

Hi Carlo,

There's an implementation of block in swi prolog's
library/dialect/sicstus directory. I'm always confused by the module
syntax, but it's possible to consult the file directly. Then the :-
block statement is accepted. If I understand the paper/code correctly,
without blocking, unit propagation is applied too eagerly (because the
watches are not sufficiently delayed).

cheers, Martin

Thanks, Martin.

The syntax that worked for me is simply

:- use_module(library(dialect/sicstus)).

On 09/08/2017 05:15 PM, Carlo Capelli wrote:
>
>
> 2017-09-08 12:48 GMT+02:00 Jan Burse <burs...@gmail.com
> <mailto:burs...@gmail.com>>:
>
>     Since ZDD are little bit complex, why not discuss the API issue
>     on the basis of CNF. Here is a nice paper, with a SICStus
>     solution. Can this be done in SWI-Prolog. If yes, how? If no, why?
>
>     A Pearl on SAT Solving in Prolog
>     Jacob M. Howe and Andy King, 2010
>     http://www.staff.city.ac.uk/~jacob/solver/flops.pdf
>     <http://www.staff.city.ac.uk/%7Ejacob/solver/flops.pdf>
>
>
> Jan, thanks so much. It's really a pearl !
> I simply copied the ~20 lines into SWI-Prolog IDE, commented out the :-
> block (is it important ?), and tried:
>
> ?- L = [[false-X, true-Y], [false-X,false-Z]], sat(L, [X,Y,Z]), writeln(L).
> [[false-false,true-true],[false-false,false-true]]
> L = [[false-false, true-true], [false-false, false-true]],
> X = false,
> Y = Z, Z = true ;
> ...
>
> <snip>
>
> --
> 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
> <mailto:swi-prolog+unsub...@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.

[Carlo Capelli]

Who knows... Pearls take their time to grow up :)

Am Freitag, 8. September 2017 17:39:40 UTC+2 schrieb cc.carlo.cap:

A Hitchhiker’s Guide to Reinventing a Prolog Machine

( btw, I've started a (lazy) attempt to port from Java to Javascript )

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

[Jan Burse]

Nevertheless I like the paper of Paul Tarau, because the Java heap
is extremly annoying. Sometimes I think Prolog should NOT be

implemented in Java. This observation came recently when
experimenting with some multithreading, especially comparing

with the performance of SWI-Prolog, the latest release, somehow
C has some advantage over the safe and hence unchangeable

memory model of Java programming language. It could be that
SWI-Prolog and C is the better option in the long run...

[Jan Burse]

What does us buy this view? Well the rollback of the pushed
goals, is just ordinary backtracking. If Paul Tarau might want
to tell us how the goal stack is ordinary difference lists buildup

and teardown during backtracking. Same for injected
attribute goals. Its also a buildup [call(G1),..,call(Gn)|B]
of a list, and similarly a tail recursive meta interpreter

which can be turned into a loop plus some backtracking
data structure. Paul Tarau has only two data structures
Clauses and the Spine besides Engines!

Now lets do the same for attribute variables...