Lion and Unicorn with Prolog SAT Solver

Example
1

@kuniaki.mukai posted a Prolog SAT solver solution to
the Lion and Unicorn riddle. Can this be further improved:

% ?- time(solve_lion_uncorn_puzzle_in_dnf(Ans)).
%@ % 8,188,821 inferences, 0.626 CPU in 0.647 seconds
(97% CPU, 13085762 Lips)
%@ Ans = today(thu) ;
%@ % 171 inferences, 0.004 CPU in 0.004 seconds (100% CPU, 47017 Lips)
%@ false.

A SAT solver is a computer program which aims to
solve the Boolean satisfiability problem. Using Boolean
modelling I only got that far:

yesterday(0,0,0,1,1,0).
yesterday(0,0,1,0,0,0).
yesterday(0,1,0,0,0,1).
yesterday(0,1,1,0,1,0).
yesterday(1,0,0,0,1,1).
yesterday(1,0,1,1,0,0).
yesterday(1,1,0,1,0,1).

lying_day(0,0,0,1).
lying_day(0,0,1,0).
lying_day(0,0,1,1).
lying_day(1,1,0,0).
lying_day(1,1,0,1).
lying_day(1,1,1,0).

solve_for(T1,T2,T3) :- yesterday(T1,T2,T3,Y1,Y2,Y3)
, contrary(lying_day(0,T1,T2,T3), lying_day(0,Y1,Y2,Y3))
, contrary(lying_day(1,T1,T2,T3), lying_day(1,Y1,Y2,Y3)).

contrary(S,T) :- \+ S, T.
contrary(S,T) :- S, \+ T.

And then:

?- time(solve_for(T1,T2,T3)).
% 32 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
T1 = 1,
T2 = T3, T3 = 0 ;
% 17 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
false.

What now, how to use a SAT Solver?

2

Ok, I was using a SAT solver in a little unorthodox way.
Used it as a compiler for a formula, so that I got:

yesterday(0,0,0,1,1,0).
yesterday(0,0,1,0,0,0).
yesterday(0,1,0,0,0,1).
yesterday(0,1,1,0,1,0).
yesterday(1,0,0,0,1,1).
yesterday(1,0,1,1,0,0).
yesterday(1,1,0,1,0,1).

two_liars(T1,T2,T3,Y1,Y2,Y3) :-
   T1=\=Y1,
   T1=:=(T1/\Y2) xor (T1/\Y3) xor (Y2/\Y3),
   Y1=:=(T2/\T3) xor (T2/\Y1) xor (T3/\Y1),
   T1=\=(T1/\T2) xor (T1/\T3) xor T2 xor (T2/\T3) xor T3,
   Y1=\=(Y1/\Y2) xor (Y1/\Y3) xor Y2 xor (Y2/\Y3) xor Y3.

solve_for(T1,T2,T3) :-
   yesterday(T1,T2,T3,Y1,Y2,Y3),
   two_liars(T1,T2,T3,Y1,Y2,Y3).

Works fine and is fast with optimise=true:

/* SWI-Prolog 9.1.17, optimise=false */
?- time(solve_for(T1,T2,T3)).
% 16 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
T1 = 1,
T2 = T3, T3 = 0 ;
% 10 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
false.

/* SWI-Prolog 9.1.17, optimise=true */
?- time((between(1, 1000000, _), solve_for(T1,T2,T3), fail; true)).
% 9,999,999 inferences, 1.203 CPU in 1.199 seconds
(100% CPU, 8311687 Lips)

Edit 14.11.2023
So how to use a SAT solver as a compiler. First model the problem
with library(clpb) as Boolean formulas.

lying_day(A, B, C, D, M) :- M = (
   ~A* ~B* ~C*D+
   ~A* ~B*C* ~D+
   ~A* ~B*C*D+
   A*B* ~C* ~D+
   A*B* ~C*D+
   A*B*C* ~D).

