and 2 with probability 2=3); rnd *propnum(d,p,K)* selects randomly the number of propositional atoms per clause P according to the [d + 1; K℄-th distribution in p (e.g, if d is 1, K is 2 and p is
[[[],[0,1,0],[0,1,0,0]] [[1,0][0,1,0]]], it returns 1 deterministically); rnd *sign* selects randomly either the positive or negative sign with equal probability; no repeated atoms *in(Cl)*
checks if the clause C l contains no repeated atom; *Sort(Cl)* returns the clause C l sorted according to some criterium; rnd propositional *atom(N)* selects with uniform probability one of the N propositional atoms Ai ; rnd *box(m)* selects with uniform probability one of the m indexed boxes 2r .

When eliminating duplicated atoms in a clause, we take care not to disturb these probabilities by first determining the "shape" of a clause (rows 8-9 in Figure 13), and only then instantiating that with propositional variables (rows 10-16 in Figure 13). If a clause has repeated atoms, either propositional or modal, the instantiation is rejected and another instantiation of the shape is performed.

If we did not take care in this way we would generate too few "small" atoms because there are fewer small atoms than large atoms, resulting in a greater chance of rejecting small atoms because of repetition.

The elimination of duplicated atoms in a clause is not only a matter of elimination of redundancies, but also of elimination of a source of flaws. In fact, one might generate top-level clauses like
::: ^ (:21(A1 _ :A1) _ :22(A2 _ :A2)) ^ :::, which would make the whole formula inconsistent.

Example 5.1 We try to guess a parameter set by which the new random generator can potentially generate the following CNF2m formula ':

$$\begin{array}{l l}{{\neg A_{3}\lor\Box_{1}\big(\neg A_{4}\lor\neg\Box_{1}A_{1}\big)\lor\Box_{1}\big(\neg A_{1}\lor\neg\Box_{1}A_{2}\big)}}&{{\big)\land}}\\ {{\neg A_{1}\lor\Box_{1}\big(A_{3}\lor\neg\Box_{1}A_{2}\big)\lor\neg\Box_{1}\big(\Box_{1}\neg A_{4}\big)}}&{{\big)\land}}\\ {{\neg A_{4}\lor\neg\Box_{1}\big(A_{2}\lor\Box_{1}\neg A_{1}\big)}}&{{\big)\land}}\\ {{A_{1}\lor\neg\Box_{1}\big(\neg\Box_{1}A_{4}\big)}}&{{\big).}}\end{array}$$
$${\sf C}\ =\ {\sf[\ [\ 0\,,\,2\,,\,2\ ]\,,\ [\ 2\,,\,4\ ]\,,\ [\ 6\ ]\ ]}\ .$$
$${\mathrm{(2)}}$$
$$1\cdot$$
$$({\boldsymbol{\mathsf{S}}})$$

After a quick look we set m = 1, d = 2, N = 4, L = 4. At top level we have 0 unary, 2 binary and 2 ternary clauses; at depth 1 we have 2 unary and 4 binary clauses; at depth 2 we have only 6 unary clauses. Thus, we can set C = [[0,2,2],[2,4],[6]]. (3)
At top level there are no unary clauses (we represent this fact by the empty list "[]"), the 2 binary clauses have 1 propositional literal, and the 2 ternary clauses have 1 propositional literal; at depth 1, the 2 unary clauses have 0 propositional literals, while the 4 binary clauses have 1 propositional literal. (There is no need to provide any information for depth 2, as all clauses are purely propositional.) Thus, we can set p = [[[],[0,2,0],[0,2,0,0]] [[2,0],[0,4,0]]]. (4)
The two expressions can then be normalized into:

$$C=\left[\,[\,0,1,1],[1,2],[1]\,]\,\right]$$ $$P=\left[\,[\,[\,],[\,0,1,0],[\,0,1,0,0]\,]\,\right]\,\left[\,[1,0],[\,0,1,0]\,]\,\right].$$

Notice that any other setting of C, p obtained by changing the non-zero values in (5) into other non-zero values, or turning zeros into non-zeros (but not vice versa!), will do the work, just with a different probability. For instance, turning the first list in C into [1,1,1] allows for generating also unary clauses at top level; anyway, with probability (2=3)Lthe generator may still produce formulae with only binary and ternary clauses at top level. 2