Thanks. But it seems not related to this thread, at least, directly.
I am having several positive programming experiences on ZDD over the boolean ring (=GF(2)). For example, the codes gf2_sat_count count the solutions of this
a + b*c + d*e*f = 0
( I am not sure 32 is correct, which my codes just said). I am new to GF(2)
algorithm which have to take care of, e.g, x*x=1 and x+x=0, in fact, I had hard time on this (and still). In addition, I have seen that the standard order (compare/3) used in my ZDD is simply lexical total ordering which satisfies necessary condition for Groebner basis calculus. As such, I have written several basic operations, to get head term of ZDD as polynomials, polynomial residue calculus, the critical Spoly operation on GF(2) in ZDD (not lists).
I hope I could get other results on this worth to post here.
% ?- zdd((even_odd_power([1-1, 2-2, 3-3], X, Y), gf2_sat_count([Y-1], 0, C))).
%@ X = 10,
%@ Y = 9,
%@ C = 32.
%
gf2_sat_count(X, Y, Z):- shift(gf2_sat_count(X, Y, Z)).
%
gf2_sat_count([], U, U, _):-!.
gf2_sat_count([P-C|As], U, V, S):- gf2_sat_count(P, C, As, U, V, S).
%
gf2_sat_count(1, C, As, U, V, S):-!, U0 is U + C,
gf2_sat_count(As, U0, V, S).
gf2_sat_count(0, _, As, U, V, S):-!, gf2_sat_count(As, U, V, S).
gf2_sat_count(P, C, As, U, V, S):- cofact(P, t(_-J, L, R), S),
C0 is C * (2^J-1),
gf2_sat_count(R, C0, [L-C|As], U, V, S).
% ?- zdd((even_odd_power([1,2,3], X, Y), Z<<pow([1,2,3]),
% zdd_join(X, Y, Z))).
even_odd_power(X, Y, Z):- shift(even_odd_power(X, Y, Z)).
%
even_odd_power([], 1, 0, _).
even_odd_power([X|Xs], Ev, Od, S):-
even_odd_power(Xs, Ev0, Od0, S),
zdd_insert(X, Ev0, X_Od, S),
zdd_insert(X, Od0, X_Ev, S),
zdd_join(X_Od, Od0, Od, S),
zdd_join(X_Ev, Ev0, Ev, S).
% ?- time(sat_count(- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( -(-(A1)) =:= A2) =:= A3) =:= A4) =:= A5) =:= A6) =:= A7) =:= A8) =:= A9) =:= A10) =:= A11) =:= A12) =:= A13) =:= A14) =:= A15) =:= A16) =:= A17) =:= A18) =:= A19) =:= A20) =:= ( A20 =:= ( A19 =:= ( A18 =:= ( A17 =:= ( A16 =:= ( A15 =:= ( A14 =:= ( A13 =:= ( A12 =:= ( A11 =:= ( A10 =:= ( A9 =:= ( A8 =:= ( A7 =:= ( A6 =:= ( A5 =:= ( A4 =:= ( A3 =:= ( A2 =:= A1) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), C)).
%@ % 276,118,742 inferences, 21.475 CPU in 21.494 seconds (100% CPU, 12857516 Lips)
%@ C = 0.
Sounds great !
Have you tried the sequent calculus LK for that ? Expanding the tree without CUT rule,
all leaves must be axiom of the LK, using weakening. The start sequent is, in the case, A \vdash (with empty right hand side).
EDIT.
p.s.
Watching the formula again, for any number of variables, the unsatisfiability of such formula seems obvious, by simple mathematical induction.
EDIT (additional)
Now blazingly fast ! (by ad hoc but often used prolog-like preprocessing).
% ?- test_formula1(X), time(sat_count(X, C)).
%@ % 4,751 inferences, 0.001 CPU in 0.001 seconds (99% CPU, 5435927 Lips)
%@ X = - (((((((((... =:= ...)=:=a14)=:=a15)=:=a16)=:=a17)=:=a18)=:=a19)=:=a20)=:=(a20=:=(a19=:=(a18=:=(a17=:=(a16=:=(a15=:=(a14=:=(... =:= ...))))))))),
%@ C = 0.
test_formula1(-(( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( -(-( a1 =:= a2)) =:= a3) =:= a4) =:= a5) =:= a6) =:= a7) =:= a8) =:= a9) =:= a10) =:= a11) =:= a12) =:= a13) =:= a14) =:= a15) =:= a16) =:= a17) =:= a18) =:= a19) =:= a20) =:= ( a20 =:= ( a19 =:= ( a18 =:= ( a17 =:= ( a16 =:= ( a15 =:= ( a14 =:= ( a13 =:= ( a12 =:= ( a11 =:= ( a10 =:= ( a9 =:= ( a8 =:= ( a7 =:= ( a6 =:= ( a5 =:= ( a4 =:= ( a3 =:= ( a2 =:= a1) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))).
I am slightly confused; is reading the code not an option for some reason? I found the full source code of the library in the official SWI-Prolog source code repo.
While looking for this I also found a repository with a “ZDD-based variant of library(clpb)”.
I see you have been tackling hard problems. So do not take my comment seriously. In fact, I posted it as almost joking because it is far beyond my reach.
The preprocess is follows. Main idea is to apply the idempotent law for AND and OR.
To wide chances to idempotent law, it sorts AND/OR parts as lists. They are typical Prolog-like programming technique. I wrote it as joking to surprise a reader, but he was not surprised.
% ?- simple_boole((c=:=b)=:=a, X).
simple_boole(X, Y):- boole_rule(X, X0), !,
simple_boole(X0, Y).
simple_boole(X, X).
boole_rule(X, Y):-boole_AND(X, Y).
boole_rule(X, Y):-boole_OR(X, Y).
boole_rule(X, Y):-boole_IMPLY(X, Y).
boole_rule(X, Y):-boole_EQ(X, Y).
boole_rule(X, Y):-boole_NOT(X, Y).
%
boole_NOT(-(-X), X).
boole_NOT(-(1), 0).
boole_NOT(-(0), 1).
boole_NOT(-(X), -(Y)):-boole_rule(X, Y).
%
boole_AND(X*X, X).
boole_AND(0*_, 0).
boole_AND(_*0, 0).
boole_AND(1*X, X).
boole_AND(X*1, X).
boole_AND((X*Y)*Z, X*(Y*Z)).
boole_AND(X*Y, Y*X):-Y@<X.
boole_AND(X*(Y*Z), (Y*(X*Z))):-Y@<X.
boole_AND(X*Y, X0*Y):- boole_rule(X, X0).
boole_AND(X*Y, X*Y0):- boole_rule(Y, Y0).
%
boole_OR(X+X, X).
boole_OR(0+X, X).
boole_OR(X+0, X).
boole_OR(1+_, 1).
boole_OR(_+1, 1).
boole_OR((X+Y)+Z, X+(Y+Z)).
boole_OR(X+Y, Y+X):-Y@<X.
boole_OR(X+(Y+Z), (Y+(X+Z))):-Y@<X.
boole_OR(X+Y, X0+Y):- boole_rule(X, X0).
boole_OR(X+Y, X+Y0):- boole_rule(Y, Y0).
%
boole_EQ(X=:=X, 1).
boole_EQ(X=:=1, X).
boole_EQ(1=:=X, X).
boole_EQ(X=X, 1).
boole_EQ(1=X, X).
boole_EQ(X=1, X).
boole_EQ(X=:=Y, Y=:=X):-Y@<X.
boole_EQ(X=Y, Y=X):-Y@<X.
boole_EQ(X=:=Y, X0=:=Y):- boole_rule(X, X0).
boole_EQ(X=:=Y, X=:=Y0):- boole_rule(Y, Y0).
boole_EQ(X=Y, X0=Y):- boole_rule(X, X0).
boole_EQ(X=Y, X=Y0):- boole_rule(Y, Y0).
%
boole_IMPLY(1->Y, Y).
boole_IMPLY(0->_, 1).
boole_IMPLY(X->Y, X0->Y):- boole_rule(X, X0).
boole_IMPLY(X->Y, X->Y0):- boole_rule(Y, Y0).
Great! For now I am programming Groebner base calculus over the Boolean Ring in ZDD. I am not sure what I am doing, but simply enjoying ZDD programming. Calculating for ab+c=0, ac+d=0 for test, latest prototype codes produces 43 polynomials in total, which I don’t know how to use further. I have to consult the text book on Groebner base. Although I have no idea how to use the Groebner Base for counting solutions, I have observed interesting things on ZDD programming. For example, ZDD programming is a sense, “the blob” programming because it uses unique id on a family of sets, that is, id represents the content. I suspect this is a key of ZDD programming. I would like to talk long on this, but my English won’t allow.
I have received “Encourage everyone to get involved in the conversation” message, which I agree. So I close this thread. Thank you for discussions.
Encourage everyone to get involved in the conversation
Admitting the advice from administrator “Encourage everyone to get involved in the conversation”, I as the starter, have to declare to close this long run thread because no other reader shows interest to this thread, and I have no idea to attract readers. Although your SAT problems are surely important topics, honestly I am not so intersted in the topic, but in ZDD programming in Prolog itself. For example, my recent codes on GF(2)-groebner base calculus in ZDD has a few of interesting features, ZDD as a blob programming, for exampl. It is simple and short, in my feeling. I wrote codes on Groebner base a several years ago under sologan “Poor man’s mathematica” when I didn’t know about setarg/term_hash, which are now two keys of the current ZDD of mine. That old codes were messy and procedural using arrays of two dimension. So I have a plan to compare the two, expanding the current version to polynomials over the real field. It is fifty-fifty, I guess, that I would give here positive post or not. Also there remains a very high wall to clear, “Minato problem.” I am going to be busy on them. I hope patient and a little bit faithful readers there to join me on this, though I know this is always illusion. They are also busy in their own problems.
Thank you for discussions.
Sigh. Anyway thanks a lot for discussions.
I have updated pack pac to pac-1.5.7 from pac-1.5.6. The update includes a lot of small revisions to ZDD library. For example, ZDD state is extended to hold a custom ordering on atoms. The update also includes a prototype codes for path counting of directed graph with source-destination points. I have still a several quesions on ZDD implementation in Prolog particularly around path counting problem. In fact, information on Knuth’s Simpath method is deeply appreciated.
I was asked by a member of this forum how to run queries such as in the ZDD cgi page
http://web.sfc.keio.ac.jp/~mukai/cgitest/zdd-demo.html
The interpreter is new and added to only this update. The following queries are copied from a comment block in the CGI solver source pac/prolog/zdd/zdd-plain.pl. I hope it’s self-explanatory.
% ?- zdd((X<<fos(a), ppoly(X))).
% ?- zdd((X<<fos((a+b)*(a+c)), ppoly(X))).
% ?- zdd((fos((1+b+1+1)*(1+a),X), ppoly(X))).
% ?- zdd((X<<fos((a+b)*(a+c) +(a*b)), ppoly(X))).
% ?- zdd((X<<fos(a*b*c*a*b), ppoly(X))).
% ?- zdd((X<<fos(a*b + c), ppoly(X))).
% ?- zdd((X<<fos((a+b)*(c+d)), ppoly(X))).
% ?- J = 1000, K=1000, numlist(1, J, Nj), numlist(1, K, Nk),
% time(zdd((X<<fos((+Nj) * (+Nk)), card(X, C)))).
% ?- zdd((X<<fos((a+b)\(c+d)), ppoly(X))).
% ?- zdd((X<<fos((a+b)\(a+b)), ppoly(X))).
% ?- zdd((X<<fos((a+b)/a), ppoly(X))).
% ?- zdd((X<<fos((a+b)//a), ppoly(X))).
% ?- zdd((X<<fos((a*c+b)//a), ppoly(X))).
% ?- zdd((X<<fos(pow([a,b])\(c+d)), ppoly(X))).
% ?- zdd((X<<fos(pow([a,b])\(a+b)), ppoly(X))).
% ?- fos([1,2,3]), fos_count.
% ?- fos(pow([1,2]^(2+1))), fos_count(C).
% ?- fos(pow([a,b]^(2+1))), fos_count(C).
% ?- fos(pow((1+1)..(5-3))), fos_count(C).
% ?- fos(pow(atoms(a(1, 3)))), fos_count(C).
% ?- fos(pow(chars(a-c))), fos_count(C).
% ?- fos(pow(chars(a-c))), fos_count(C).
I have noticed that the thread on “Toward ZDD library in SWI-Prolog” is revived. It is coincident that I think it might be time to drop “Toward” for interested readers. To drop it, most difficult problem for me is documentation, aside quality of the library. I have no idea how to do for the moment except polishing source codes for readability as possible as
for the standard criteria for SWI library.
BTW, as prolog is useful for preprocessing and post-processing to send to core task of zdd library, functional notations are supported. There are a few of such support as in the log. I hope it should be clear for the reader.
@ is pragma for the standard prolog atomic goal in the convention of the last argument as output. $ is quote. This notations is interpreted
by zdd_eval/3, which is simplest interpreter, which is in at library(pac/zdd/zdd.pl). Following queries should work with use_module(library(pac)), use_module(zdd(zdd)), module(zdd).
% ?- zdd((X<<pow([a,b,c]), sets(X, P))).
%@ X = 4,
%@ P = [[], [a], [a, b], [a, b, c], [a, c], [b], [b, c], [c]].
% ?- zdd((set_compare(opp_compare), X<<pow([a,b,c]), sets(X, Y))).
%@ X = 4,
%@ Y = [[c, b, a], [c, b], [c, a], [c], [b, a], [b], [a], []].
% ?- zdd((X<<pow([]), sets(X, P))).
% ?- zdd((X<<pow([a]), sets(X, P))).
% ?- zdd((X<<pow(@numlist(1,3)), sets(X, Y))).
% ?- zdd((X<<pow([a,b,c]), sets(X, Y))).
% ?- zdd((X<<pow(@charlist($a, $c)), sets(X, Y))).
% ?- zdd((X<<(pow(@charlist($a, $c)) + pow(@numlist(1, 3))), sets(X, Y))).
I don’t remember well. I will check it later. Thanks…
I have found that my zdd library already has power to find an associative algebra with brute force search on the domain {1,…,10} in about 32 seconds. It is not an answer to what you asked, but I am not far from problem of finding models except naive and brute force search relying on what ZDD has in nature. In fact, the test is restricted version of the existing one to search first model.
% ?- N = 10, numlist(1, N, D),
% time(zdd(?(( mk_algebra(D, A),
% mk_assoc(D, A, B), card(A, C), card(B, E))))).
%@ % 192,468,051 inferences, 32.737 CPU in 32.798 seconds (100% CPU, 5879235 Lips)
%@ N = 10,
%@ D = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
%@ A = 5501,
%@ B = 5600,
%@ C = 10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000,
%@ E = 1.
EDIT.
Here is a non commutative, associative algebra with a left identity
with five elements, which is not impressive very much though.
% ?- N=5, open_state(S), numlist(1, N, D),
% mk_algebra_with_left_unit(D, A, S),
% find_non_commu(2, 3, A, A0, S),
% mk_assoc_first(D, A0, B, S),
% sets(B, [Sets], S), maplist(writeln, Sets).
%@ [1,1]-1
%@ [1,2]-2
%@ [1,3]-3
%@ [1,4]-4
%@ [1,5]-5
%@ [2,1]-5
%@ [2,2]-5
%@ [2,3]-5
%@ [2,4]-5
%@ [2,5]-5
%@ [3,1]-4
%@ [3,2]-4
%@ [3,3]-4
%@ [3,4]-4
%@ [3,5]-4
%@ [4,1]-4
%@ [4,2]-4
%@ [4,3]-4
%@ [4,4]-4
%@ [4,5]-4
%@ [5,1]-5
%@ [5,2]-5
%@ [5,3]-5
%@ [5,4]-5
%@ [5,5]-5
I made the big missing. Thank you you for pointing. The full version returns “no model exists.“ for 3 or 4 elements domain. For 5, it does not terminate.
EDIT.
My brute force codes have finally found a solution after long long run.
% ?- time(find_model(6, B, S)), psa(B, S).
%@ % 896,018,635,494 inferences, 56245.613 CPU in 110023.200 seconds (51% CPU, 15930463 Lips)
%@ zid = 5677
%@ [[1,1]-1,[1,2]-2,[1,3]-3,[1,4]-4,[1,5]-5,[1,6]-6,[2,1]-2,[2,2]-6,[2,3]-5,[2,4]-3,[2,5]-4,[2,6]-1,[3,1]-3,[3,2]-4,[3,3]-1,[3,4]-2,[3,5]-6,[3,6]-5,[4,1]-4,[4,2]-5,[4,3]-6,[4,4]-1,[4,5]-2,[4,6]-3,[5,1]-5,[5,2]-3,[5,3]-2,[5,4]-6,[5,5]-1,[5,6]-4,[6,1]-6,[6,2]-1,[6,3]-4,[6,4]-5,[6,5]-3,[6,6]-2]
%@ B = 5677,
%@ S = ..
BTW, I, human, could find a solution much faster ( in 0.0 second) than the codes using elementary group theory, the permutation group over 3 elements domain, for instance.
Not exactly.
% ?- zdd_sat_count(((a =b)=c)=(a=(b=c)), X).
%@ X = 8.
% ?- zdd_sat_count(((A =B)=C)=(A=(B=C)), X).
%@ X = 8.
In fact, I posted in some thread as structured propositional variable including, Prolog variables. But compound terms with variables are not allowed for simplicity. In fact, my zdd version sat can be used as a prover by counting the number of solutions. I managed to find a way of counting. But it is not interesting to others, I think. I did it only for testing basic operations on ZDD. CLPB is well designed without question.
Is it a question ? Yes. I posted the result. BTW, I got warning that this topic has been solved. And I agree, because now I would like to drop “toward”, as I said.