Counting solutions for a polynomial over GF(2)

General
, ,
25

(Nothing of importance)

26

Since some point of time, I believe that GF(2) is
exactly the same as the Boolean ring of order 2. So your
comment sounds for me that GF(2) is not extremely useful … . This disappointed me a little, but I have to believe you who are rich of experience as for XOR. Anyway I will keep your comment in mind. Thanks.

28

(Nothing of importance)

29

My sat uses DNF as normal form. So the “nasty” test
rather sounds for me that my sat works efficiently as I expected.

BTW, my dnf/cnf assumes input form is ground.
Prolog variables are converted with numbervars and
atomic propositions are ground prolog terms. I never
think my sat is used as substitute for clpb.

Here is the nasty test in addition with counting.
It also works “efficiently”

% ?- between(10,20,N), nasty(N,X), time(sat(X=:=X)), 
%	sat_count(C), writeln(C), fail; true.
%@ % 274,225 inferences, 1.584 CPU in 2.891 seconds (55% CPU, 173102 Lips)
%@ 2048
%@ % 349,802 inferences, 0.299 CPU in 0.518 seconds (58% CPU, 1168211 Lips)
%@ 4096
%@ % 469,595 inferences, 0.322 CPU in 0.550 seconds (59% CPU, 1459013 Lips)
%@ 8192
%@ % 734,666 inferences, 0.369 CPU in 0.596 seconds (62% CPU, 1988836 Lips)
%@ 16384
%@ % 1,118,548 inferences, 0.461 CPU in 0.700 seconds (66% CPU, 2427178 Lips)
%@ 32768
%@ % 1,822,181 inferences, 0.648 CPU in 0.912 seconds (71% CPU, 2812898 Lips)
%@ 65536
%@ % 3,183,806 inferences, 1.007 CPU in 1.315 seconds (77% CPU, 3161699 Lips)
%@ 131072
%@ % 5,859,967 inferences, 1.732 CPU in 2.127 seconds (81% CPU, 3382993 Lips)
%@ 262144
%@ % 11,280,442 inferences, 2.713 CPU in 3.268 seconds (83% CPU, 4158314 Lips)
%@ 524288
%@ % 21,852,124 inferences, 5.585 CPU in 6.498 seconds (86% CPU, 3912755 Lips)
%@ 1048576
%@ % 42,888,461 inferences, 12.466 CPU in 15.622 seconds (80% CPU, 3440310 Lips)
%@ 2097152
%@ true.
32

Do you have multiply heuristics in your library for ZDD.
Markus Triskas library(clpb) can do it. Here is an example:

foo(_#_#_+_#_#_*_#_).

?- foo(A), foo(B), foo(C), foo(D), time(sat_count(A*B*C*D, X)).
% 30,745 inferences, 0.000 CPU in 0.004 seconds (0% CPU, Infinite Lips)
A = _#_#_+_#_#_*_#_,
B = _#_#_+_#_#_*_#_,
C = _#_#_+_#_#_*_#_,
D = _#_#_+_#_#_*_#_,
X = 268435456.

How do you count such a big number in 4 milliseconds?

Edit 20.11.2023
Here I guess Markus Triska chooses X first and later multiply rule, still fast:

foo(_#_#_+_#X#_*_#_, X).

?- foo(A,X), foo(B,X), foo(C,X), foo(D,X), time(sat_count(A*B*C*D, Y)).
% 43,247 inferences, 0.000 CPU in 0.003 seconds (0% CPU, Infinite Lips)
A = _#_#_+_#X#_*_#_,
B = _#_#_+_#X#_*_#_,
C = _#_#_+_#X#_*_#_,
D = _#_#_+_#X#_*_#_,
Y = 33554432.