Improving the Generation of Random Modal Formulae for Testing Decision Procedures

The recent emergence of heavily-optimized modal decision procedures has led to a number of generation methods for modal formulae. However, the generation methods developed so far are not satisfactory To cope with this fact, we propose a much improved version of one of the best-known methods, the random CNFo sub m test. The new method drastically reduces the influence of a major flow of the previous method and allows us to generate a wider variety of problems covering much more of the input space. This produces more interesting test sets for the current generation of modal decision procedures.