normal modal formulae and CNF2m formulae9. We may wonder how well our generation technique covers the whole space of CNF2m formulae, and how well we can approximate a restricted subclass of this space. Example 5.1 represents an instance of a very general property of our random generation technique, which we present and discuss below.

Now we assume that the rnd CNF2m of Figure 13 is a "purely random" generator, i.e., it performs all non-deterministic choices independently and in a pure random way. (Of course pseudorandom generators only approximate this feature.) Moreover, with no loss of generality, we restrict our discussion to CNF2m formulae which have no repeated clauses at top level and no repeated atoms inside any clause at any level, and in which atoms are *sorted* within each clause, according to the generic function *Sort()* of Figure 13. The former allows for considering only formulae which are already simplified out; the latter allows for considering only one representative for each class of formulae which are equivalent modulo order permutations. As discussed by Giunchiglia et al. (2000), the latter allows for further simplifying subformulae like, e.g., 2(A1_A2)_2(A2_A1)
or 2(A1 _ A2) _ :2(A2 _ A1).

Let ' be a sorted CNF2m formula of depth d and with L top-level clauses built on all the propositional atoms fA1; :::AN g and on all the modal boxes f21; :::2mg, which has no repeated clause at top level and no repeated atoms inside any clause at any level. Then we can construct C and p so that, for each i, j, r:

(a) the j-th element of the i-th sublist in C is non-zero if and only if there is a clause of length j occurring at depth i in ', and
(b) the r + 1-the element of the j-th sub-sublist of the i-th sublist in p is non-zero if and only if there is a clause of length j occurring at depth i which contains r propositional literals.
One possible operative technique to build C and p works as follows. Initialize C as a list of d + 1 sublists. Then, for every depth level i 2 f0; :::; dg, set the i-th sublist of C as follows:

(i) set the size K of the sublist as the maximum size of clauses occurring in ' at depth i;
(ii) for all j 2 f1; ::; Kg, count the number of clauses of length j occurring in ' at depth i, and append the result to the sublist.
Initialize p as a list of d sublists of sub-sublists. Then, for every depth level i 2 f0; :::; d  1g, set the i-th sublist of p as follows:
(i) look at C: set the size K of the sublist as the maximum size of clauses occurring in ' at depth i;
(ii) for all j 2 f1; ::; Kg, generate the j-th sub-sublist as follows:

 look at C: if the number of clauses of length j occurring at depth i is non-zero, then set the length l of the sub-sublist to j + 1, else set l to 0;
i

'ij =)
^

$\mathbf{v}$
j

2r

_
