Abstract
Previous methods for generating random modal formulae (for the multimodal logic
Km) result either in
flawed test sets or formulae that are too hard for current modal decision
procedures and, also, unnatural.
We present here a new system and generation methodology which results
in unflawed test sets and morenatural formulae that are better suited for
current decision procedures.
Talk presented at IJCAR2001, Sienna, Italy, June 2001.
Empirical Testing of Modal Decision Procedures
 Why:
 to see how a decision procedure performs
 How:
 try the procedure on lots of formulae
 Problem:
 generating a reasonable test set
 reasonable difficulty
 good coverage
 no problem formulae
Using Randomlygenerated Modal Formulae
 Why:
 easy to generate lots of formulae
 How:
 generate formulae according to some recipe, typically
 a conjunction of some number of clauses
 each clause has (usually) three disjuncts
 each disjunct is a (possibly negated) propositional variable
or modal formula
 contents of each modal formula is the same as a clause, until a maximum
depth is reached
 Parameters:

 maximum modal depth (d)
 number of propositional variables (N)
 probability of propositional variables (p)
 number of modal boxes (M; usually 1)
 number of disjuncts in a clause (C; usually 3)
 number of clauses (L; usually varied within each test)
Using Randomlygenerated Modal Formulae
 Problem:
 repeated propositional variables in a clause
 reduce effective size and complexity
 Solution:
 don't repeat
 Problem:
 complementary literals in a clause
 in negated modal formulae can make entire formula
unsatisfiable
 Solution:
 don't repeat
Using Randomlygenerated Modal Formulae
 Problem:
 small collection of clauses may be propositionally inconsistent
 Solution:
 eliminate propositional variables (except at maximum depth)
 Problem:
 makes the formulae unnatural and very hard
 Solution:
 new generation methodology
First Change
 restrict variability in number of propositional literals per clause
 less than one different from pC
 average number of propositional variables is pC
 eliminates strictlypropositional clauses
 sharply reduces the number of problem formulae
Old Method, Depth 2, Prop. Prob. 0.5
Median difficulty for DLP (version 4.1).
Old Method, Depth 2, Prop. Prob. 0.5
Median difficulty for *SAT (version 1.3).
Old Method, Depth 2, Prop. Prob. 0.5
Fraction of formulae that can be determined unsatifiable (or satisfiable)
by purely propositional means.
New Method, Depth 2, Prop. Prob. 0.5
Median difficulty for DLP (version 4.1).
New Method, Depth 2, Prop. Prob. 0.5
Median difficulty for *SAT (version 1.3).
New Method, Depth 2, Prop. Prob. 0.5
Fraction of formulae that can be determined unsatifiable (or satisfiable)
by purely propositional means.
Second Change
 allow the number of disjuncts in a clause to vary
 manner similar to previous method
 then determine the number of propositional literals in each clause based on
the number of disjuncts in that particular clause
 allows for easier test sets
 allows for a new source of variability
New Method, Depth 2, Prop. Prob. 0.5, 2.5 Clauses
Median difficulty for DLP (version 4.1).
New Method, Depth 2, Prop. Prob. 0.5, 2.5 Clauses
Fraction of formulae that can be determined unsatifiable (or satisfiable)
by purely propositional means.
Third Change
 direct specification of probability distributions
 for the number of disjuncts in a clause
 for the number of propositional literals in a clause
 can depend on modal depth and on number of disjuncts in the clause
 example with
 m=1
 C=[[1,8,1]]
 p=[[[1,0],[0,3,0],[0,3,3,0]]]
 N=3,4; d=3,4
C=[[1,8,1]]; p=[[[1,0],[0,3,0],[0,3,3,0]]]; N=3,4; d=3,4
Median difficulty for DLP (version 4.1).
C=[[1,8,1]]; p=[[[1,0],[0,3,0],[0,3,3,0]]]; N=3,4; d=3,4
Fraction of formulae that can be determined unsatifiable (or satisfiable)
by purely propositional means.
Summary
 New generator for random modal formulae
 Benefits
 no ``errors'' in formulae
 can generate test sets with fewer problem formulae
 can generate reasonable test sets with deeper modal depth
 Drawback
 more parameters, so harder to exhaustively explore parameter
space
 Available at http://ect.belllabs.com/who/pfps/dlp