 we further extend the parameters p and C, allowing for shaping explicitly the probability distribution of the propositional/modal rate and the clause length respectively (Section 5.1); and we allow p and C vary with the nesting depth of the subformulae (Section 5.2), allowing for different distributions at different depths.
To investigate the properties of our CNF2m generator we also present a series of experiments with appropriate settings either to mimic previous generation methodologies or to produce improved or new kinds of tests.

In all tests we have adopted the testing criteria of the 3CNF2m method. For each test set, we fixed all parameters except L, which was varied to span at least the satisfiability transition area.

(Because of the "Valid vs. non-valid balance" feature of Section 2, we consider the transition area to be the interesting portion of the test set.) For almost all test sets we varied L from N to 120N,
150N, or 200N, resulting in integral values for L=N ranging from 1 to 120, 150, or 200. For each value of L we generated 100 formulae, a sufficient number to produce reasonably reliable data. A
time limit of 1000 seconds was imposed on each attempt to determine the satisfiability status of a formula. As it is common practice, we set the number of boxes m to 1 throughout our testing. This setting for m produces the hardest formulae (Giunchiglia & Sebastiani, 1996; Hustadt & Schmidt, 1999; Giunchiglia et al., 2000). We performed several test sets with similar parameters, often, but not always, varying only N.

We tested our formulae against two systems, DLP version 4.1 (Patel-Schneider, 1998) and
*SAT version 1.3 (Tacchella, 1999), two of the fastest modal decision procedures. They are available at http://www.bell-labs.com/usr/pfps/dlp and http://www.mrg.dist.unige.it/˜tac respectively.

All the code used to generate the tests is available at http://www.bell-labs.com/usr/pfps/dlp.

We plotted the results of our test groups (test sets with similar parameters) on six or four plots.

Two plots were devoted to the performance of DLP, one showing the median and one showing the 90th percentile time taken to solve the formulae at each value of L, plotted against L=N. For those test groups were we ran *SAT we also plotted the median and 90th percentile for *SAT.

We also plotted the fraction of the formulae that are determined to be satisfiable or unsatisfiable by DLP within the time limit.6 To save space, satisfiability and unsatisfiability fractions are plotted together on a single plot. Satisfiability fractions are higher on the left side of the plot while unsatisfiability fractions are higher on the right. This multiple plotting does obscure some of the details, but the only information that we are interested in here is the general behavior of the fractions, which is not obscured. In fact, the multiple plotting serves to highlight the crossover regions, where the satisfiability and unsatisfiability fractions are roughly equal.

Finally, we plotted the fraction of the formulae where DLP finds a model or determines that the formula is unsatisfiable without investigating any modal successors. We call these fractions the trivial satisfiability and trivial unsatisfiability fractions. These last fractions are an estimate of the number of formulae that are satisfiable in a Kripke structure with no successors —like, e.g.,
(A1 _ 21A2)— and that have no propositional valuations —like, e.g., (21A1 ^ :21A1)— respectively. For various reasons, discussed below, they are better indicators of triviality than the more