In MPII research report 97-2-003 we identify three guidelines for generating more challenging problems.

- Parameters that have no significant influence on the ``difficulty'' of the randomly generated formulae should be set to the smallest possible value. This applies to the parameters M and D. That is, we restrict our attention to random modal 3CNF formulae of degree one using only one modality.
- We have to avoid generating trivially unsatisfiable
modal formulae. A straightforward solution is to require that all
literals of a 3CNF clause of modal degree 1 are expressions of the
form
*[]p*or*~[]p*where*p*is a random modal 3CNF clause of propositional variables. This amounts to setting the parameter P to zero. - For all occurrences of
*[]p*in a random modal 3CNF formula of degree 1,*p*has to be a non-tautologous clause containing exactly three differing literals.

Note that these guidelines still allow that a random modal 3CNF formula contains
tautological clauses, for example,
*[] (p | -q | r) | -[](p | r | -q) | [](p | -r | q)*.
However, the number of such tautological clauses actually occurring in randomly
generated formulae is very small and does not influence the hardness of the overall
set of randomly generated formulae.
In the experiments of Giunchiglia, Giunchiglia, Sebastiani, and Tachella (1998)
such tautological clauses have been excluded. Nevertheless, their results are without
restriction comparable to ours.

An effect that we haven't observed and has later been pointed out by Ian Horrocks is
that random modal 3CNF formulae generated according to the guidelines above are
harder for modal depth *M=2* in comparison to *M=1*. In fact, they are
too hard for most of the existing decision procedures. Thus, we restrict
ourselves to parameter settings with *M=1*.

It is important to stress that it is not the intention of these guidelines to limit empirical comparisons to just those formulae generated according to them. The major purpose of the guidelines is to demonstrate that there are suitable random generators and parameter settings which allow us to obtain hard random modal formulae, in particular, hard unsatisfiable random modal formulae.