Refutation on extended propositional CNF (experiment)

General
1

In general, refutation for propositional CNF in ZDD is fast. In fact, if input CNF has n atoms (not occurrences), clearly at most n resolutions are enough because of ordering of literals in ZDD representation. One of merits of CNF refutation in ZDD are resolved upon all at once for a couple of bundles which divides all current clauses into two parts.

	{[a,b],[a,c]}, {[-a,d],[-a,e]} => {[b,d], [c,d], [b,e],[c,e]}

Propositional refutation process is similar to left-empty (one-sided) sequent calculus. In fact, if axioms are restricted to sequents of literals, sequent calculus is isomorphic to a refutation process identifyting the one sided sequent with a clause in the obvious way.

  |- A1, A2, ..., An  (one sided sequent)    <==>  [A1, A2, ..., An] (clause)

How about to extend literals to include ->(IMPLY), * (AND), + (Or) terms to CNF, extends ZDD refutation to right-elimination rules for them

      |- A, C   |- B, C           |- -A, B, C
	---------------------- (*)  ------------- (-> variant)
         |- A*B, C                |- A->B, C

Currently propositions in input clauses are assumed in NNF ( negation normal form) for simplicity.I have played around this extension based on prover/1 of mine on the standard CNF. Below is log for small queries. Although this little exercise was interesting for me on ZDD programming in SWI-Prolog, I am far from sure that this extended literals will work well on a big CNF. Anyway I will take a survey on related works on the net later.

% ?- seq_zdd X<<{[a*b*(a->c)*(b->c)], [-c]}, resolve(X).
%@ X = 4.
% ?- seq_zdd X<<{[a*(a->b)], [-b]}, resolve(X).
%@ X = 4.
% ?- seq_zdd X<<{[a], [a->b], [a-> -b], [b]}, resolve(X).
%@ X = 11.
% ?- seq_zdd X<<{[a*b], [a->c], [b->c], [-c]}, resolve(X).
%@ X = 11.
% ?- seq_zdd X<<{[(a->b)->c], [-c]}, resolve(X).
%@ false.
4

I have found a case of a big formula below,
which is too big to be read in as a CNF.
However, the experimental extended CNF prover
can read and solve in a few seconds, though it is ad hoc case.

BTW, I will stop posting on ZDD, or decrease frequency.
Don’t ask me the reason why.

Big formula in CNF 
% ?- formula(1, 3, F).
%@ F = (1==(2==(3==4))).
formula(I, I, I==J):-!,  J is I+1.
formula(I, J, I==P):- K is I + 1, formula(K, J, P).

% ?- conj(1, 3, P).
%@ P = 1*(2*3).
conj(I, I, I):-!.
conj(I, J, I*P):- I0 is I + 1, conj(I0, J, P).

% ?- N = 1000, formula(1, N, _P), K is N + 1, conj(1, N, _Q),
%	time(((seq_zdd X << {[_P*_Q], [-(K)]}, resolve(X)))).
%@ % 46,973,957 inferences, 5.339 CPU in 5.854 seconds (91% CPU, 8797908 Lips)
%@ N = 1000,
%@ K = 1001,
%@ X = 4 .


% ?- N = 100, formula(1, N, _P), K is N + 1, conj(1, N, _Q),
%	call_with_time_limit(60, time(zmod:prove(_P*_Q -> K))).
%@ % 97,712,729 inferences, 46.162 CPU in 61.089 seconds (76% CPU, 2116713 Lips)
%@ ERROR: Unhandled exception: Time limit exceeded