Artificiality: Our method allows the user to shape the test formulae so that to maximize the resemblance to the expected typical inputs of his/her system(s). Of course, this is done within the limits imposed by randomness: the more irregular the typical input formulas, the higher the variance of the randomly generated formulas, the lower their average resemblance to the typical input formulas.

Over-size: The new method allows for generating extremely hard problems with reasonable size.

It comes from the analysis of the resulting data that hard problems require very big amounts of both search branches and modal successors generated, so that the search is not dominated by parsing and data managing.

The generator presented by Horrocks and Patel-Schneider (2002), extends the 3CNF2m generator of Giunchiglia et al. (2000) too. However, our new generator allows for shaping the probability distributions of both C and p, and for using different distributions at every depth level. In principle, the generator of Horrocks and Patel-Schneider (2002) allows also for setting the probabilities np and nm by which propositional and modal atoms are negated. However, this feature is not used very much—in the experiments by Horrocks and Patel-Schneider (2002) np is always 0:5 and nm is different from 0:5 only in one experiment— and adds nothing to the generality of the generator, so that in our new generator we decided not to re-introduce it.

## 7.3 Comparison With The Qbf-Based Method

Before comparing our new CNF2m generation method with the QBF-based generation method, we must notice that, so far, they have been used in different ways, corresponding to the two different test techniques briefly summarized in Section 3.

 In the TANCS competition(s) (Massacci, 1999), the tests have been performed on single data points, and the results are presented in the form of big tables, each entry consisting of the number of successful solutions and in the rescaled geometrical mean CPU time for such solutions. Two or more systems are compared according to their number of successful solutions, considering the geometrical mean CPU time value only when the result is even. This is due to the fact that a comparison between geometrical means is possible only if they are computed on the same number of successful values, or, for a more accurate comparison, on the same successful values.12 This method was chosen to guarantee the fairness of the comparison between the competitors, which is the key requirement in a competition.

 In this paper instead, we have focused on highlighting both the qualitative and quantitative behavior of the system(s). Thus we have preferred plots to tables, and we have preferred representing percentiles CPU times rather than the number of successful solutions and their geometrical mean times. In fact, the former does not require to distinguish between successful and non-successful solutions.13 Thus, they are much more suitable for plotting, because a comparison on geometrical means makes sense only for those data points with the same number of successful solutions, which is very hard to follow in a plot.