Evaluating Optimized Decision Procedures for Propositional Modal K(m) Satisfiability
01 February 2002
Heavily-optimizes decision procedures for propositional modal satisfiability are now becoming available. Two systems incorporating such procedures for modal K, DLP and KSATC are tested on randomly-generated CNF formulae with several sets of parameters, varying the maximum modal depth and ratio of propositional variable to modal subformulae. The results show some easy-hard-easy behavior, but there is as yet no sharp peak as in propositional satisfiability.