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.