# A New General Method To Generate Random Modal Formulae For Testing Decision Procedures

Peter F. Patel-Schneider PFPS@RESEARCH.BELL-LABS.COM
Bell Labs Research 600 Mountain Ave. Murray Hill, NJ 07974, USA
Roberto Sebastiani RSEBA@DIT.UNITN.IT
Dip. di Informatica e Telecomunicazioni Universita di Trento `
via Sommarive 14, I-38050, Trento, Italy

## Abstract

The recent emergence of heavily-optimized modal decision procedures has highlighted the key role of empirical testing in this domain. Unfortunately, the introduction of extensive empirical tests for modal logics is recent, and so far none of the proposed test generators is very satisfactory. To cope with this fact, we present a new random generation method that provides benefits over previous methods for generating empirical tests. It fixes and much generalizes one of the best-known methods, the random CNF2m test, allowing for generating a much wider variety of problems, covering in principle the whole input space. Our new method produces much more suitable test sets for the current generation of modal decision procedures. We analyze the features of the new method by means of an extensive collection of empirical tests.

## 1. Motivation And Goals

Heavily-optimized systems for determining satisfiability of formulae in propositional modal logics are now available. These systems, including DLP (Patel-Schneider, 1998), FACT (Horrocks, 1998), *SAT (Giunchiglia, Giunchiglia, & Tacchella, 2002), MSPASS (Hustadt, Schmidt, & Weidenbach, 1999), and RACER (Haarslev & M¨oller, 2001), have more optimizations and are much faster than the previous generation of modal decision procedures, such as LEANK (Beckert & Gor´e, 1997), LOGICS WORKBENCH (Heuerding, J¨ager, Schwendimann, & Seyfreid, 1995), 2KE (Pitt &
Cunningham, 1996) and KSAT (Giunchiglia & Sebastiani, 2000).1 As with most theorem proving problems, neither computational complexity nor asymptotic algorithmic complexity is very useful in determining the effectiveness of optimizations, so that their effectiveness has to be determined by empirical testing (Horrocks, Patel-Schneider, & Sebastiani, 2000). Empirical testing directly gives resource consumption in terms of compute time and memory use; it factors in all the pieces of the system, not just the basic algorithm itself. Empirical testing can be used not only to compare different systems, but also to tune a system with parameters that can be used to modify its performance; moreover, it can be used to show what sort of inputs the system handles well, and what sort of inputs the system handles poorly.

Unfortunately, the introduction of extensive empirical tests for modal logics is recent, and so far none of the proposed test methodologies are very satisfactory. Some methods contain many