OK. I see. My understanding the subexpression problem is not sufficient.
The results …, 48, 720, 23040, … are correct. You can look it up here:
Order of orthogonal group O(n, GF(2)).
…, 48, 720, 23040, …
https://oeis.org/A003053
Thanks. I have registered at the site. I will seek appropriate exercises solvable for benchmark.
OK. I will do so. Thanks.
The sequence 1, 2, 6, 48, 720, 23040, … at the site is that of orthogonal group O(n, GF(2)). The Galois filed GF(2) is different from the boolean algebra B. 1+1= 0 in GF(2) but 1+1 =1 in B. Surely, I took the problem as that in the Boolean algebra. In fact, my solutions uses boolean law heavily, including the duality law on + and * in nature. Thus the different sequences of solutions might not be strange. You solved GF(2) problem via the Boolean algebra, which sounds great, I think. I heard of boolean ring, but not of boolean field. So it is a little bit fresh and surprising.
It is highly probable. There are several simplifications on handling sets of clauses of literals based on the duality law, which I am not 100 percent sure. I will check codes, and post the result. Thanks for reviewing my codes. By the way, I took x#y simply as not (x=y), not as Exclusive OR. However after amending it, the result is the same as before. Hmmmmmm, I will borrow your codes at the url posted for further checking.
So, negation operation is not used in the problem. That seems good idea.
Thanks for note on boolean ring.
p.s.
I have noticed that I have to rewrite, at least, boolean macro expansion of my codes.
How many bugs are there in the codes !
I have rewritten drastically codes on expanding macros for boolean expression for ZDD, though
this time, drastically slow.
% ?- time(galois(7, C)).
%@ % 11,791,150,624 inferences, 1841.975 CPU in 1860.820 seconds (99% CPU, 6401364 Lips)
%@ C = 1451520.
It was the first run. This version on O(n, GF(2)) using new macro expansion is very slow as the log says, for which I am disappointed. But that unbelievable time statistics was due to my big mistakes in codes. (galois(7, C) was jburse(7, C) only for now)
I am erroneous. In fact, I made big ones. So this time, I have rewritten macros in a simple way so that less mistakes would happen. This macro definition is supposed to be used in conjunction with ZDD. De Morgan law seems a bottle neck of my use for ZDD, so this macro moves outer negation into inner. So this macro takes care of negation in a special way. (Double negation, for instance).
% ?- make_boole_canonical(a->(b->c), R).
% ?- make_boole_canonical(a=b, R).
% ?- make_boole_canonical(+([a, b]), R).
% ?- make_boole_canonical(-(+([a, b])), R).
% ?- make_boole_canonical(-(*([a, b])), R).
% ?- make_boole_canonical(-(a+b), X).
% ?- make_boole_canonical(-(a+ -b), X).
% ?- make_boole_canonical(-(a = -b), X).
% ?- make_boole_canonical(-(-a = - -b), X).
% ?- make_boole_canonical(-(-(0) = - (-(0))), X).
% ?- make_boole_canonical(-(0), X).
% ?- make_boole_canonical(-(-(0)), X).
% ?- make_boole_canonical(p(1,1), X).
% ?- make_boole_canonical(true, X).
% ?- make_boole_canonical(false, X).
% ?- make_boole_canonical(-false, X).
% ?- make_boole_canonical(-true, X).
% ?- make_boole_canonical(- - -true, X).
% ?- make_boole_canonical(exor(a, b), X).
% ?- make_boole_canonical(nand(a, b), X).
% ?- make_boole_canonical(- nand(a, b), X).
% ?- make_boole_canonical(- #(a, b), X).
make_boole_canonical(X, Y):- make_boole_canonical(X, Y, boole_macro).
%
:- meta_predicate make_boole_canonical(?, ?, :).
%
make_boole_canonical(-(-(X)), Y, Pred):-!,
make_boole_canonical(X, Y, Pred).
make_boole_canonical(-(X), Y, Pred):- make_boole_canonical(X, X0, Pred), !,
( de_morgan(X0, Y) -> true
; Y = -(X0)
).
make_boole_canonical(X, Y, Pred):- default_boole_macro(X, X0),!,
make_boole_canonical(X0, Y, Pred).
make_boole_canonical(X, Y, Pred):- call(Pred, X, X0), !,
make_boole_canonical(X0, Y, Pred).
make_boole_canonical(X, X, _).
%
default_boole_macro(X->Y, -X + Y).
default_boole_macro(X=Y, (X->Y)*(Y->X)).
default_boole_macro(nand(X,Y), -(X*Y)).
default_boole_macro(exor(X,Y), (X + Y) * (-(X * Y))).
%
canonical_boole(X):- integer(X).
canonical_boole(+(_,_)).
canonical_boole(*(_,_)).
canonical_boole(-(_)).
canonical_boole(+(X)):- is_list(X).
canonical_boole(*(X)):- is_list(X).
%
boole_macro(true, 1).
boole_macro(false, 0).
boole_macro(X=:=Y, X=Y).
boole_macro(X ~ Y, X=Y).
boole_macro(X <-> Y, X=Y).
boole_macro(X <=> Y, X=Y).
boole_macro(\/(X,Y), +(X,Y)).
boole_macro(\(X), -(X)).
boole_macro(/\(X, Y), *(X,Y)).
boole_macro((X;Y), +(X,Y)).
boole_macro(X\=Y, -(X=Y)).
boole_macro(\+(X), -(X)).
boole_macro((X,Y), *(X,Y)).
boole_macro(#(X,Y), exor(X,Y)).
boole_macro(equiv(X,Y), X=Y).
boole_macro(imply(X,Y), -(X) + Y).
boole_macro(not(X), -(X)).
boole_macro(and(X,Y), *(X,Y)).
boole_macro(or(X,Y), +(X,Y)).
%
de_morgan(1, 0).
de_morgan(0, 1).
de_morgan(-(X), X). % double negation.
de_morgan(*(X, Y), (-X) + (-Y)). % de Morgan
de_morgan(+(X, Y), (-X) * (-Y)). % de Morgan
de_morgan(*(X), +(Y)):- maplist(negate_macro, X, Y).
de_morgan(+(X), *(Y)):- maplist(negate_macro, X, Y).
%
pred_plus(A, U, A + U).
pred_mul(A, U, A * U).
%
negate_macro(X, -(X)).
Sounds interesting discovery based on your insight of the symmetric property on O(n, qf(2)).
For negation symbol, “~” may be better than arithmetic prefix “-”.
In fact, I took a while for debugging caused by using -0 for -(0), and realized this.
(0 is for the boolean false here.)
?- write_canonical(-0).
0
true.
?- write_canonical(-(0)).
-(0)
true.
?- write_canonical(-a).
-(a)
true.
However, as far as my private use concerned, I prefer - to ~, only because of keyboard typing, but I am flexible on this.
No. I have no idea how to use that idea. I am new on “symmetry breaking.”
Anyway, Congratulation ! It sounds like a kind of breaking-through news.
Here it is.
% ?- time(galois(4, C)).
%@ % 2,084,489 inferences, 0.163 CPU in 0.168 seconds (97% CPU, 12783727 Lips)
%@ C = 48.
% ?- time(galois(5, C)).
%@ % 34,582,341 inferences, 3.758 CPU in 3.815 seconds (99% CPU, 9202632 Lips)
%@ C = 720.
% ?- time(galois(6, C)).
%@ % 583,472,162 inferences, 55.405 CPU in 56.636 seconds (98% CPU, 10531009 Lips)
%@ C = 23040.
pac-1.5.7.tgz is underway. However I have made a lot of revisions to the pac-1.5.6. For instance, more than 10 thousand lines of codes on ZDD has become less than three thousand ones. I have to continue this editing work. More worse, an interesting (new?) idea has come to me on ZDD application, which is difficult for me to put aside. When a prototype of the idea will works, I wish include it the next version as a sample application of the ZDD library. Also I have the “Minato challege problem”, which seems desperately difficult for me for now, but I would like to try it as a test stone of ZDD towards a “SWI-Prolog package”.
With macros untouched, here is the result.
% ?- sat(X+Y), sat_count(C).
%@ C = 3.
% ?- sat(Z*T), sat_count(C).
%@ C = 1.
% ?- sat(X+Y=:=Z*T), sat_count(C).
%@ C = 6.
% ?- sat(X+Y=Z*T), sat_count(C).
%@ C = 6.
I may be missing the point. Anyway, for me, xor is simply a macro like → .
(edit)
I think it is a nice idea of yours to transform the counting the group O(n, GF(2)) into Boolean algebras by the coordinate transformation, which obviously is a bijection (one-to-one onto). So, I must say, what is the problem ? I hope it is not related to the boolean macros of mine, which is no more than macros.
Intersting. I can not verify this at this moment. I might have done a similar but more general thing in the predicate ltr_card, which counts the number solutions of a disjunction normal form (DNF).
ltr_card(N, X, Y):- shift(ltr_card(N, X, Y)).
%
ltr_card(N, X, Y, S):- zdd_shift(ltr_card(N, X, Y, S)).
ltr_card(_, 0, 0, _, _):-!.
ltr_card(N, 1, C, _, _):-!, C is 2^N.
ltr_card(N, X, C, S, M):- memo(path_count(N, X)-C, M),
( nonvar(C) -> true
; cofact(X, t(A, L, R), S),
N0 is N-1,
( L > 1,
positive(A),
cofact(L, t(B, L0, R0), S),
complementary(A, B)
-> ltr_join(R, L0, U, S), % for not counting multple time.
ltr_join(R0, L0, V, S),
ltr_card(N0, U, C_U, S, M),
ltr_card(N0, V, C_V, S, M),
C is C_U + C_V
; ltr_card(N0, L, C_L, S, M),
ltr_card(N0, R, C_R, S, M),
C is C_L + C_R
)
).
(edit)
ltr_card is a yet-another-theorem prover in the sense as follows: A DNF P is a tautology if and only if the number of the DNF of negation of P is 0 (unsatisfiable). I think the root of such power is the lines calling ltr_join. To be honest I checked the codes of ltr_card a couple of time, still I feel some strangeness there. I only have a mental proof for the assertion based on a simple induction on the tree structure of ZDD, but still I am not sure. I have met no counter example so far.
Following a comment that Markus Triska’s interface is now de fact standard, I wrote small predicates sat/1, sat_count/1, sat_count/2 below to see no serious problems as far as unify_hook is not concerned. I have no plan to use unify_hook in the future as for ZDD.
% ?- sat(-(true)).
%@ false.
% ?- sat(-(a + -a)).
%@ false.
% ?- sat(a).
%@ true.
% ?- sat(or(a, b)), sat_count(C).
%@ C = 3.
% ?- sat(xor(a, b)), sat_count(C).
%@ C = 1.
% ?- sat(exor(a, b)), sat_count(C).
%@ C = 2.
% ?- sat(e_x_o_r(a, b)), sat_count(C).
%@ C = 1.
% ?- sat(a), sat(-a).
%@ false.
% ?- sat(a), sat(a+b), sat_count(C).
%@ C = 2.
% ?- sat(a(1)+a(2)), sat_count(C).
%@ C = 3.
% ?- sat(A+a(2)), sat_count(C).
%@ C = 3.
% ?- sat(A + B), sat_count(C).
%@ C = 3.
% ?- sat(a+b+c+d), sat_count(C).
%@ C = 15.
% ?- sat(a+b), sat(c+d), sat_count(C).
%@ C = 9.
% ?-sat(a->b), sat(b->c), sat(c->d), sat(d->a), sat_count(C).
%@ C = 2.
% ?- sat(X=(a=b)), sat(Y=(b+c)), sat(X=Y), sat_count(C).
%@ C = 4.
% ?- sat(X=(a=b)), sat(Y=(b+c)), sat(X=Y), sat(X = (-Y)).
%@ false.
% ?-sat(a->b), sat(b->c), sat(c->d), sat(d->a), sat(-(d = b)).
%@ false.
% ?- E = (a=b)*(b=c)*(c=a), sat(E), sat_count(C).
%@ E = (a=b)*(b=c)*(c=a),
%@ C = 2.
sat(X):-
( nb_current(sat_state, S), S \== [] -> true
; open_state(S0, [extra([root-1, varnum-0, varzip-[]])]),
b_setval(sat_state, S0)
),
b_getval(sat_state, State),
get_key(root, Root, State),
dnf(X, Y, State),
ltr_merge(Y, Root, Root0, State),
set_key(root, Root0, State),
Root0 \== 0.
%
sat_count(C):- b_getval(sat_state, S),
get_key(root, R, S),
get_key(varnum, N, S),
ltr_card(N, R, C, S).
%
sat_count(F, C):- zdd((
dnf(F, X),
get_key(varnum, N),
ltr_card(N, X, C))).
1 Like
Implicitly it is used in ltr_card. Note that ZDD is a suitable in nature for such purpose.
if X and Y have no variable in common, this seems obvious.