 for all r 2 f0; ::; l  1g, count the number of clauses of length j occurring in ' at depth i which have r propositional literals, and append the result to the sub-sublist.
Example 5.1 represents an instance of application of the above technique for construction C and p from '. Notice that the C and p parameters not only verify points (a) and (b) above, but are such that the probability distributions mimic the actual number of occurrences of the different kinds of clauses.

Theorem 6.1 Let rnd CNF2m be a purely random generator as in Figure 13. Let ' *be a sorted* CNF2m formula of depth d and with L *top-level clauses built on all the propositional atoms in* fA1; :::AN g *and on all the modal boxes in* f21; :::2mg, which has no repeated clause at top level and no repeated atoms inside any clause at any level. Let C and p be built from ' so that to verify points (a) and (b) above. Let C0and p0be obtained from C and p *respectively by substituting some* zero-values with some non-zero values. Then we have:
(i) rnd CNF2m(d,m,L,N,p,C) returns ' *with some non-zero probability* P;
(ii) rnd CNF2m(d,m,L,N,p',C') returns ' *with some non-zero probability* P0  P.

Proof The fully-detailed proof is reported in Appendix. Here we sketch the main steps.

The following facts come straightforwardly by induction on the structure of ':

1. every propositional atom occurring in ' at some depth i is returned with the same non-zero probability P1 by both rnd *atom(0,m,N,p,C)* and rnd *atom(0,m,N,p',C')*;
2. every modal atom 2vC l occurring in ' at some depth i is returned with some non-zero probability P2 by rnd *atom(d-i,m,N,p,C)*, and is returned with some non-zero probability P0 2  P2 by rnd *atom(d-i,m,N,p',C')*;
3. every clause C l occurring in ' at some depth i is returned with some non-zero probability P3 by rnd *clause(d-i,m,N,p,C)*, and is returned with some non-zero probability P0 3  P3 by rnd *clause(d-i,m,N,p',C')*.
Thus, every top level clause C lk is returned by rnd *clause(d,m,N,p,C)* and rnd *clause(d,m,N,p',C')* with some non-zero probabilities Pk and P0 k respectively, being P0 k  Pk. From this fact, it comes straightforwardly that ' is returned by rnd CNF2m*(d,m,L,N,p,C)* and rnd CNF2m*(d,m,L,N,p',C')*
with some non-zero probabilities P and P0respectively, being P0  P. Q.E.D.

Q.E.D.

From a theoretical viewpoint, Theorem 6.1 (i) shows that our generation technique is very general, because, for every CNF2m formula ', there exists a choice for the parameters s.t. a purely random generator returns ' with some non-zero probability P.

Of course, the choice criterium for C and p suggested by points (a) and (b) is not unique as, for example, any other setting obtained from it by turning zeros into non-zeros would match the requirements. As an extreme case, we might think to do very general choices like C = [[1,1,1,...],...] p = [[[[1,1],[1,1,1],[1,1,1,1]...]]]. (6)
which guarantee to have every possible CNF2m formula within a given bound in clause size with non-zero probability. Anyway, Theorem 6.1 (ii) shows that, extending the number of non-zeros values, the probability of generating ' decreases.

$$[\,1\,,\,1\,,\,1\,]\,,\,[\,1\,,\,1\,,\,1\,]\,\cdot\,\cdot\,]\,]\,]\,.$$
