Re: [SWIPL] SWISH down

[Jan Wielemaker]

It is back up. Thanks for the message and sorry for the inconvenience.
We had a chat that it is about time to add reduncdancy ...

--- Jan

On 17/05/18 16:40, 64kilobit via SWI-Prolog wrote:
> Hello,
>
> the site https://swish.swi-prolog.org/ is down. First noticed about
> 12:00 UTC, 2018-05-17.
>
> Error Message: *502 Bad Gateway nginx/1.10.3 (Ubuntu)*
>
> I tested this from 2 different networks and 2 computers.
>
> I informed the IRC Channel, which answered I would be a good idea to use
> the mailinglist.
>
> Thanks for the effort and all the work.
>
>
> Kind Regards,
>
> Kilobit
>
> --
> 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>.
> Visit this group at https://groups.google.com/group/swi-prolog.
> For more options, visit https://groups.google.com/d/optout.

[Kuniaki Mukai]

About the number of nodes of ROZDD as a family of subsets of a set V,
I said in a recent thread something like A:

(A) Most nodes becomes useless (garbage) when the construction is done.

I must withdraw A, because I have not a proof for it.
The A above comes to me only from the construction of the powset of V,
including the case in which V = A x B for the map spaces:
the set of functions from A to B.

Kuniaki Mukai

[Kuniaki Mukai]

More precisely,

Let |V| = n: n is the cardinal of V. Then there are 2^(2^n) families of subsets of V:

|ROZDD(V)| = 2^(2^n).

So, for any 1=< k =< 2^(2^n), there exists a rozdd g in ROZDD(V) which has exactly k nodes.

This proposition is almost obvious. I am ashamed for not noticing this basic fact before.

Kuniaki Mukai

[Jan Wielemaker]

On 17/05/18 20:25, Jan Wielemaker wrote:
> It is back up. Thanks for the message and sorry for the inconvenience.
> We had a chat that it is about time to add reduncdancy ...

Seems this was caused by some changes to the exception unwinding code
that now uses a buggy path way more often than older versions. Should be
fixed now.

I general it seems we are facing a problem. Where last year the peak
usage of SWISH was about 200 concurrent users it now often exceeds 400.
That doesn't pose much capacity problems to the server yet. I've only
enlarged connection and file handle limits.

What is more worrying is that I see sudden login/logout of up to 250
users. That suggests large classroom usage. Seems we need horizontal
scaling, both to support more users and to guarantee close to 100%
uptime.

If this was a startup I'd be happy, but SWISH as a teaching community
service is a project without financial or organizatorial backup. In
end end we need

- Hardware in several places or hired cloud servers.
- A robust load balancer that can deal with the stateful query
processing (all the rest is stateless)
- Distributed storage management. Currently multiple nodes can
share via a share file system.
- Some plan and people to prepare the software
- Some people willing to play operator to handle emergencies.

Ideas, volunteers?

Cheers --- Jan

[Kuniaki Mukai]

Just a report, hoping this report does not disturve the forum.

I have tested a ROZDD processing which constructs
a large function spaces whose domain and range have both one thousand elemets.
Query and codes are below.

It is surprisingly fast.

?- N = 1000, numlist(1, N, L), zdd_init, time(zdd_map(L, L, M)).
33,050,578 inferences, 3.938 CPU in 4.094 seconds (96% CPU, 8393729 Lips)
N = 1000,
L = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
M = 1000000.

zdd_map([], _, true).
zdd_map([X|Xs], R, Y):- zdd_map(Xs, R, Z),
zdd_map(R, X, Z, Y).
%
zdd_map([], _, _, false).
zdd_map([V|Vs], X, Z, Y):-
zdd_map(Vs, X, Z, Y0),
cofact(Y, if(X-V, Z, Y0)).

On the contray, a usual list processing version does not terminate
even for N = 10.

Kuniaki Mukai

[j4n bur53]

I guess its this algorithm:
https://groups.google.com/d/msg/swi-prolog/oVFpyytrMK4/4PlAGjtvAQAJ

which needs only steps #(D)*#(R) to construct map(D,R).

[j4n bur53]

I guess your cofact needs around 16 inference steps.
If I use a cofact that does nothing and needs only 1
inference step I get around 2*#(D)*#(R) inference steps:

?- findall(X,between(1,400,X),L), findall(X,between(1,300,X),R), time(zdd_map(L, R, _)).

% 240,802 inferences, 0.062 CPU in 0.071 seconds (87% CPU, 3890618 Lips)

L = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],

R = [1, 2, 3, 4, 5, 6, 7, 8, 9|...].

?- findall(X,between(1,200,X),L), findall(X,between(1,600,X),R), time(zdd_map(L, R, _)).

% 240,402 inferences, 0.064 CPU in 0.073 seconds (88% CPU, 3734806 Lips)

L = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],

R = [1, 2, 3, 4, 5, 6, 7, 8, 9|...].

Code:

% dummy, used for pair, concat, +
cofact(X, X).

[Kuniaki Mukai]

> On May 18, 2018, at 21:47, j4n bur53 <janb...@xlog.ch> wrote:
>
> I guess its this algorithm:

Never, Not at all.

In the first place, I did not think you are doing “ROZ" programming.

Also, R(educed) of ROZDD means complete structure sharing, or
equivalently, I preferf to say, extensionality in the sense of set theory (Axiom of extensionality).

Most of ROZDD programming codes inevitably looks similar like my codes so far posted, that is, a style of recursion on
binary decision trees. The cofact primitive works like X = [A|B] in the traditional list processing which works
as both constructor and destructor. I dare to say, ROZ programing is in a sense cofact programming.

Kuniaki Mukai

[j4n bur53]

Well what the ROZ is doing is a blackbox, its only the
predicate cofact/2. It can be anything, provided it preserves

