# A New System and Methodology for Generating Random Modal Formulae

by
Peter F. Patel-Schneider & Roberto Sebastiani

# Abstract

Previous methods for generating random modal formulae (for the multi-modal 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 more-natural formulae that are better suited for current decision procedures.

Talk presented at IJCAR-2001, 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 Randomly-generated 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 Randomly-generated 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 Randomly-generated 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 strictly-propositional 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.bell-labs.com/who/pfps/dlp