Lion and Unicorn with Prolog SAT Solver

Example
34

2 posts were merged into an existing topic: Benchmarking

36

How can I display the ZDD normal form for such a zid?
The tree that is behind such a zid? Is there a command in
your ZDD library that allows inspecting the tree?

Thats some bootstrapping, not a basic operation.
Do you have a basic XOR ZDD operation? Does Markus
Triska have a basic XOR ZDD operation?

Edit 11.12.2023
You can derive a basic XOR operation from Minatos OR operation in
Fig 9 in his paper here. Just replace OR by XOR, and you almost
immediately arrive at a basic XOR operation:

Fig 9: Algorithm of the basic operations
https://eprints.lib.hokudai.ac.jp/dspace/bitstream/2115/16895/1/IJSTTT3-2.pdf

Feel free to use mine from recent tree3.p:

% tree3_xor(+Tree, +Tree, -Tree)
tree3_xor(0, B, B) :- !.
tree3_xor(A, 0, A) :- !.
tree3_xor((X->A;B), (X->C;D), R) :- !,
   tree3_xor(A, C, H),
   tree3_xor(B, D, J),
   tree3_make(X, H, J, R).
tree3_xor((X->A;B), N, R) :- (N = (Y->_;_), X @< Y; N = 1), !,
   tree3_xor(B, N, J),
   tree3_make(X, A, J, R).
tree3_xor(N, (Y->C;D), R) :- !,
   tree3_xor(N, D, J),
   tree3_make(Y, C, J, R).
tree3_xor(1, B, R) :- !, R is 1-B.
tree3_xor(A, 1, R) :- !, R is 1-A.