So, at a maximum modal depth of d = 1 our method results in formulae that are of similar difficulty to the previously-generated formulae and still have trivially unsatisfiable formulae, but ones that do not seriously affect the difficulty of the test sets.

## 4.1.2 Modal Depth 2

Restricting attention to a maximum modal depth of d = 1 is not very useful. Formulae with maximum modal depth of 1 are not representative of modal formulae in general, particularly as they have no nested modal operators. Sticking to a maximum modal depth of 1 seriously limits the significance of the generated tests.

We would thus like to be able to perform interesting experiments with larger maximum modal depths. So we performed a set of experiments with a maximum modal depth of d = 2. We started with a set of tests that corresponds to previously-performed experiments.

At depth d = 2, in the old method for p = 0:5 the time curves are dominated by a "half-dome" shape, whose steep side shows up where the number of trivially unsatisfiable formulae becomes large before the formulae become otherwise easy to solve, as shown in Figure 4. In fact, nearly all the unsatisfiable formulae here are trivially unsatisfiable.

This is an extremely serious flaw, as the difficulty of the test set is being drastically affected by these trivially unsatisfiable formulae. Changing to p = 0 is not a viable solution because at depth d = 2 such formulae are much too difficult to solve, as shown in Figure 5, where the median percentile exceeds the timeout before any formulae can be determined to be unsatisfiable, even for 3 propositional variables.

With our new method, as shown in Figure 6, the formulae are much more difficult to solve than the old method, because there is no abrupt drop-off from propositional unsatisfiability, but they are much easier to solve than those generated with p = 0. Further, trivially unsatisfiable formulae do not appear at all in the interesting portion of the test sets.

Nevertheless this choice of parameters (d = 2, p = 0:5) is not entirely suitable. The formulae are becoming too hard much too early. In particular, there are no unsatisfiable formulae that can be solved for N > 3, and thus the unsatisfiability plots cannot be distinguished from the x axis (recall Footnote 6). However, our new method does provide some advantages already, providing an interesting new set of tests, albeit one of limited size.

## 4.2 Increasing P

We would like to be able to produce better test sets for depth d = 2 and greater. One way of doing this is to increase the propositional probability p from 0:5 to something like 0:6, increasing the number of propositional atoms and thus decreasing the difficulty of the generated formulae.

This would be very problematic with previous generation methods as it would result in the trivially unsatisfiable formulae determining the results for even smaller numbers of clauses L, but with our method here it is not much of a problem.

To investigate the increasing of the the propositional probability, we ran a collection of tests with maximum modal depth d = 2 and propositional probability p = 0:6 with both the old method and our new method. The results of these tests are given in Figures 7 and 8. As before, the asymmetries between the satisfiability and unsatisfiability curves in Figure 8 for N = 5; 6 are due to the fact that many tests are not solved by DLP within the time limit (c.f., Footnote 6).