 # Toward ZDD library in SWI-Prolog (Useful Code)

Toward ZDD library in SWI-Prolog

Once I posted a codes on a prover for propositional logic using ZDD.
This time I have simplified that codes. At first I was afraid that it looked too simple to be complete, but it seems to work correctly as far as I tested.

``````% valid_formula/1.
valid_formula(-(-a)->a).
valid_formula(a -> a).
valid_formula(a -> (b -> a)).
valid_formula((a->b)->((b->c)->(a->c))).
valid_formula(a->((a->b)->b)).
valid_formula((a*(a->b))->b).
valid_formula((a->b)->(-b -> -a)).
valid_formula((a->b)->((b->c)->(a->c))).

non_valid_formula(a).
non_valid_formula((a->b)->a).
non_valid_formula((a->b)->(b->a)).
non_valid_formula(a -> (b -> c)).
``````

The simplified codes is here.

``````ltr_pow([], 1, _).
ltr_pow([A|As], P, S):- ltr_pow(As, Q, S),
ltr_insert(A, Q, R, S),
ltr_insert(-A, Q, L, S),
ltr_join(L, R, P, S).

% ?- time(forall(valid_formula(A), zdd(prop_neg_refute(A)))).
% ?- time(forall(non_valid_formula(A), zdd(prop_neg_refute(A)))).
prop_neg_refute(Prop):- shift(prop_neg_refute(Prop)).
prop_neg_refute(Prop, S):- cnf(-Prop, X, S),
(	refute(X, S) ->   M = 'VALID'
;	M = 'NON VALID'
),
writeln(M).
``````
``````%
refute(X, S):- zdd_has_1(X, S), !.      % Empty clause found.
refute(X, S):- X > 1,
cofact(X, t(A, L, R), S),
(	A = -(_) -> refute(L, S)		% (e.g. a < -a in ltr_compare.)
;   L > 0,
(	cofact(L, t(B, U, V), S),	% Pure literal rule.
(	B = -(A)
->  ltr_merge(V, R, M, S),  % Resolution.
ltr_join(U, M, W, S),	% Tautology rule.
refute(W, S)
;	refute(L, S)			% Pure literal rule in merging.
)
)
).
``````

In this codes `cofact`, `ltr_join`, `ltr_merge` are all simple basic operations defined in the ZDD library.

The following two sample queries are to see how robust the prover is.
The first one is for a satisfiable set of clauses with 40 variables
the lengh of each clause is 40, and the set has 2^40-1 clauses

``````% ?- N = 40, time((open_state(S), numlist(1, N, L), ltr_pow(L, P, S),
%	zeval(set(L), A, S), zdd_subtr(P, A, Q, S), card(Q, C, S),
%	writeln(C), refute(Q, S))).
%@ 1099511627775
%@ % 616,170,135 inferences, 52.360 CPU in 59.584 seconds (88% CPU, 11767885 Lips)
%@ false.      <==  satisfiable.
``````

The second one is similar, but an unsatisfiable set of clauses with N variables, the lengthh of each clause is N, and the set has 2^N clauses, where N = 100,000 !

``````% ?- N = 100000, time((open_state(S), numlist(1, N, L), ltr_pow(L, P, S),
%	card(P, C, S))), C =:= 2^N, refute(P, S), writeln('Refuted.'), fail; true.
%@ % 32,866,021 inferences, 3.938 CPU in 4.660 seconds (85% CPU, 8346653 Lips)
%@ Refuted.
%@ true.
``````

Although this is artificial, I am afraid that the usual Prolog programming in list processing can compute for the same problem in a day.

1 Like