the semantics that are required logically for this builder. So
you could use the same O(#(D)*#(R)) algorithm with potatos. :-)

[Kuniaki Mukai]

On May 19, 2018, at 0:01, j4n bur53 <janb...@xlog.ch> wrote:

Well what the ROZ is doing is a blackbox, its only the 
predicate cofact/2. It can be anything, provided it preserves 

I posted codes cofact early in different name something like getzdd, 

getid_with_zero_suppress.  So it is not a blackbox, but array doubling, access,  and 

rehash things.   It might not have been  kind for those who are interested if any.

Kuniaki Mukai

[j4n bur53]

But if you use hashing and doubling, this black box will have
O(1) compexity, and since the algorithm is rectangular, it
will take #(D)*#(R). Its just the algorithm. You can view map(D,R),

as a special case of dependent function space pi x:D.R(x), where
each R(x) is constant. In general the size of such a function space is,
a function f would be an array or sequence r, where you index

with the argument value dj, and get some value r(dj) in R(dj),
so that the set of all arrays or sequences r, is this set:

         R(d1) x R(d2) x ... x R(dn-1) x R(dn)

But when R(x) is constant the size of such a function space is,
with the special case pow(n) = 2'n:

        R^n

but nevertheless you can use the product formula above to
construct the function space, and if you use the above product
formula recursively you get your algorithm and the same I posted.

Bye

P.S.: Here is the recursive formula:

    R(d1) x R(d2) x ... x R(dn-1) x R(dn) =

    {r1} x H u {r2} x H u .. u {rm-1} x H u {rm} x H

    where

    H = R(d2) x ... x R(dn-1) x R(dn)

    {r1,r2,..,rm-1,rm} = R(d1)

[j4n bur53]

Maybe an even faster algorithm would use some
bisection, for example bisect the product:

        R(d1) x R(d2) x ... x R(dn-1) x R(dn)

Into two sub products:

     R(d1) x R(d2) x ... x R(dm-1)

     - and -

     R(dm) x ... x R(dn-1) x R(dn)

So it could be that cofact/ROZ programming is not the
best solution, that with bisection and maybe other trees, you
could even get a faster map(D;R) computation,

if you dare to compute it.

[j4n bur53]

With bisection you would possibly get an algorithm
which calls the tree blackbox operations

     O(log_2 #(D)*#(R)) times

and not

     O(#(D)*#(R)) times

But the overall performance would depend on what the
blackbox can do, how it combines the bisections.

Disclaimer: Not sure whether this can be done.

P.S.: This is the same trick how you would compute
(x+1)^5 you would not compute (x+1)*(x+1)*(x+1)*(x+1)*(x+1),
but rather ((x+1)^2)^2*(x+1).

[Kuniaki Mukai]

For those who happen to be interested in the ROZ processing.

% cofact/2 is bi-directional.
cofact(Id, C):- integer(Id), !, getzdd(Id, C).
cofact(X, if(_, false, X)):-!. % zero-suppress.
cofact(truth(I0), if(I, truth(I), truth(I))):-!, succ(I, I0). % for sat mode only
cofact(proper(I0), if(I, truth(I), proper(I))):-!, succ(I0, I). % for sat mode only.
cofact(Id, C):- getid(C, Id).

cofact(X, if(A,L,R)) works like X =[L|R] in list processing, bidirectionally, which
I hope, useful to enjoy simply ROZDD processing like list processing.

I don’t think cofact is the best primitive for ROZDD processing, but it works for
now so and so for learning purpose of ROZDD.

Kuniaki Mukai

[Kuniaki Mukai]

> P.S.: This is the same trick how you would compute
> (x+1)^5 you would not compute (x+1)*(x+1)*(x+1)*(x+1)*(x+1),
> but rather ((x+1)^2)^2*(x+1).

This is also well-known. In fact I used this technique in
“domino” tiling problem, which I posted in this forum. I did so
because some page talked that a similar problem took three days
computer running. I forgot the context of the page.
Fortunately, my solution took only a few second.

Anyway it will be really good that you can apply this technique in your ROZ programming.
Good luck !.

Kunaiki Mukai

[j4n bur53]

Actually the Acronym ROZ doesn't make any sense.
It would mean Reduced Ordered Zero suppressed.

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

But I am not sure whether a tree can be both
reduced and zero suppressed.

Lets say Reduced means this BDD rule:

    bdd-if-then-else(V, A, A) == A

    "In popular usage, the term BDD almost always refers to Reduced
    Ordered Binary Decision Diagram (ROBDD in the literature, used
    when the ordering and reduction aspects need to be emphasized)."
    https://en.wikipedia.org/wiki/Binary_decision_diagram#Definition

And lets say Zero suppressed means this ZDD rule:

    zdd-if-then-else(V, F, A) = A

But a tree cannot be both reduced and zero suppresed.

[j4n bur53]

You can also try Google, there is not a single ROZDD mention.
https://www.google.ch/search?q=ROZDD

The term doesn't exist. You would need to call your trees
ZOBDD. Or ZBDD resp ZDD if there is no Ordering. Whereby I
 dunno whether they are only ZBB or ZOBDD.

Do you have some ordering?
In this code I don't see some ordering:

%  cofact/2 is bi-directional.
cofact(Id, C):- integer(Id), !, getzdd(Id, C).
cofact(X, if(_, false, X)):-!. % zero-suppress.
cofact(truth(I0), if(I, truth(I), truth(I))):-!, succ(I, I0).              % for sat mode only
cofact(proper(I0), if(I, truth(I), proper(I))):-!, succ(I0, I).        % for sat mode only.
cofact(Id, C):- getid(C, Id).

[j4n bur53]

An important property of the usuall R-O-BDD, is that the
reduction and ordering gives unique normal forms.

So you have this theorem for any variable ordering O:

    A = B  /* logical equivalent */

   -- if and only-if --

    ROBDD(O,A) == ROBDD(O,B) /* syntactic equivalent */

[Kuniaki Mukai]

> On May 19, 2018, at 1:46, j4n bur53 <janb...@xlog.ch> wrote:
>
> An important property of the usuall R-O-BDD, is that the
> reduction and ordering gives unique normal forms.

I am not sure, but is ROZDD “authorized” to be used by Knuth for ROBZDD ?

Kuniaki Mukai

[Kuniaki Mukai]

On May 19, 2018, at 1:46, j4n bur53 <janb...@xlog.ch> wrote:

An important property of the usuall R-O-BDD, is that the
reduction and ordering gives unique normal forms.

So you have this theorem for any variable ordering O:

    A = B  /* logical equivalent */

   -- if and only-if --

    ROBDD(O,A) == ROBDD(O,B) /* syntactic equivalent */

Really ? I am afraid this good property holds for ROBZDD.

I am not sure it does for ROBDD. A “counter" example is in my head

which use family of sets model.

Have you proved it yourself ?

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.

[j4n bur53]

Who is Knuth? Didn't he dieded already?

Anyway if you don't do a lot of ordering precautions,
it meight happen for these two inputs:

      map([1,2,3],[1,2,3],_)

     - and -

      map([3,2,1],[3,2,1],_)

That one of them is much slower, or that one of
of them is not working at all.

Am Freitag, 18. Mai 2018 18:43:14 UTC+2 schrieb j4n bur53:

[j4n bur53]

Or maybe there is no impact, since hashing
is ordering immune and the ZDD is ordered from
the input order index.

Maybe if you do thngs like:

      map([1,2,3],[1,2,3])-map([1,2],[1,2])

Versus:

      map([1,2,3],[1,2,3])-map([2,3],[2,3])

One of them could be slower.

[Kuniaki Mukai]

On May 19, 2018, at 2:19, j4n bur53 <janb...@xlog.ch> wrote:
>
> Who is Knuth? Didn't he dieded already?

Now it is time for me to contact a ROBDD people, or
to read articles on ROBZDD. I will let you know
about the state of official acronym if I get some.

Kuniaki Mukai

[Kuniaki Mukai]

> On May 19, 2018, at 2:19, j4n bur53 <janb...@xlog.ch> wrote:
>

> Who is Knuth? Didn't he dieded already?
>
> Anyway if you don't do a lot of ordering precautions,
> it meight happen for these two inputs:
>
> map([1,2,3],[1,2,3],_)
>
> - and -
>
> map([3,2,1],[3,2,1],_)

So far I take “@<“ as default ordering.
and assume the domain and the range sorted beforehand.
Note that cartesian product may be given as basic set. As you said,
attention must be paid to ordering of pairs. So far I have not
met yet difficulty.

By the way, you seem to begin talking about very basic things as if
you were newbie. I am afraid we are disturving enough this forum with
not interesting things to them including me.

Kuniaki Mukai

[j4n bur53]

Then be quiet. Its only you who posts all the time about
ROZ programming. Which is a really trival thing.

Just joking, please go on! And what is the timing of:

      map([1,2,3],[1,2,3])-map([1,2],[1,2])

versus:

      map([1,2,3],[1,2,3])-map([2,3],[2,3])

[j4n bur53]

Your functions are total? So map(D,R) is the set of total
functions? So the difference is probably the original set

in both cases, in the example I gave you. can you reproduce
that? So I need to give another example.Then what about

this test case:

      map([1,2,3],[1,2,3])-map([1,2,3],[1,2])

versus:

      map([1,2,3],[1,2,3])-map([1,2,3],[2,3])

Some difference in timing because of variable ordering?
Anyway both ideas are interesting to measure.

[Kuniaki Mukai]

On May 19, 2018, at 5:47, j4n bur53 <janb...@xlog.ch> wrote:
>
> Your functions are total? So map(D,R) is the set of total
> functions?

Yes.

> So the difference is probably the original set
>
> in both cases, in the example I gave you. can you reproduce
> that? So I need to give another example.Then what about
>
> this test case:
>
> map([1,2,3],[1,2,3])-map([1,2,3],[1,2])

No problem with my codes.

>
> versus:
>
> map([1,2,3],[1,2,3])-map([1,2,3],[2,3])

No problem with my zdd_map.

I don’t know what is wrong with such easy problem.

Anyway, enjoy debugging to get something new. I have been always
doing so.

I won’t reply anymore unless you quote me wrongly. As I asked before,
do not quote me.

Kuniaki Mukai

[j4n bur53]

Well you wrote "I have tested a ROZDD processing which constructs
a large function spaces whose domain and range have".

https://groups.google.com/d/msg/swi-prolog/ZQZV2i6TlN4/RmaG8e-0BgAJ

You only showed the data for one function space. What if you
have multiple function spaces in the same query and combine
them. Are you still fast. I dunno, and I don't have your code,

so I cannot test it. I also don't have a code that would convert
map(D;R) to BDD. But I think your original message is misleading
since it talks about large functions spaces in plural,

buit you only showed generating one function space. And you
did do anything with it. The interesting case would be like
computing the difference of two function spaces.

So I guess your post is a little cheating, you didn't show a lot.

[j4n bur53]

English would be: map(D,R) = a function space
No need to write "spaces", just "space".

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

But "spaces" would be the interesting thing. Or
what are you planning to do with map(D,R)?

[j4n bur53]

Some google, I find a paper here:

Scalable Exploration of Functional Dependency by
Interpolation and Incremental SAT Solving
Chih-Chun Lee, Jie-Hong R. Jiang, Chung-Yang (Ric) Huang
Alan Mishchenko - 2007
http://alcom.ee.ntu.edu.tw/publications/iccad07-fd.pdf

Which uses functional dependency detection to speed
up SAT solvers. There is a simple condition based
on computing off sets and on sets, and

then you can also compute don't care sets.

But I guess the method in the paper is more practical
since you work with an existing relation F, and then determine
whether its functional.

So instead of first building map(D,R) and then checking
whether F in map(D,R). You simple examine F, in
a particular way.

[Kuniaki Mukai]

> On May 19, 2018, at 8:05, j4n bur53 <janb...@xlog.ch> wrote:
>
> Well you wrote "I have tested a ROZDD processing which constructs
> a large function spaces whose domain and range have".
>
> https://groups.google.com/d/msg/swi-prolog/ZQZV2i6TlN4/RmaG8e-0BgAJ
>
> You only showed the data for one function space. What if you
> have multiple function spaces in the same query and combine
> them. Are you still fast. I dunno, and I don't have your code,

No problem with handling plural spaces. It is usual thing.

The following queries have three such spaes.

?- zdd_init, zdd_map([1,2,3],[1,2,3], X), zdd_map([1,2,3],[2,3], Y),
zdd([Z := X-Y]), sets(Z, S), maplist(writeln, S).

>
> so I cannot test it. I also don't have a code that would convert
> map(D;R) to BDD. But I think your original message is misleading
> since it talks about large functions spaces in plural,

I am very open on that as I did with the pack pacm (and variant/2)
I will do so with zdd codes if there is other interested people.

On bottle neck is to prepare documentation. which is a kind of torture for me,
very much reluctant.

> buit you only showed generating one function space. And you
> did do anything with it. The interesting case would be like
> computing the difference of two function spaces.
>
> So I guess your post is a little cheating, you didn't show a lot.

I thought so far I have posted codes enough for interested
people could easily and fully reconstruct his own codes.

I am far from cheating others. You seem saying something
very bad at this public forum.

Kuniaki Mukai

[Kuniaki Mukai]

> On May 19, 2018, at 8:10, j4n bur53 <janb...@xlog.ch> wrote:
>
> English would be: map(D,R) = a function space
> No need to write "spaces", just "space".
>
> https://en.wikipedia.org/wiki/Function_space
>
> But "spaces" would be the interesting thing. Or
> what are you planning to do with map(D,R)?

Yes. In fact I posted map(D,R) as an initial variety, which is
intended to be a generalization of the truth set. I am far from
sure on this analogy from math (algebraic geometry). It is a truly experimental.

I regret to post such not mature idea. Do not ask me any more endlessly.

Kuniaki Mukai

[j4n bur53]

Here is a fundep checker like in the paper. But without craig
interpolation. Instead it uses the following:

- CLP(X) schema of programming, to get multiple
   copies of the same SAT problem
- call/n, for the same reason, to get multiple
   copies of the same SAT problem

So the truth table is given as a predicate fun_n in CLP(X)
programming. And a predicate test(fun_n) then tests whether
the last column is functionally dependent on the first column.

Here is the test data:

fun1: The last column is not functionally dependent on the first column

?- fun1(A,B,C), labeling([A,B,C]), write(A-B-C), nl, fail; true.
0-1-0
1-0-0
1-1-0
0-0-1
Yes

fun2: The last column is not functionally dependent on the first column

?- fun2(A,B,C), labeling([A,B,C]), write(A-B-C), nl, fail; true.
1-0-0
1-1-0
0-0-1
0-1-1
Yes

Here are the test results:

fun1: Missing Functional Dependency Confirmed

?- test(fun1).
No

fun2: Existing Functional Dependency Confirmed

?- test(fun2).
Yes

I guess you can use this for deep learning. Ha Ha.
The code is very simple, I have uploaded it to gist.
It should be self explanatory with the preceeding paper.

https://gist.github.com/jburse/3e081f01c7de5c725e8b94e4e8f14e76#file-fundep-p

But just for the record this is the code:

:- use_module(library(finite/clpb)).

fun1(A,B,C) :- sat(C=:=(~A)*(~B)).

fun2(A,_,C) :- sat(C=:=(~A)).

test(F) :-
   call(F,A,B,0),
   call(F,A,C,1),
   labeling([A,B,C]), !, fail.
test(_).

[j4n bur53]

Corr.: Typo
fun2: The last column is functionally dependent on the first column

[j4n bur53]

For a picture see here:
https://gist.github.com/jburse/3e081f01c7de5c725e8b94e4e8f14e76#gistcomment-2593965

[Kuniaki Mukai]

Hi, 

I am trying to put qlf files for the ROZDD constructor of mine at

http://web.sfc.keio.ac.jp/~mukai/zdd.zip

There are some troubles in  making  all qlf files to work for others, which 

is not fixed yet. However,  with such a couple of modules separated,  main functions   seems

run as expected.

I appreciate if someone let me know what happens after trying  to download it and  run on 

the latest SWI-Prolog devel. 

Here is some Instructions.

- download the zip file from 

http://web.sfc.keio.ac.jp/~mukai/zdd.zip

- unzip it.

- cd  to the directory.

% swipl

Welcome to SWI-Prolog (threaded, 64 bits,

version 7.7.14-12-g589d58c79)

         ^^^^^^^^^

?- [zdd].

true.

?- module(zdd).

true.

zdd:  ?- solve([X:=[[a,b],[c,d]]]), sets(X, R).

X = 5,

R = [[c, d], [a, b]].

Kuniaki Mukai

[j4n bur53]

Ok we are waiting. ..
Tokio (or Tokyo) 2020 isn't that far away...

Am Samstag, 19. Mai 2018 01:42:11 UTC+2 schrieb Kuniaki Mukai:

[Kuniaki Mukai]

Hi Fernando,

Thank you  for noticing.   I will prepare soon a minimum  document for interested people 

to do ROZDD programming in SWI-Prolog.  I myself am  now enjoying 

with N-queen puzzle in ROZDD.

Kuniaki Mukai

On May 20, 2018, at 0:28, Fernando Sáenz Pérez <fsaen...@gmail.com> wrote:

Hi Kuniaki,

In Windows 10 64 bit it seems to work:

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

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

Please run ?- license. for legal details.

For online help and background, visit http://www.swi-prolog.org

For built-in help, use ?- help(Topic). or ?- apropos(Word).

?- cd('c:/tmp/zdd').

true.

?- [zdd].

true.

?- module(zdd).

true.

zdd:  ?- solve([X:=[[a,b],[c,d]]]), sets(X, R).

X = 5,

R = [[c, d], [a, b]].

zdd:  ?- 

All the best,

Fernando

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

[j4n bur53]

Thats a little strange module that provides some zdd
functionality, doesnt make any sense. Usually one
would simply only do:

?- use_module(zdd).

?- solve([X:=[[a,b],[c,d]]]), sets(X, R).
X = 5,

R = [[c, d], [a, b]].

Why consult via [ ] and why module? Module is not a
top-level test of some sort, it creates a new module or
enters an existing module in SWI-Prolog.

If you want to wrap your zdd library
in a module and deliver as such, you just
 need to begin your module, in your file zdd.pl with:

:- module(zdd, [solve/1,
                sets/2]).

Then the two predicates solve/1 and sets/2
will be exported and visible in the
module that does the use_module/1.

P.S.: Further remarks, why use_module
and not [ ] consult? Because use_module usually
has an additional check, namely that the file

is really a module and not an ordinary text.
This is specified here. Namely you can read
the following:

"This predicate is equivalent to ensure_loaded/1,
except that it raises an error if Files are not module files. "
http://www.swi-prolog.org/pldoc/man?predicate=use_module/1

Here is what happens if a file is loaded that
is not empty and that doesnt start with a module/2
directive, as promised you get an error:

?- use_module('/Users/janburse/Desktop/zddfake').

ERROR: /Users/janburse/Desktop/zddfake.pl:2:

Domain error: `module_file' expected, found `'/Users/janburse/Desktop/zddfake.pl''

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

[j4n bur53]

For example here, I see an empty export list:
http://www.swi-prolog.org/pack/file_details/pac/prolog/misc/bdd.pl?show=src

But you can add to the export list:
- predicate indicators,  i.e. name/arity
- operators, i.e. op(level, mode, name)

So that in the end you don't need to enter the module
on the toplevel in normal use mode.

How operators are exported, you see for example here,
in Markus Triskas library:

:- module(clpb, [
                    op(300, fy, ~),
                    op(500, yfx, #),
                    sat/1,
                    taut/2,
                    labeling/1,
                    sat_count/2,
                    weighted_maximum/3,
                    random_labeling/2
                 ]).

http://www.swi-prolog.org/pldoc/doc/_SWI_/library/clp/clpb.pl?show=src

[Kuniaki Mukai]

Thanks.

That is  is a mistake of mine,    On developing a module  I use ?- [<the module>] for 

“reconsulting”  because I often experienced  the  use_module directive 

does not reconsult the updated module, though  I did not try to 

find a reason for it.  Maybe I was missing something.

[Kuniaki Mukai]

Here is a time statistics for the popular  N-queens puzzle in ROZDD of mine.

Is this  somehow meaningful for SWI-Prolog ? I am not sure for it; 

One might see related aweful results on the net.

?- time(n_queens(8, C)).

 % 138,761 inferences, 0.016 CPU in 0.016 seconds (96% CPU, 8844477 Lips)

 C = 92.

?- time(n_queens(10, C)).

 % 2,202,839 inferences, 0.246 CPU in 0.253 seconds (97% CPU, 8951537 Lips)

 C = 724.

?- time(n_queens(11, C)).

 % 10,368,042 inferences, 1.209 CPU in 1.233 seconds (98% CPU, 8572618 Lips)

 C = 2680.

?- time(n_queens(12, C)).

 % 55,254,091 inferences, 7.011 CPU in 7.172 seconds (98% CPU, 7880751 Lips)

 C = 14200.

?- time(n_queens(13, C)).

 % 321,029,259 inferences, 41.645 CPU in 42.286 seconds (98% CPU, 7708707 Lips)

 C = 73712.

% N-queens source.

n_queens(N, Count):- n_queen_matrix(N, M),

zdd_init,

n_queens(M, [], [], [], S),

card(S, Count).

%

n_queens([], _, _, _, true):-!.

n_queens([C|R], Po, Ne, Ho, U):-

n_queens(C, R, Po, Ne, Ho, U).

%

n_queens([], _, _, _, _, false).

n_queens([_I-J|D], R, Po, Ne, Ho, U):- memberchk(J, Ho), !,

n_queens(D, R, Po, Ne, Ho, U).

n_queens([I-J|D], R, Po, Ne, Ho, U):- K is I+J, L is I-J,

( check_safe(K, L, Po, Ne)

-> n_queens(R, [K|Po], [L|Ne], [J|Ho], V),

insert_atom(K-L, V, V0),

n_queens(D, R, Po, Ne, Ho, U0),

zdd([join(V0, U0, U)])

;   n_queens(D, R, Po, Ne, Ho, U)

).

%

n_queen_matrix(N, M):- N0 is N-1,

findall(C,

 ( between(0, N0, I),

findall(I-J, between(0, N0, J), C)

 ),

M).

%

check_safe(K, L, Po, Ne):-

( (memberchk(K, Po); memberchk(L, Ne))

-> false

; true

).

Kuniaki Mukai

[Kuniaki Mukai]

I have made a comparison of the N-queens between versions of the usual list processing  and the ROZDD.

They make big differences at  N = 13,  N = 14. 

For N = 14,  ROZDD version takes about one hundred seconds,  on the other hand the usual version

is still running now since  one hour passed.  I have to  force it to quit soon.

Kuniaki Mukai

[Kuniaki Mukai]

The comparison was not exact.  An exact difference  is this:

**** ROZDD version ****

?- time(n_queens(13, C)).

 % 321,029,259 inferences, 41.470 CPU in 42.141 seconds (98% CPU, 7741236 Lips)

 C = 73712.

?- time(n_queens(14, C)).

 % 1,859,442,502 inferences, 258.919 CPU in 261.993 seconds (99% CPU, 7181547 Lips)

 C = 365596.

**** Usual version ****

?- time(usual_n_queens(13, C)).

 % 221,871,892 inferences, 131.416 CPU in 131.688 seconds (100% CPU, 1688314 Lips)

 C = 73712.

?- time(usual_n_queens(14, C)).

 % 1,365,891,482 inferences, 2748.561 CPU in 2757.472 seconds (100% CPU, 496948 Lips)

 C = 365596.

Kuniaki Mukai

[j4n bur53]

There is something wrong with your "usual" queen. I
am now testing on a very slow machine of mine (an
old Mac laptop), and I get:

?- time((search([1,2,3,4,5,6,7,8,9,10,11,12,13], [], _), fail)).
% Up 53,383 ms, GC 379 ms, Thread Cpu 51,941 ms (Current 05/20/18 11:13:47)
No

But this is without counting. How do you count in the
usual solution? Using this trick doesn't make it any slower:

?- time((findall(hit,search([1,2,3,4,5,6,7,8,9,10,11,12,13], [], _),L), 
length(L,N), write(N), nl, fail)).
73712
% Up 50,160 ms, GC 431 ms, Thread Cpu 49,149 ms (Current 05/20/18 11:19:01)
No

Usual code is:

http://www.jekejeke.ch/idatab/doclet/prod/en/docs/15_min/15_stdy/06_bench/09_programs/03_queens/01_queens.p.html

In the old times I was comparing it to CLP(FD), CLP(FD) was slower:

http://www.jekejeke.ch/idatab/doclet/prod/en/docs/15_min/15_stdy/06_bench/09_programs/03_queens/02_queens3.p.html

Unfortunately this part of my web site is not maintained. I
have not yet a CLP(FD) benchmark. Maybe I should start a
CLP(B) benchmark. That CLP(FD) was slower so far
is seen here:

CLP(FD) slower for 8-queens:

?- time((queens3(_), fail;true)).
% Up 308 ms, GC 2 ms, Thread Cpu 301 ms (Current 05/20/18 11:26:37)
Yes

Traditional faster for 8-queens:

?- time((queens(_), fail;true)).
% Up 24 ms, GC 0 ms, Thread Cpu 23 ms (Current 05/20/18 11:10:30)
Yes

[Kuniaki Mukai]

On May 20, 2018, at 18:28, j4n bur53 <janb...@xlog.ch> wrote:

There is something wrong with your "usual" queen. I
am now testing on a very slow machine of mine (an
old Mac laptop), and I get:

“Usual” means non ROZDD version, which is obtained easily  by modifying 

the ROZDD version posted, quite easy.  So I have to say it is your codes that is wrong 

not mine.

Kuniaki Mukai

[Kuniaki Mukai]

I forgot to attach codes:

usual_n_queens(N, Count):- n_queen_matrix(N, M),

usual_n_queens(M, [], [], [], S),

length(S, Count).

%

usual_n_queens([], _, _, _, [[]]).

usual_n_queens([C|R], Po, Ne, Ho, U):-

usual_n_queens(C, R, Po, Ne, Ho, U).

%

usual_n_queens([], _, _, _, _, []).

usual_n_queens([_I-J|D], R, Po, Ne, Ho, U):- memberchk(J, Ho), !,

usual_n_queens(D, R, Po, Ne, Ho, U).

usual_n_queens([I-J|D], R, Po, Ne, Ho, U):- K is I+J, L is I-J,

( check_safe(K, L, Po, Ne)

-> usual_n_queens(R, [K|Po], [L|Ne], [J|Ho], V),

maplist(cons(K-L), V, V0),

usual_n_queens(D, R, Po, Ne, Ho, U0),

union(V0, U0, U)

;   usual_n_queens(D, R, Po, Ne, Ho, U)

).

On May 20, 2018, at 18:28, j4n bur53 <janb...@xlog.ch> wrote:

[j4n bur53]

Thats not the usual backtracking solution. Its an algebraic
solution that uses union. Why do you use union

and not simply append? Backtracking would also not
look back, doesn't make any sense.

[j4n bur53]

Also using maplist/3 to build the solution, is by far

not the usual backtracking solution.

The Prolog interpreter in backtracking builds the
soluton by using the Prolog logical variables.

Your code is interestig, since it shows what your
are up to. For example it shows that your ZDD
queens, is not a ZDD queens, since you do not
let ZDD search the solution. Instead your CLP(X)

scheme of programming does the search already,
thats why your ZDD and non-ZDD code are
so similar. But somehow this all makes no sense,
since you dont use labeling/1 search. There is

not really a model setup phase and then a model
solving phase. The model is already the solution.
If you want to solve all problems this way, you
remain in usual Prolog programming, where there

is less declarativity. Your solution is very procedural.

[j4n bur53]

Your solution is procedural since you mistake ZDD as
a datatructure for union and length. But ZDD or
a SAT Solver schould deliver a little more intelligence
and declarative programming.

[Kuniaki Mukai]

I have found the “usual" codes usual_n_queens/2 with union replaced with append

is faster than ROZDD version  n_queens/2  at both N= 13 and 14. As I believe 

that the replacement is safe, this is  a little bit strange.

Kuniaki Mukai

[Kuniaki Mukai]

On May 20, 2018, at 19:13, j4n bur53 <janb...@xlog.ch> wrote:

Your solution is procedural since you mistake ZDD as
a datatructure for union and length. But ZDD or
a SAT Solver schould deliver a little more intelligence
and declarative programming.

Could you show us such an  intelligent  solution to  N-queens in your sense ?

Kuniaki Mukai

[j4n bur53]

Not yet. Its increasingly difficult if your code needs to compete
to a backtracking solution in Prolog. Because Prolog is
especially made for backtracking.

You can only compete if you have really some intelligence
in your code. This happens in CLP(FD) usually, since some
Euclid GCD (number theory) is applied and you can fail early

on some constraints. But its much more difficult for CLP(B). I
made a CLP(FD) to CLP(B) translator. You find it here, it
translates a small fragment of CLP(FD):

CLP(FD) to CLP(B) translator.
https://gist.github.com/jburse/3e081f01c7de5c725e8b94e4e8f14e76#file-finsat-p

I was then using it to run the 8-queens problem:

8-queens using CLP(FD) to CLP(B) translator
https://gist.github.com/jburse/3e081f01c7de5c725e8b94e4e8f14e76#file-queens4-p

To run the code I had only to replace this line:

:- use_module(library(finite/clpfd)).

By ths line:

:- use_module(library(finite/clpb)).

:- use_module(library(mukai/finsat)).

The results shows nothing. I will later today also try the SWI-
Prolog CLP(B) solver. But the way I have coded the problem
and the way my CLP(B) solver performs, everything is fine, the

solution is correct, except no special performance:

% ?- queens3(X), term_variables(X,L), labeling(L).
% X = [[0,0,0,1],[0,1,0,1],[1,0,0,0],[0,1,1,0],[0,0,1,1],[0,1,1,1],[0,0,1,0],[0,1,0,0]],
% L = [0,0,0,1,0,1,0,1,1,0,0,0,0,1,1,0,0,0,1,1,0,1,1,1,0,0,1,0,0,1,0,0] ;
% X = [[0,0,0,1],[0,1,1,0],[1,0,0,0],[0,0,1,1],[0,1,1,1],[0,1,0,0],[0,0,1,0],[0,1,0,1]],
% L = [0,0,0,1,0,1,1,0,1,0,0,0,0,0,1,1,0,1,1,1,0,1,0,0,0,0,1,0,0,1,0,1]

% ?- time((queens3(X), term_variables(X,L), sat_count(L,N), write(N), nl, fail)).
% 92
% % Up 1,453 ms, GC 21 ms, Thread Cpu 1,438 ms (Current 05/20/18 14:01:40)
% No

Compare this with the traditional backtracking solution:

% ?- queens(X).
% X = [1,5,8,6,3,7,2,4] ;
% X = [1,6,8,3,7,4,2,5]

% ?- time((findall(hit,queens(_),L), length(L,N), write(N), nl, fail)).
% 92
% Up 18 ms, GC 0 ms, Thread Cpu 15 ms (Current 05/20/18 14:06:14)
% No

I don't know why the CLP(B) solution gives exactly the same
initial enumeration of solution. Maybe this is accidential,
since my CLP(B) has not yet some reordering during labeling.

Intelligent labeling with automatic variable reordering is
one way of making CLP(B) faster (you find easily literature
about it). I did not yet implement it. Anyway, lets see later

today what SWI-Prolog Markus Triskas solver can do
with the example. His sat_count/2 could be faster, since
like the labeling/1 my sat_count/2 is also still very

unintelligent. His sat_count/2 might be better.

[j4n bur53]

I already made some experiments with reordering. But
for the orthonormal example, it made the example only
slower. But this was based on an earlier version of my CLP(B).

Maybe I should repeat the experiments, with automatic
reordering. The challenge is to make the reordering really
dynamic, that is not only do some ordering before

labeling/1 goes to work, but all the time during the
solving process. I have such an algorithm in my CLP(FD)
solver, but for the CLP(B) solver, the problem is that

the number of variables is much higher, so this
"replanning" gets much more expensive. So I don't
do it yet. I am waiting for an idea to make this "replanning"

more faster. A faster labeling would then also imply
a faster sat_count in my case, because I could this
continous "replanning" also apply to the counting....

[Kuniaki Mukai]

On May 20, 2018, at 20:07, Kuniaki Mukai <kuniak...@gmail.com> wrote:

I have found the “usual" codes usual_n_queens/2 with union replaced with append

is faster than ROZDD version  n_queens/2  at both N= 13 and 14. As I believe 

that the replacement is safe, this is  a little bit strange.

Perhaps, a solution is searched only once because of “attack-condition check”, which makes 

structure sharing is  rare in N-queens problem. This is my intuition but with no proof.

Any idea ?

[j4n bur53]

What do you add by maplist/3? I guess you make disjoint
solutions, so you can use append instead union.

[Kuniaki Mukai]

On May 20, 2018, at 21:30, j4n bur53 <janb...@xlog.ch> wrote:

What do you add by maplist/3? I guess you make disjoint
solutions, so you can use append instead union.

 So,  ROZDD data structure may not have merit  as for N-queens problem.

Kuniaki Mukai

[j4n bur53]

I didn't test some data structure. I tested a solver, labeling/1
and sat_count/2. I cannot tell you anything about a data structure,
for a solving problem. Solving has more aspects...

[j4n bur53]

When working with particular problem instances, the solver
should really appear as a black box. So that different solvers
can easily use different data structures and different solving

techniques. What was really fun today, and what I borrowed
from Picat, that I could easily turn my CLP(FD) queens
problem into a CLP(B) queens problem by replacing this line:

:- use_module(library(finite/clpfd)).

By ths line:

:- use_module(library(finite/clpb)).

:- use_module(library(mukai/finsat)).

The module finsat is a CLP(FD) to CLP(B) translator. What is
now missing is a better solving technique for my CLP(B) itself,
and maybe a different translation.

Picat had an intesting paper recently about all this:

Optimizing SAT Encodings for Arithmetic Constraints
Neng-Fa Zhou1 and H akan Kjellerstrand - 2017
http://www.picat-lang.org/papers/cp17.pdf

So the library is a first stride towards this direction, the code is open source:

CLP(FD) to CLP(B) translator.
https://gist.github.com/jburse/3e081f01c7de5c725e8b94e4e8f14e76#file-finsat-p

Maybe you have different plans for ROZDD. My plans are
more around the idea to make CLP(B) a black box, that I
can improve inpendent from some given problems,

I want to use the same code, even if my CLP(B) solver gets
better. Something that helps mere here is CLP(X) scheme
of programming. But now the CLP(FD) to CLP(B) translation

is also a neat tool I guess.

[Kuniaki Mukai]

Summary:

The usual_n_queens/2 codes  is twice faster than ROZDD version at N =14

?- time(usual_n_queens(14, C)).

% 1,360,773,124 inferences, 173.802 CPU in 174.265 seconds (100% CPU, 7829454 Lips)

C = 365596 .

This result was accidentally obtained via ROZDD version against what I had expected.

Kuniaki Mukai

[j4n bur53]

Maybe work on other examples, like magic square 8,
where more can happen in solver and its data structures
magic square 8 is in the PicatSAT paper mentioned.

[Kuniaki Mukai]

Hi j4n,

Skimming the Picat paper, I feel I understand what your are interested, 

though this thread is far from that.  

Really I wish you keep going towards goals of your resarch 

and developing plan   you have  outlined.

Kuniaki Mukai

[j4n bur53]

I don't know whether the paper talks a lot about variable
ordering, and how labeling/1 and sat_count/2 could be
improved. Thats more what I am interested in.

The paper doesn't say much about SAT Solving itself,
since they anyway delegate it to Lingeling.

But I can give you a simple proof of concept, that ordering
matters. You can try it also with your ZDD. Its very simple,
I just do 8-queen in two different ways:

% place inner queens first
% queens3a(-List)
queens3a(X) :-
   X = [A,B,C,D,E,F,G,H],
   [C,D,E,F] ins 1..8,
   [A,B,G,H] ins 1..8,
   noattack_list(X),
   all_different(X).

% place outer queens first
% queens3b(-List)
queens3b(X) :-
   X = [A,B,C,D,E,F,G,H],
   [A,B,G,H] ins 1..8,
   [C,D,E,F] ins 1..8,
   noattack_list(X),
   all_different(X).

Here are the results, the static ordering of outer
queens first is slower, than inner queens first.
See for yourself:

/* inner queens first is faster */
?- time((queens3a(X), term_variables(X, V), sat_count(V, N), write(N), nl, fail)).
92
% Up 1,347 ms, GC 16 ms, Thread Cpu 1,344 ms (Current 05/20/18 20:29:13)
No

/* outer queens first is slower */

?- time((queens3b(X), term_variables(X, V), 
   sat_count(V, N), write(N), nl, fail)).
92
% Up 2,349 ms, GC 24 ms, Thread Cpu 2,328 ms (Current 05/20/18 20:29:05)
No

But a good labeling predicate would have some topological
heuristics, which would choose the order of variables
not only statically, but also dynamically during solving,

and thus find a better ordering without any hints from
the end-user. Thats a kind of intelligence that needs to
be put in a CLP(B) solver, and that is already found

in my CLP(FD) solver.

[j4n bur53]

The topological reason that the strategy inner queens
first is better is very simple. Inner queens do bar more
squares than outer queens.

You can count the stars, lets make a 4x4 Example:

Outer Queen                   Inner Queen
+----+            +----+
|Q***|            |.***|
|**..|            |**Q*|
|*.*.|            |.***|
|*..*|            |*.*.|
+----+            +----+

Outer Queen: 9 barred squares
Inner Queen: 11 barred squares

[j4n bur53]

You can measure such things by analysing the sat/1
constraints, especially how the attribute variables
are assigned.

An attribute variable that points to a lot of sat/1
constraints is like an inner queen. An attribute variable
that points only to a few of sat/1 constraints,

is like an outer queen. Its not very difficult to code
then some heuristics that chooses inner queen
variables first during labeling.

But I am struggeling with making it highly dynamic.
I want to "replan" constantly the ordering of
the variables. Not sure whether this is possible...

[j4n bur53]

I guess you can even use the Prolog builtin keysort/2
for that. Although in the case of CLP(FD) I didn't do it

like that. But anyway, just to give you a picture what
can be done, to put intelligence into a CLP(B) solver.

[Kuniaki Mukai]

I said I would prepare soon a minimum “document" for the ROZDD constructor zdd.pl
Below it is. It is just a hash-array handler. Fibonnchi and N-queens sample codes
indicates the handler is fast enough to playing around. Rehash was added by Jan’s suggestion.

It would be is a miracle that someone could make a codes. The doc
is only for patient reader.

%% Hash and Array
zdd_init : initialize hash and array.
zdd_memo(X, V): memorize X with association V.
zdd_dump: dump the array.
zdd_max(I): I is the current number of intermidiate nodes in the array.


%%%
zdd(As): interprete a series As of a rozdd constructing commands.

-- zdd commands --
meet(U, V, R) : R is the intersection of U and V.
join(U, V, R) : R is the union of U and V.
subtr(U, V, R) : R is the subtraction of U and V.
neg(X, Y): Y is the complement of X.
K <- IF: IF is the cofact of K.
V := E : eval E to V.
quotient(X, I, J, Y): Y is the quotient of X w.r.t the unifiction I =J.
dim(Dim): the current dimension.
singleton(X, Y): Y is the singleton of X.
intern(X, Y): Y is the internal of X.
root(X): X is the current root.
input(X, Y): convert X into the primitive form Y.
{G}: call(G)

%%
cofact(X, Y): X is the internal index for a ROZDD Y.
sat(X) : solve X in SAT mode.
fos(X) : solve X in FOS mode.
card(C) : C is the cardinality of the root.

%%
zdd_quotient(X, Y) : the root is updated by X=Y.
solc(Form, C): C is the count of solutions of Form.
varnum(D): D is the current numbers of boolean basics.
sets(X, P): P is the set of sets in a ROZDD X.
intern(X, Y): Y is the internal form of X.
extern(X, Y): Y is the external form of X.
solve(As): interprete a series AS of rozdd constructing commands.

%%
zdd_count_nodes(X, C): C is the number of intermediate_nodes of X.
zdd_singleton(X, P): P is the singleton of X.
zdd_merge(X, Y, Z): Z is the merge of X and Y.
zdd_unify(X, I=J, Y): Y is the quotient of X induced by I = J.
zdd_unify(X, Eqs, Y): Y is the quotient of X induced by a union-find Eqs.

Kuniaki Mukai

[Kuniaki Mukai]

I forgot an important primitive insert_atom/3.

insert_atom(X, A, Y):  insert atom to each set of X, that is, conceptually, 

if X = {As1,...,Asn} then Y = {[A|As1], [A|As2],...[A|Asn]}.

The meaning of every operation on ROZDD is conceptually simple like this. 

IMO, ROZDD is conceptually very  simple in nature. 

Kuniaki Mukai

[Kuniaki Mukai]

I have found that  zdd.pl  misses an operation which removes a specified atom from a zdd.

Here a naive version  is.

remove_atom(_, true, true):-!.

remove_atom(_, false, false):-!.

remove_atom(A, I, J):- cofact(I, if(X, L, R)),

( A @< X  -> cofact(J, if(A, I, false))

;   A @> X  -> remove_atom(A, L, L0),

 remove_atom(A, R, R0),

 cofact(J, if(X, L0, R0))

; zdd_join(L, R, J)

).

% ?- solve([X:=[[a,b,c], [u,b,v], [x,y]]]), remove_atom(b, X, Y), sets(Y, S).

%@ S = [[x, y], [u, v], [a, c]].

A more sophisticated version is necessary considering to apply 

it to SAT,  which should be  also easy.

I do not intend to continue this kind of thread endlessly.  

Although I thinks the current zdd.pl  is still a toy anyway,

as the current zdd.pl got stable,  I feel it is  time for me to step further, 

in my own way as so far, but in silent mode.    

SAT on ROZZD, top down breadth-first construction of ROZDD,  etc.

There are so many branches, and for now  I am not sure which I will take to go.

Kuniaki Mukai

[Kuniaki Mukai]

I have written a Prolog codes on rules of DPLL algorithm for SAT.

- one literal rule, unit rule

- pure literal rule, affirmative-nagative rule

- splitting rule, rule of case analysis

- subsumption rule

- cleanup rule

Through this experiement, I used ZDD structure not only for representing CNF

(conjunctive normal form), but also use ZDD as building pieces for large CNFs,

such large ones that I could not succeed to construct with the usual naive list

processing because of its not serious structure sharing, I guess.

I have no idea on applying this codes for now. 

Kuniaki Mukai

[Kuniaki Mukai]

I have enjoyed another mini ZDD programming exercise:

converting a cnj (conjunctive normal form)

to an equivalent dnf(disjunctive normal form).

A solution is cnf_to_dnf/2 below.  I have not tested,

but I am sure it works correctly, because I expect

ZDD programming should allow us to do such a simple recursion 

programming like familiar Prolog list precessing, 

otherwise I would not be interested in ZDD.

% ?- solve_cnf((a+ b)*(-a + b), X),

% cnf_to_dnf(X, Y), sets(X, Sx), sets(Y, Sy).

%@ X = 6,

%@ Y = 9,

%@ Sx = [[-a, b], [a, b]],

%@ Sy = [[b], [-a, b], [a, b]] .

cnf_to_dnf(true, false):-!.

cnf_to_dnf(false, true):-!.

cnf_to_dnf(X, Y):- zdd_memo(dnf(X), Y),  % For not calculating twice.

( nonvar(Y) -> true

; cofact(X, if(A, L, R)),

cnf_to_dnf(L, L0),

cnf_to_dnf(R, R0),

insert_literal(A, R0, U),

sat_merge(L0, R0, V),

sat_join(U, V, Y)

).

Kuniaki Mukai