

![0_image_0.png](0_image_0.png)

than for C = 2:5. Trivially unsatisfiable formulae do appear, but again only after the formulae become all unsatisfiable, and not until the formulae become easy, particularly for *SAT.

At C = 2:25 we now have a reasonable set of formulae for maximum modal depth d = 2.

With a maximum modal depth of 2, the formulae are much more representative than formulae with maximum modal depth of 1. The formulae are neither too easy nor too hard for current modal decision procedures so the satisfiability transition can be investigated for significant numbers of propositional variables.

Further, with this new method we can provide a collection of test sets that vary in difficulty by varying C. Most previous comparative test sets varied N, which is problematic because most interesting parameter sets become too hard for small values of N, in the range of 6 to 10.