Bell Labs logo

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

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

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

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