Toward ZDD library in SWI-Prolog (Useful Code)

Useful Code
1

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