two_liars(T1, T2, T3, Y1, Y2, Y3, ((M1#M2)*(M3#M4))) :-
    lying_day(0, T1, T2, T3, M1),
    lying_day(0, Y1, Y2, Y3, M2),
    lying_day(1, T1, T2, T3, M3),
    lying_day(1, Y1, Y2, Y3, M4).

Then look at the normalform:

?- two_liars(T1,T2,T3,Y1,Y2,Y3,M), sat(M).
sat(1#T2*T3#T2*Y1#T3*Y1#Y1),
sat(T1=:=T1*Y2#T1*Y3#Y2*Y3),
sat(T1=\=Y1),
sat(T1=\=T1*T2#T1*T3#T2#T2*T3#T3),
sat(Y1=\=Y1*Y2#Y1*Y3#Y2#Y2*Y3#Y3).

Take the normalform, reorder the equations a little bit, fewer
variables first, and rewrite them into ISO core standard bitwise
operations, and then take profit.

3

I am busy on revising codes for DNF/CNF converter based on ZDD. They are still enough dirty or confused for me to remember details. However I hope it will drastically be improved in a week. I will upgrade package pac with it.

IMHO, SAT solving is to get DNF as normal form of the input formula. Therefore computational complexity must be high, perhaps NP-complete, though I am not sure on this. So I am not interested in efficiency of my approach, but in conceptual clearness.

For now I can only show an example below, where psa is
to show current dnf as normal form of SAT solving.

Sorry for not able to discussing about what you might want, which
might be too difficult for me to catch up with.

% ?- sat(a=:=b), psa, sat(b=:=c),psa, sat(c=:=d), psa.
%@  zid = 8
%@ 	[-a,-b]
%@ 	[a,b]
%@ -------------------
%@  zid = 16
%@ 	[-a,-b,-c]
%@ 	[a,b,c]
%@ -------------------
%@  zid = 26
%@ 	[-a,-b,-c,-d]
%@ 	[a,b,c,d]
%@ -------------------
%@ true.
4

Yeah, I wonder what the CNF would be of this:

sat(1#T2*T3#T2*Y1#T3*Y1#Y1),
sat(T1=:=T1*Y2#T1*Y3#Y2*Y3),
sat(T1=\=Y1),
sat(T1=\=T1*T2#T1*T3#T2#T2*T3#T3),
sat(Y1=\=Y1*Y2#Y1*Y3#Y2#Y2*Y3#Y3).

What Markus Triska shows is kind of a Boolean ring polynomial
M but factorized into M = M1*…*Mn, and then you have multiple
constraints and not a single constraint. Nice!

If you produce a CNF, actually a product sum form, you would
get also something of the form M = M1’*…*Mn’. Are these
M1’,…,Mn’ faster than the M1,…,Mn from

Markus Triskas library(clpb), when running the example?

Edit 14.11.2023
Whats also giving some speed, is introducing extra variables?
Tried this with SWI-Prolog:

two_liars(T1,T2,T3,Y1,Y2,Y3) :-
   T1=\=Y1,
   H is (Y2/\Y3),
   T1=:=(T1/\Y2) xor (T1/\Y3) xor H,
   J is (T2/\T3),
   Y1=:=J xor (T2/\Y1) xor (T3/\Y1),
   T1=\=(T1/\T2) xor (T1/\T3) xor T2 xor J xor T3,
   Y1=\=(Y1/\Y2) xor (Y1/\Y3) xor Y2 xor H xor Y3.

New benchmark results:

/* SWI-Prolog 9.1.17, optimise=true */
?- time((between(1, 1000000, _), solve_for(T1,T2,T3), fail; true)).
% 9,999,999 inferences, 1.203 CPU in 1.204 seconds (100% CPU, 8311687 Lips)
true.

No speed up, possibly the additional temporary variables
are too expensive? Or the goals with the extra variable
are not enough often reached to amortisize?

5

Here is only query log for that as it is. ‘true’ is for 1.
I need time for understanding other parts of your posts.
I hope you could reproduce the query like this.

?- use_module(library(pac)).  % version 1.8.3
?- module(pac).
pac:  ?- use_module(zdd(zdd)).
?-  time((sat(.....
query result 
% ?- time((sat(true#T2*T3#T2*Y1#T3*Y1#Y1), psa,
%	sat(T1=:=T1*Y2#T1*Y3#Y2*Y3), psa,
%	sat(T1=\=Y1), psa,
%	sat(T1=\=T1*T2#T1*T3#T2#T2*T3#T3), psa,
%	sat(Y1=\=Y1*Y2#Y1*Y3#Y2#Y2*Y3#Y3), psa)). 
%@  zid = 56
%@ 	[-B,-C]
%@ 	[-A,-C]
%@ 	[-A,-B,-C]
%@ 	[-A,B,C]
%@ 	[A,-B,C]
%@ 	[A,B,C]
%@ -------------------
%@  zid = 126
%@ 	[-B,-C,-D,-F]
%@ 	[-B,-C,-D,-E]
%@ 	[-B,-C,D,-E,F]
%@ 	[-B,-C,D,E,-F]
%@ 	[-B,-C,D,E,F]
%@ 	[-A,-C,-D,-F]
%@ 	[-A,-C,-D,-E]
%@ 	[-A,-C,D,-E,F]
%@ 	[-A,-C,D,E,-F]
%@ 	[-A,-C,D,E,F]
%@ 	[-A,-B,-C,-D,-F]
%@ 	[-A,-B,-C,-D,-E]
%@ 	[-A,-B,-C,D,-E,F]
%@ 	[-A,-B,-C,D,E,-F]
%@ 	[-A,-B,-C,D,E,F]
%@ 	[-A,B,C,-D,-F]
%@ 	[-A,B,C,-D,-E]
%@ 	[-A,B,C,D,-E,F]
%@ 	[-A,B,C,D,E,-F]
%@ 	[-A,B,C,D,E,F]
%@ 	[A,-B,C,-D,-F]
%@ 	[A,-B,C,-D,-E]
%@ 	[A,-B,C,D,-E,F]
%@ 	[A,-B,C,D,E,-F]
%@ 	[A,-B,C,D,E,F]
%@ 	[A,B,C,-D,-F]
%@ 	[A,B,C,-D,-E]
%@ 	[A,B,C,D,-E,F]
%@ 	[A,B,C,D,E,-F]
%@ 	[A,B,C,D,E,F]
%@ -------------------
%@  zid = 174
%@ 	[-B,-C,D,-E,F]
%@ 	[-B,-C,D,E,-F]
%@ 	[-B,-C,D,E,F]
%@ 	[-A,-C,D,-E,F]
%@ 	[-A,-C,D,E,-F]
%@ 	[-A,-C,D,E,F]
%@ 	[-A,-B,-C,D,-E,F]
%@ 	[-A,-B,-C,D,E,-F]
%@ 	[-A,-B,-C,D,E,F]
%@ 	[-A,B,C,-D,-F]
%@ 	[-A,B,C,-D,-E]
%@ 	[A,-B,C,-D,-F]
%@ 	[A,-B,C,-D,-E]
%@ 	[A,B,C,-D,-F]
%@ 	[A,B,C,-D,-E]
%@ -------------------
%@  zid = 336
%@ 	[-A,-B,-C,D,-E,F]
%@ 	[-A,-B,-C,D,E,-F]
%@ 	[-A,-B,-C,D,E,F]
%@ 	[-A,B,-C,D,-E,F]
%@ 	[-A,B,-C,D,E,-F]
%@ 	[-A,B,-C,D,E,F]
%@ 	[-A,B,C,-D,-F]
%@ 	[-A,B,C,-D,-E]
%@ 	[A,-B,-C,D,-E,F]
%@ 	[A,-B,-C,D,E,-F]
%@ 	[A,-B,-C,D,E,F]
%@ 	[A,-B,C,-D,-F]
%@ 	[A,-B,C,-D,-E]
%@ 	[A,B,C,-D,-F]
%@ 	[A,B,C,-D,-E]
%@ -------------------
%@  zid = 424
%@ 	[-A,-B,-C,D,-E,F]
%@ 	[-A,-B,-C,D,E,-F]
%@ 	[-A,-B,-C,D,E,F]
%@ 	[-A,B,-C,D,-E,F]
%@ 	[-A,B,-C,D,E,-F]
%@ 	[-A,B,-C,D,E,F]
%@ 	[-A,B,C,-D,-E,-F]
%@ 	[-A,B,C,-D,-E,F]
%@ 	[-A,B,C,-D,E,-F]
%@ 	[A,-B,-C,D,-E,F]
%@ 	[A,-B,-C,D,E,-F]
%@ 	[A,-B,-C,D,E,F]
%@ 	[A,-B,C,-D,-E,-F]
%@ 	[A,-B,C,-D,-E,F]
%@ 	[A,-B,C,-D,E,-F]
%@ 	[A,B,C,-D,-E,-F]
%@ 	[A,B,C,-D,-E,F]
%@ 	[A,B,C,-D,E,-F]
%@ -------------------
%@ % 63,375 inferences, 0.005 CPU in 0.007 seconds (72% CPU, 12708041 Lips)
%@ T2 = A,
%@ T3 = B,
%@ Y1 = C,
%@ T1 = D,
%@ Y2 = E,
%@ Y3 = F.
6

In Markus Triskas library(clpb) the (#)/2 is XOR.

Its quite easy, I have only run the contrary part of solve_for/3
through a SAT solver and not yesterday/6. And then I used the
SAT solver as a compiler and replaced the contrary part.

To run it through a SAT solver this here:

two_liars(T1, T2, T3, Y1, Y2, Y3) :-
    contrary(lying_day(0,T1,T2,T3), lying_day(0,Y1,Y2,Y3))
   , contrary(lying_day(1,T1,T2,T3), lying_day(1,Y1,Y2,Y3)).

Became this here, returning a formula with XOR in the 7-th argument:

two_liars(T1, T2, T3, Y1, Y2, Y3, ((M1#M2)*(M3#M4))) :-
    lying_day(0, T1, T2, T3, M1),
    lying_day(0, Y1, Y2, Y3, M2),
    lying_day(1, T1, T2, T3, M3),
    lying_day(1, Y1, Y2, Y3, M4).

The CNF seems to be much longer than the algebraic normal form,
Introduced by the Russian mathematician Ivan Ivanovich Zhegalkin
in 1927. No wonder the two liars is quite an XOR statement.

But I don’t have a paper right now at hand, that shows the further
factoring as in the result of Markus Triska, even don’t know whether
this is rather by accident or whether this is done more systematic?

7

It seems that the requested formula is tautology, though
I have tested based on my guess. Perhaps it is not relevant to what you might expected. I hope the current zdd library might be enough
for one to test such things for oneself.

% ?- F1 = (true#T2*T3#T2*Y1#T3*Y1#Y1),
% F2 = (T1=:=T1*Y2#T1*Y3#Y2*Y3),
% F3 = (T1=\=Y1),
% F4 = (T1=\=T1*T2#T1*T3#T2#T2*T3#T3),
% F5 = (Y1=\=Y1*Y2#Y1*Y3#Y2#Y2*Y3#Y3),
% time((ltr_zdd  X<< cnf(-(F1+F2+F3+F4+F5)))).
%@ % 38,038 inferences, 0.004 CPU in 0.005 seconds (65% CPU, 10699859 Lips)
%@ F1 = #(..),
%@ T2 = A,
%@ T3 = B,
%@ Y1 = C,
%@ F2 = #(..),
%@ T1 = D,
%@ Y2 = E,
%@ Y3 = F,
%@ F3 = (D=\=C),
%@ F4 = #(..),
%@ F5 = #(..),
%@ X = 1.
8

There is a bug somewhere in your reasoning or how
you enter the formula or how you use your system to
check for tautology. The binary encoding is:

T1 T2 T3 weekday
0 0 0 sunday
0 0 1 monday
0 1 0 tuesday
0 1 1 wednesday
1 0 0 thursday
1 0 1 friday
1 1 0 saturday

Its obviously not a tautology. For example sunday / saturday
doesn’t satisfy the formula, refuting that it would be a tautology.
You can try yourself.

?- two_liars(0,0,0,1,1,0).
false.

The only yesterday pair that satisfies the formula,
is thursday / wednesday, namely this here:

?- two_liars(1,0,0,0,1,1).
true.

Or using the solve_for/2 predicate which combines two_liars/6
with yesterday/6, we find, like in the 1986 paper:

̀?- solve_for(T1,T2,T3).
T1 = 1,
T2 = T3, T3 = 0 ;
false.
9

Do you mean that F1+F2+F3+F4+F5 is not tautology ?
where

	F1 = (true#T2*T3#T2*Y1#T3*Y1#Y1),
	F2 = (T1=:=T1*Y2#T1*Y3#Y2*Y3),
	F3 = (T1=\=Y1),
	F4 = (T1=\=T1*T2#T1*T3#T2#T2*T3#T3),
	F5 = (Y1=\=Y1*Y2#Y1*Y3#Y2#Y2*Y3#Y3).

If not tautology, I must take time (later) to see what happened.

11

Internally, disjunction AND( comma) disjunction
is converted to disjunction incremental way. SAT keeps
the DNF all the time as its normal form.

13

If one of your questions which I can answer was what is the DNF of (-F1)* (-F2) * (-F3) * (-F4) * (-F5) ?,
where

F1 = (true#T2*T3#T2*Y1#T3*Y1#Y1),
F2 = (T1=:=T1*Y2#T1*Y3#Y2*Y3),
F3 = (T1=\=Y1),
F4 = (T1=\=T1*T2#T1*T3#T2#T2*T3#T3),
F5 = (Y1=\=Y1*Y2#Y1*Y3#Y2#Y2*Y3#Y3).

The answer by my dnf is

%	 ( ltr_zdd X<< dnf((-F1)* (-F2) * (-F3) * (-F4) * (-F5)), psa(X)).
%@  zid = 0
%@ 	0
%@ -------------------

which means that is “FALSE” (unsatisfible).

14

Seems you are totally off topic and not talking about the two Liars
from the riddle, namely this here what Alice in the forest hears
from the animals:

Lion: Yesterday was one of my lying days.
Unicorn: Yesterday was one of my lying days.

Thats why my predicate is called two_liars/6. First liar is Lion,
the second liar is Unicorn, in total we have two liars.

There is a bug somewhere in your reasoning or how you enter
the formula or how you use your system to check for antinomy.
Since you make a quite far off claim.

But the riddle gives a hint that it is satisfiable. Even uniquely
satisfiable, since the riddle says:

From these statements, Alice, who was a bright girl, was able to
deduce the day of the week. What was it?

You can also verify satisfiable via my Prolog code:

Or via library(clpb) by using the predicate which has this documentation:

labeling(+Vs)
Assigns truth values to the variables Vs such that all constraints are satisfied.

So if I use this SAT solver predicate I also find that it is satisfiable:

image
image810×402 68.1 KB

15

No. I am talking about propositional formula you gave. On the other hand, satisfiability of the puzzle was already shown by my SAT solver with my formulation of the puzzle in propositional logic, which I was satisfied enough not to have interest in other solutions. I need time to digest your idea.

16

You are using the wrong formula then. My formula is:

sat(1#T2*T3#T2*Y1#T3*Y1#Y1),
sat(T1=:=T1*Y2#T1*Y3#Y2*Y3),
sat(T1=\=Y1),
sat(T1=\=T1*T2#T1*T3#T2#T2*T3#T3),
sat(Y1=\=Y1*Y2#Y1*Y3#Y2#Y2*Y3#Y3)

Which is the same as, i.e. conjunction. I already explained
at length that it is a conjunction, but you didn’t listen!

sat((1#T2*T3#T2*Y1#T3*Y1#Y1)
*(T1=:=T1*Y2#T1*Y3#Y2*Y3)
*(T1=\=Y1)
*(T1=\=T1*T2#T1*T3#T2#T2*T3#T3)
*(Y1=\=Y1*Y2#Y1*Y3#Y2#Y2*Y3#Y3)).

Which is neither a tautology, i.e. always true, nor an antinomy,
i.e. always false. You can use this predicate from the documentation
to check that it is neither a tautology nor an antinomy:

taut(+Expr, -T)
If Expr is a tautology with respect to the posted constraints,
succeeds with T = 1. If Expr cannot be satisfied,
succeeds with T = 0. Otherwise, it fails.

I get this result, its neither a tautology nor an antinomy:

image

17

Sorry for that. I will check later when I come back home. I am taking coffee at a feed corner.

19

Aster inserting parens by guess base, the test result is
as you said.

% ?- F =
%    (T1=\=Y1) *
%    ( T1=:=(T1*Y2) xor (T1*Y3) xor (Y2*Y3)) *
%    ( Y1=:=(T2*T3) xor (T2*Y1) xor (T3*Y1)) *
%    ( T1=\=(T1*T2) xor (T1*T3) xor T2 xor (T2*T3) xor T3) *
%    ( Y1=\=(Y1*Y2) xor (Y1*Y3) xor Y2 xor (Y2*Y3) xor Y3), 
%	( ltr_zdd X<<dnf(F), psa(X), ltr_card(X, C)).
%@  zid = 491
%@ 	[-A,B,-C,-D,-E,F]
%@ 	[-A,B,-C,-D,E,-F]
%@ 	[-A,B,-C,-D,E,F]
%@ 	[-A,B,-C,D,-E,F]
%@ 	[-A,B,-C,D,E,-F]
%@ 	[-A,B,-C,D,E,F]
%@ 	[-A,B,C,-D,-E,F]
%@ 	[-A,B,C,-D,E,-F]
%@ 	[-A,B,C,-D,E,F]
%@ 	[A,-B,-C,D,-E,-F]
%@ 	[A,-B,-C,D,-E,F]
%@ 	[A,-B,-C,D,E,-F]
%@ 	[A,-B,C,-D,-E,-F]
%@ 	[A,-B,C,-D,-E,F]
%@ 	[A,-B,C,-D,E,-F]
%@ 	[A,-B,C,D,-E,-F]
%@ 	[A,-B,C,D,-E,F]
%@ 	[A,-B,C,D,E,-F]
%@ -------------------
%@ F = (A=\=B)*(A=:=A*C xor (A*D)xor(C*D))*(B=:=E*F xor (E*B)xor(F*B))*(A=\=A*E xor (A*F)xor E xor (E*F)xor F)*(B=\=B*C xor (B*D)xor C xor (C*D)xor D),
%@ T1 = A,
%@ Y1 = B,
%@ Y2 = C,
%@ Y3 = D,
%@ T2 = E,
%@ T3 = F,
%@ X = 491,
%@ C = 18.


% ?- F =
%    (T1=\=Y1) *
%    ( T1=:=(T1*Y2) xor (T1*Y3) xor (Y2*Y3)) *
%    ( Y1=:=(T2*T3) xor (T2*Y1) xor (T3*Y1)) *
%    ( T1=\=(T1*T2) xor (T1*T3) xor T2 xor (T2*T3) xor T3) *
%    ( Y1=\=(Y1*Y2) xor (Y1*Y3) xor Y2 xor (Y2*Y3) xor Y3),
%	 prove(F).
%@ INVALID
%@ F = (T1=\=Y1)*(T1=:=T1*Y2 xor (T1*Y3)xor(Y2*Y3))*(Y1=:=T2*T3 xor (T2*Y1)xor(T3*Y1))*(T1=\=T1*T2 xor (T1*T3)xor T2 xor (T2*T3)xor T3)*(Y1=\=Y1*Y2 xor (Y1*Y3)xor Y2 xor (Y2*Y3)xor Y3).
23

It is not suprising that my DNF/CNF based on ZDD have drawbacks. However I noticed several merits of it due to high structure sharing caused by ZDD. Let me explain one of them.

Suppose 1, 2, 3, 4 ,… are propositional atoms,
and define p(1) = (1 + -1). (- for negation).
p(2) = (1 + 2)*(1 + -2)*(-1 + 2)*(-1 + -2)
etc.

Clearly p(n) is a CNF and unsatisfiable. So refutation must be successful.

I tested this CNF p(n) on my prover.

% ?- N=2, numlist(1, N, Ns), time((	(ltr_zdd P << ltr_pow(Ns), psa(P), resolve(P)))).
%@  zid = 11
%@ 	[- 1,- 2]
%@ 	[- 1,2]
%@ 	[1,- 2]
%@ 	[1,2]
%@ -------------------
%@ % 1,177 inferences, 0.000 CPU in 0.000 seconds (86% CPU, 7133333 Lips)
%@ N = 2,
%@ Ns = [1, 2],
%@ P = 11.

It was surprising to see that it passed even for n=2000; the CNF has 2^2000 clauses.

% ?- N=2000, numlist(1, N, Ns), time((	(ltr_zdd P << ltr_pow(Ns), resolve(P)))).
%@ % 1,285,503,224 inferences, 124.254 CPU in 133.949 seconds (93% CPU, 10345745 Lips)
%@ N = 2000,
%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
%@ P = 13997.

IMHO, this shows a merit of DNF/CNF based on ZDD.
One could reproduce this experiment on the package pac 1.8.3

25

I have no idea to answer your request at least for now,
perhaps because of drawbacks of my DNS/CNS which you pointed. Now my codes is simple and straightforward, I hope, and all codes are accessible in zdd.pl under package library(pac). I wish smart someone could answer your request, and that my codes would be useful for that purpose.

29

Of course I agree on this. On this occasion, I will add
XOR (排他的論理和 in Japanese) as a basic operation on families of sets.

BTW, I am wondering if I happened to write already the code as for handling polynomials on GF(2) without noticing that it is the XOR. I will check it later.

EDIT
XOR as operation on families of sets was quite easy, and performance seems not bad.

% ?- numlist(0, 1000, Ns), numlist(500, 1500, Ms),
%	time((zdd X<<pow(Ns), Y<<pow(Ms), Z<<zdd_xor(X, Y))).
%@ % 318,806 inferences, 0.024 CPU in 0.025 seconds (93% CPU, 13524201 Lips)
%@ Ns = [0, 1, 2, 3, 4, 5, 6, 7, 8|...],
%@ Ms = [500, 501, 502, 503, 504, 505, 506, 507, 508|...],
%@ X = 1002,
%@ Y = 2003,
%@ Z = 4004.

zdd_xor(X, Y, Z, S):-zdd_subtr(X, Y, A, S),
	zdd_subtr(Y, X, B, S),
	zdd_join(A, B, Z, S).

EDIT2

I have checked that zdd_join/4 for ZDD
and gf2_join/4 for polynomials over GF(2) are almost
the same only except X+X = X for ZDD, X+X=0 for GF(2). Perhaps I noticed at that time, and I forgot soon later.

31

3 posts were split to a new topic: Benchmarking