There are five parameters:
the number of propositional variables *N*,
the number of modalities *M*,
the number of modal subformulae per disjunction *K*,
the number of modal subformulae per conjunction *L*,
the modal degree *D*, and
the probability *P*.
Based on a given choice of parameters random modal *K*CNF formulae
are defined inductively as follows.

A *random (modal) atom* of degree 0 is a
variable randomly chosen from the set of *N* propositional variables.

A *random modal atom* of degree *D*, *D{>}0*,
is with probability *P* a random modal atom of degree *0* or
an expression of the form *[i] F*, otherwise, where *[i]* is a modality
randomly chosen form the set of *M* modalities and *F* is a random
modal *K*CNF clause of modal degree *D-1* (defined below).

A *random modal literal* (of degree *D*) is with probability
*0.5* a random modal atom (of degree *D*) or its negation, otherwise.

A *random modal KCNF clause* of degree *D*) is a disjunction of
*K* random modal literals (of degree *D*).

Now, a *random modal KCNF formula* (of degree

The parameter settings considered in Giunchiglia and Sebastiani (1996b) are the following.

N | M | K | D | P | N | M | K | D | P | ||

PS0 | 5 | 1 | 3 | 2 | 0.5 | PS5 | 4 | 1 | 3 | 2 | 0.5 |

PS1 | 3 | 1 | 3 | 5 | 0.5 | PS6 | 4 | 2 | 3 | 2 | 0.5 |

PS2 | 3 | 1 | 3 | 4 | 0.5 | PS7 | 4 | 5 | 3 | 2 | 0.5 |

PS3 | 3 | 1 | 3 | 3 | 0.5 | PS8 | 4 | 10 | 3 | 2 | 0.5 |

PS4 | 3 | 1 | 3 | 2 | 0.5 | PS9 | 4 | 20 | 3 | 2 | 0.5 |

It is important to note that
for *D=0* and *K=3* random modal *K*CNF formulae do
**not**
coincide with random *3*SAT formulae (as mistakenly claimed
by Giunchiglia and Sebastiani (1996b)).
Generating a clause of a
random *3*SAT formula means randomly generating a **set** of
three propositional variables and then negating each member of the set with
probability *0.5*. In contrast, generating a random
modal *3*CNF clause of degree 0 means randomly generating a
**multiset** of three propositional variables and negate each member
of the multiset with probability *0.5*. For example,
*(p | q | -r)* is a *3*SAT clause and also a
modal *3*CNF clause of degree 0. The clauses
*(p | -p | p)* and *(p | p | q)* are not
*3*SAT clauses, but both are random modal *3*CNF clauses of degree 0.
In random modal *3*CNF formulae of higher degree,
such clauses occur within the scope of a modal operator. For example,
contradictory expressions like *-[1](p | -p | p)* may occur.
Thus, random modal *K*CNF formulae contain
tautological and contradictory subformulae.

Occurrences of tautological and contradictory subformulae in the randomly generated formulae are not a problem in themselves as long as the evalution of the methods takes this fact into accout. Let us first investigate the question whether the occurrence of tautological and contradictory subformulae is only a rare phenomenon or whether it could seriously influence the evalution. To this end we apply standard simplication rules to the randomly generated formulae to remove tautological and contradictory subformulae and compare the size of the formulae before and after the simplification. The following graph shows the effect on the average formula size for two of the parameter settings used by Giunchiglia and Sebastiani (1996b).

Thus, occurrences of tautological and contradictory subformulae are not a rare phenomenon for the parameter settings used by Giunchigila and Sebastiani (1996b). Any modal theorem prover which does not efficiently eliminiate such trivial subformulae will have a disadvantage on these random modal formulae.