What are you talking about ? I have to stop reading.
% ?- ltr_zdd X<< dnf(a*b + c), cofact(X, t(A, L, R)), psa(X).
%@ zid = 6
%@ [c]
%@ [a,b]
%@ -------------------
%@ X = 6,
%@ A = a,
%@ L = 5,
%@ R = 3.
(Nothing of importance)
The codes shows that zdd_find is really based on cofactor representation of DNF.
Let F be a family of sets, and x an atom. Roughly the zdd_find checks if x is a member of the union of the family F. It only assumes the general cofactoring structure of ZDD,
it does not matter even whether it is CNF/DNF, as the name of the predicate suggests. Things are so simple.
% ?- ltr_zdd X<< cnf(a*b + c), psa(X).
%@ zid = 8
%@ [b,c]
%@ [a,c]
%@ -------------------
%@ X = 8.
I mean something else, the same ZDD has two views!
Like for example:
X << a*b+c, psa_dnf(X), psa_cnf(X)
Should show DNF and CNF. Then you can also do:
X << a*b+c, psa_dnf(X), psa_cnf(X), psa_xor(X)
No. But a predicate is (was) prepared as exercise to convert between them. It was interesting to see that the predicate just build all choice functions of family of sets. So duality was observed.
You wrote:
Why not:
[c]
[a,b,-c]
To make the DNF consist of disjoint products?
psa print as it is. it is for ZDD general, not specific for CNF/DNF. psa is PRINT SETs AT a specified family of sets.
Python sympy has all 3, psa_dnf/1, psa_cnf/1 and psa_xor/1:
SymPy 1.2 documentation
The logic module for SymPy allows to form and manipulate
logic expressions using symbolic and Boolean values.
https://docs.sympy.org/latest/modules/logic.html
But I donât know whether there are some flags to control
the outcome, i.e disjoint products or non-disjoint overlapping
producs, etc⌠etc⌠Also they use other names:
- DNF: sum-of-products, SOP
- CNF: product-of-sums, POS
- XOR: algebraic normal form, ANF
Edit 16.11.2023
You wrote:
So it doesnât print a DNF? Well its also a DNF, but not using to the fullest
what a DNF can do, i.e. allow negative literals? Would need another test
case, might produce even more SETs than a DNF has products?
1 Like
CNF/DNF means a set of clauses, a clause is a set of literals.
% ?- ltr_zdd X<< dnf(-(a + b)), psa(X).
%@ zid = 4
%@ [-a,-b]
%@ -------------------
%@ X = 4.
In case XOR might nevertheless land on your todo list.
Well you have still time on your side. No need to hurry with XOR.
For example the online WASM version of Sympy cannot yet do XOR forms:
This is because it has only SymPy 1.11 and not yet SymPy 1.12:
>>> import sympy
>>> sympy.__version
'1.11.1'
With SymPy 1.12 the to_anf() function should be also available.
1 Like
Thanks for sharing! I donât want to âput too much meat on the grillâ, but SymPy looks really an interesting thing 
As I touched, I am reviewing my codes on handling polynomials over GF(2) in ZDD, which is almost parallel to that over Boole for CNF/DNF. I am not sure for now whether it is exactly related to handling XOR in ZDD in the sense of your comment. Currently Iâm recalling how to count the solutions. It was not so easy for me like DNF on boolean.
% ?- zdd gf2_solve_poly((a+b)*(b+c), C, Y), psa(Y).
%@ zid = 24
%@ []
%@ [c]
%@ [b,c]
%@ [a]
%@ [a,b]
%@ [a,b,c]
%@ -------------------
%@ C = 6,
%@ Y = 24.
Tested using your nasty_xor, nasty_or as it is.
For the latter, looks very fast. It is because the input is already close to DNF, I guess.
nasty_xor
% ?- between(10,20,N), nasty_xor(N,X), time(sat(X=:=X)),
% sat_count(C), writeln(C), fail; true.
%@ % 508,831 inferences, 4.203 CPU in 7.638 seconds (55% CPU, 121076 Lips)
%@ 2048
%@ % 616,642 inferences, 0.579 CPU in 1.012 seconds (57% CPU, 1064916 Lips)
%@ 4096
%@ % 785,981 inferences, 0.598 CPU in 1.036 seconds (58% CPU, 1314934 Lips)
%@ 8192
%@ % 1,202,247 inferences, 0.665 CPU in 1.109 seconds (60% CPU, 1806700 Lips)
%@ 16384
%@ % 1,663,658 inferences, 0.730 CPU in 1.187 seconds (62% CPU, 2279527 Lips)
%@ 32768
%@ % 2,477,517 inferences, 0.927 CPU in 1.405 seconds (66% CPU, 2672785 Lips)
%@ 65536
%@ % 4,259,787 inferences, 1.282 CPU in 1.801 seconds (71% CPU, 3321474 Lips)
%@ 131072
%@ % 7,095,802 inferences, 1.968 CPU in 2.571 seconds (77% CPU, 3605222 Lips)
%@ 262144
%@ % 12,583,701 inferences, 3.342 CPU in 4.128 seconds (81% CPU, 3765352 Lips)
%@ 524288
%@ % 23,346,880 inferences, 6.066 CPU in 7.213 seconds (84% CPU, 3849094 Lips)
%@ 1048576
%@ % 45,212,070 inferences, 10.230 CPU in 12.035 seconds (85% CPU, 4419586 Lips)
%@ 2097152
%@ true.
Fast for nasty_or.
nasty_or
% ?- between(10,20,N), nasty_or(N,X), time(sat(X=:=X)),
% sat_count(C), writeln(C), fail; true.
%@ % 36,915 inferences, 0.514 CPU in 0.949 seconds (54% CPU, 71822 Lips)
%@ 2048
%@ % 41,961 inferences, 0.002 CPU in 0.002 seconds (100% CPU, 17133932 Lips)
%@ 4096
%@ % 54,859 inferences, 0.003 CPU in 0.003 seconds (100% CPU, 16101849 Lips)
%@ 8192
%@ % 62,086 inferences, 0.004 CPU in 0.004 seconds (100% CPU, 17395909 Lips)
%@ 16384
%@ % 68,430 inferences, 0.004 CPU in 0.004 seconds (100% CPU, 17636598 Lips)
%@ 32768
%@ % 75,232 inferences, 0.005 CPU in 0.005 seconds (100% CPU, 15875079 Lips)
%@ 65536
%@ % 82,340 inferences, 0.005 CPU in 0.005 seconds (100% CPU, 16477887 Lips)
%@ 131072
%@ % 104,940 inferences, 0.006 CPU in 0.006 seconds (100% CPU, 17385686 Lips)
%@ 262144
%@ % 113,120 inferences, 0.007 CPU in 0.007 seconds (100% CPU, 16977338 Lips)
%@ 524288
%@ % 124,603 inferences, 0.007 CPU in 0.007 seconds (99% CPU, 17308376 Lips)
%@ 1048576
%@ % 133,781 inferences, 0.008 CPU in 0.008 seconds (100% CPU, 16927875 Lips)
%@ 2097152
%@ true.
Well we donât look only at sunshine cases.
Thats not what Alice encounters, both statements are XOR:
Lion: Yesterday was one of my lying days.
Unicorn: Yesterday was one of my lying days.
Your nasty_xor in ZDD is exponential. Time doubles
with each increment. You see this here, from 19 to 20:
%@ % 23,346,880 inferences, 6.066 CPU in 7.213 seconds (84% CPU, 3849094 Lips)
%@ 1048576
%@ % 45,212,070 inferences, 10.230 CPU in 12.035 seconds (85% CPU, 4419586 Lips)
%@ 2097152
First 7 seconds and then 12 seconds. Thats almost a doubling.
Thats the XOR explosion problem, that your ZDD is also subject to.
There are a few SAT solver that donât explode for XOR.
Prolog and the holy grail
As I said at some point, that is far from surprising because it is well known that computational complexity of SAT problem is NP-complete. This means that it might be extremely difficult or impossible to invent a universal way to transform the input form into DNF âefficientlyâ. As such, provided that DNF is used as normal form, it might be useful to allow user defined plugin to transform the input to DNF using known structural property of the input by the user, though I havenât any good example.
DNF/CNF is only one of applications of mine based on ZDD as seen in zdd.pl. There are some other interesting stuff, I hope.
Anyway, programming on ZDD in SWI-Prolog is a hobby of mine. Despite of your rather negative advice, I see some possibility to do ZDD based mass computation in Prolog. For example, refutation for a special cnf with 2^2000 clauses in a few second. One might say,
use ZDD public library in Python. But I would like to enjoy
ZDD programming in SWI-Prolog. Flexible term handling with SWI-Prolog for ZDD input is fun.
No, I didnât say that at all.