On Evaluating Decision Procedures for Modal Logic

1 Introduction

There are a variety of automated reasoning approaches for the basic propositional multi-modal logic K(m) and its syntactical variant , the knowledge representation for­ malism A.CC. Some approaches utilize standard first­ order theorem proving techniques in combination with translations from propositional modal logic to first-order logic [Ohlbach and Schmidt, 1995]. Others use Gentzen systems [Goble, 1974]. Still others use tableaux proof methods [Baader and Hollunder, 1991].

Usually, the literature on theorem provers for modal logic confines itself to a description of the underlying calculus and methodology accompanied with a consid­ eration of the worst-case complexity of the resulting al­ gorithm. Sometimes a small collection of benchmarks is given as in [Catach, 1991]. However, there have not been any exhaustive empirical evaluations or comparisons of the computational behavior of theorem provers based on different methodologies.

Giunchiglia and Sebastiani [1996a; 1996b] changed that. They report on an exhaustive empirical anal­ ysis of a new theorem prover, called KSAT, and the tableaux system ICRIS. KSAT is an adaptation for the multi-modal logic K(m) of a SAT-procedure for check­ ing satisfiability in propositional logic. The evaluation of Giunchiglia and Sebastiani has some shortcomings which we address. The random generator used to set up a benchmark suite produces formulae containing a sub­ stantial amount of tautologous and contradictory sub­ formulae. It favours the SAT-procedure KSAT which utilizes a preprocessing routine that eliminates trivial tautologies and contradictions from the formulae. This property of the random formulae mislead Giunchiglia and Sebastiani in their analysis and comparison of KSAT and ICRIS. We show the random generator does not produce challenging unsatisfiable modal formulae.

The paper is structured as follows. In Sections 2, 3 and 4 we briefly describe the inference mechanisms of. KsAT, ICRIS and the translation approach. Section 5 describes the evaluation method of Giunchiglia and Se­ bastiani. The main part is Section 6 which evaluates the test method.

2 The SAT-based procedure KSAT

By definition, a formula of the multi-modal logic K(m), where m is a natural number, is a boolean combination of propositional and modal atoms. A modal atom is an expression of the form 0;1/J, where i is such that 1::=;i::=;m and 1/J is a formula of K(m). 0;1/; is an abbreviation for ·0;·1/J. The semantics of K(m) is given by the usual Kripke semantics.

KSAT tests the satisfiability of a given formula ¢> of K(m). Its basic algorithm, called KsATO, is based on the following two procedures:

KDP: Given a modal formula¢>, this procedure generates a truth assignment J1. for the propositional and modal atoms in ¢> which renders ¢> true propositionally. This is done using a decision procedure for propositional logic.

KM: For a given¢> and J1. computed by KDP, let 0;1/;;j denote any modal atom in ¢> with J.l.(0;1/;;j ) = .l and O;¢>;k any modal atom with Jl.(O;¢>;k ) = T. The proce­ dure checks for each index i, 1::=;i::=;m, and each j whether the formula cpii = 1\k ¢ik 1\ ·'1/Jii is satisfiable. This is done with KDP. If at least one of the formulae cpii is not satisfiable, then KM fails on J.L, otherwise it succeeds.

KSATO starts by generating a partial truth assignment J.L for¢ using KDP. If KM succeeds on J.L, then ¢is K(m)­ satisfiable. Otherwise, we have to generate a new truth assignment for ¢ using KDP. If no further truth assign­ ment is found, then ¢ is K(m)-unsatisfiable.

The decision procedure KDP for propositional logic can be described by a set of transition rules on ordered pairs P t> S where P is a sequence of pairs (¢, J.L) , and S is a set of satisfying truth assignments.

if c is a unit clause in ¢ and ¢' is the result of replacing all occurrences of c and c by T and .L, respectively, followed by boolean simplification.

d l"t· (¢~m~, J.L) IP t> S p_sp 1 · (¢[m]/\ p, J.L l¢[mJ 1\ ·p, J.L) I P t> S if dp_unit cannot be applied to (¢[m] , J.L), and m is a propositional or modal atom.

The symbol I denotes concatenation. <f> and ¢ are com­ plementary, e.g. ·p = p and Dip= Oi'P·

Starting with (¢, 0) t> 0, exhaustively applying the inference rules will result in 0 t> S where S is a complete set of partial truth assignments making ¢ true.

Note that the transition rules form a variant of the Davis-Putnam procedure for propositional formulae not in conjunctive normal form. The crucial nondeterminism of the procedure is the selection of the splitting 'variable' m in the transition rule dp_spli t . KSAT employs the heuristic that selects an atom with a maximal number of occurrences in ¢.

3 The tableaux-based system KRIS

While KSAT abstracts from the modal part of formu­ lae to employ decision procedures for propositional logic, KRIS manipulates modal formulae (in variant notation) directly. More precisely, the inference rules of KRIS are relations on sequences of sets of labeled modal for­ mulae of the form w: 'l/J, where w is a label chosen from a countably infinite set of labels r and '1/J is modal for­ mula. For improved readability we write w:'l/J, C instead of{w:'l/J} U C.

T -elim:

if D = w:Di'l/Jl, ... , w:D;'l/Jn, C does not contain any w:Di'l/J, none of the other rules can be ap­

The application of the V-elim rule to any labeled for­ mula w:¢ V '1/J is preceeded by the application of the sim­ plification rules to that formula. In no other situation the simplification rules are invoked. Given a formula ¢, the input sequence for KRIS is wo:¢', where wo is a new label chosen from r and ¢' is the modal negation normal form of ¢. If KRIS arrives at a sequence C I S such that no transformation rule can be applied to C, then the original formula ¢ is satisfiable. Otherwise the transformation rules will eventually reduce w0 :¢' to the empty sequence and ¢ is unsatisfiable.

4 The translation approach

The translation approach (TA) is based on the idea that modal inference can be done by translating modal for­ mulae into first-order logic and conventional theorem proving. We use the optimised functional translation ap­ proach of Ohlbach and Schmidt [1995]. It has the prop­ erty that ordinary resoiution without any . refinement strategies is a decision procedure for K(m) [Schmidt , 1997]. The translation maps modal formulae into a logic, called basic path logic, which is a monadic fragment of sorted first-order logic with one binary function symbol o that defines accessibility. A formula of path logic is fur­ ther restricted in that its clausal form may only contain Skolem terms that are constants.

The optimised functional translation does a sequence of transformations. The first transformation II 1 maps a modal formula ¢ to its so-called functional translation defined by Ill(¢)= 'Vx1r1(¢, x). For K(m) , 1r1 is defined by

p is a propositional variable and P is a unary predi­ cate uniquely associated with p, defi is a special unary predicate of sort i , and a i denotes a variable of sort i. For the propositional connectives 1r 1 is a homomor­ phism. The second transformation applies the so-called quantifier exchange operator Y which moves existential quantifiers inwards over universal quantifiers using the rule '3a.V/3'1/J becomes Vf33a.'lj;'. Ohlbach and Schmidt prove YIT 1 preserves satisfiability.

Our aim is to test the satisfiability of a given modal formula ¢. This can be achieved by testing the satis­ fiability of the clausal form of --, YII 1 ( ·¢). The theo­ rem prover we use is SPASS Version 0.55 developed by Weidenbach et al. [1996] which is an ordered resolution­ based theorem prover for sorted first-order logic.

5 The test method

The evaluation method adopted by Giunchiglia and Se­ bastiani follows the approach of Mitchell et al. [1992j. To set up a benchmark suite for Davis-Putnam-based the­ orem provers Mitchell et al. generate propositional for­ mulae using the fixed clause-length model. Giunchiglia and Sebastiani modify this approach for K(m) .

There are five parameters: the number of proposi­ tional variables N, the number of modalities M, the number of modal subformulae per disjunction K, the number of modal subformulae per conjunction L, the modal degree D, and the probability P . Based on a given choice of parameters random modal KCNF formulae are defined inductively as follows. A random (modal} atom of degree 0 is a variable randomly chosen from the set of N propositional variables. A random modal atom of degree D, D>O, is with probability P a random modal atom of degree 0 or an expression of the form Di¢, other­ wise, where Di is a modality randomly chosen form the set of M modalities and ¢ is a random modal KCNF clause of modal degree D -l (defined below). A ran­ dom modal literal (of degree D) is with probability 0.5 a random modal atom (of degree D) or its negation, oth­ erwise. A random modal KCNF clause (of degree D) is a disjunction of K random modal literals (of degree D) . Now, a random modal KCNF formula (of degree D) is a conjunction of L random modal KCNF clauses (of degree D) .

For the comparison of the performance of KsAT and KRIS, Giunchiglia and Sebastiani proceed as follows . They fix all parameters except L, the number of clauses. For example, they choose N=3, M=l, K=3, D=5, and P=0.5. The parameter L ranges from N to 40N. For each value of the ratio L / N a set of 100 random modal KCNF formulae of degree D is generated. We will see that for small L the generated formulae are most likely to be satisfiable and for larger L the generated formulae are most likely to be unsatisfiable. For each generated formula ¢ they measure the time needed by one of the decision procedures to determine the satisfiability of ¢. Since checking a single formula can take arbitrarily long in the worst case, there is an upper limit for the CPU time consumed. As soon as the upper limit is reached, the computation for ¢ is stopped. If the computation for more than 50% of the formulae of a set associated with a value of L has been abandoned, then the com­ putation for the set is discontinued. Now, the median CPU time over the ratio L/N is presented. For example, the graphs of Figure 1 ·show the performance of KniS and KSAT on the parameter settings PSO (N=3, M=l, K=3, D=5) and PSI (N=5, M=l, K=3, D=2) . Our tests have been run on a Sun Ultra 1/170E with 196MB main memory using a time-limit of 1000 CPU seconds. Altogether Giunchiglia and Sebastiani [1996b] present graphs for ten different parameter settings. Based on their graphs including Figure 1 they come to the follow­ ing conclusions:

1. KSAT outperforms by orders of magnitude the pre­ vious state-of-the art decision procedures.
2. All SAT-based modal decision procedures are intrin­ sically bound to be more efficient than tableaux­ based decision procedures.
3. There is partial evidence of an easy-hard-easy pat­ tern on randomly generated modal logic formulae independent of all the parameters of evaluation con­ sidered.

We show that the situation is more complex and does not justify such strong claims. For our analysis it suffices to focus on the settings PSO and PSI of Figure 1.

6 Analysis of the test method

Selecting good test instances is crucial when evaluating and comparing the performance of algorithms empiri­ cally. We address the question whether the random gen­ erator and the parameter settings chosen by Giunchiglia and Sebastiani [1996b; 1996a] are appropriate for this purpose and actually support claims (1) to (3) .

It is important to note that the claim of Giunchiglia and Sebastiani [1996b, p. 307] that for D=O random modal 3CNF formulae coincide with random 3SAT

clauses as defined in Mitchell et al. is wrong: To gen­ erate a random 3SAT clause we have to randomly gen­ erate a set of three propositional variables and negate each member of the set with probability 0.5. In con­ trast, to generate a random modal 3CNF clause of de­ gree 0, we have to randomly generate a multiset of three propositional variables and negate each member of the multiset with probability 0.5. For example, p V q V -,r is a 3SAT clause and also a modal 3CNF clause of degree 0. The clauses p V -,p V p and p V p V q are not random 3SAT clauses, but both are random modal 3CNF clauses of degree 0. As we move to random modal 3CNF for­ mulae of higher degree, such clauses may occur within the scope of a modal operator. For example, expres­ sions like -,01 (p V -,p V p) may occur which are contra­ dictory. Consequently, random modal KCNF formulae contain tautological and contradictory subformulae. It is straightforward to remove these subformulae without affecting satisfiability. The extent to which the size of the random modal 3CNF formulae can be reduced by such simplifications is reflected by the graphs of Fig­ ure 2. They depict the average ratio of the size of the simplified random modal 3CNF formulae over the size of the original formulae . For the random modal 3CNF for­ mulae generated using three propositional variables only, on average, the size of a simplified formula is only 1/4 of the size of the original formula. For the second parame­ ter setting we see a reduction to 1/2 of the original size. In other words, one half to three quarters of the random modal 3CNF formulae is "logical garbage" that can be eliminated at little cost.

KSAT utilizes a form of preprocessing that removes duplicate and contradictory subformulae of an input for­ mula. That is, KSAT performs exactly the simplification whose effect we have just described. KRIS on the other hand does not perform a similar simplification. We con­ sider how KsAT performs if we remove the preprocessing step from its code. In Figure 3 KSATO denotes this mod­ ified form of KSAT, since it is actually identical to the algorithm described in Section 2. We see that the behav­ ior of KsATO differs from the behavior of KSAT by orders of magnitude. Since the preprocessing is not an intrin­ sic part of the decision procedures, for the comparison of the procedures, either both KSAT and KRIS should utilize the preprocessing or none of them should. Sim­ plification of the generated formulae is reasonable, so we have added the preprocessing function to KRIS. This modified version of KRIS will be denoted by KRIS*. The graphs in Figure 4 show the performance of KsAT and KRIS*. Although the performance of KSAT is still better than that of KRIS*, KSAT is no longer qualita­ tively better than KRIS with preprocessing.

We now address claim (2) that, intrinsically, SAT­ based modal decision procedures are bound to be more efficient than tableaux-based decision procedures. The explanation is based on the work by D' Agostino [1992] , who shows that in the worst case algorithms using the V-elim rule cannot simulate truth tables in polynomial time. Instead one has to replace V-elim by the rule

This rule ensures that the two generated subproblems w:¢, C and w:'!f;, w:-.¢, C are mutually exclusive.

We have just seen that a major cause of the difference in computational behavior of the two algorithms is ac­ tually the absence of the preprocessing step in KR:IS. To explain the remaining difference we study the qual­ ity of the random modal 3CNF formulae. Suppose that we want to test a random modal 3CNF formula ¢ gen­ erated using N propositional variables for satisfiability in a Kripke model with only one world. We have to test at most 2N truth assignments to the propositional variables. Since N ~5 for the modal formulae under con­ sideration, this is a trivial task, even if we use the truth table method. We say a random modal 3CNF formula ¢ is trivially satisfiable if ¢ is satisfiable in a Kripke model with only one world. We also say a random modal 3CNF formula ¢ is trivially unsatisfiable if the conjunc­ tion of the purely propositional clauses of ¢ is unsatisfi­ able. Again, testing whether ¢ is trivially unsatisfiable requires the consideration of 2N truth assignments only.

The graphs of Figure 5 show the percentage of satisfi­ able, trivially satisfiable, unsatisfiable, trivially unsatis­ fiable, and unsatisfiable samples detected by KR:IS* for the parameter setting PSl. We see that almost all un­ satisfiable formulae are trivially unsatisfiable. We have verified that this also holds for all the other parame­ ter settings used by Giunchiglia and Sebastiani. This indicates, none of these parameter settings is suited to generate challenging unsatisfiable modal formulae.

If we consider Figure 4 and 5 together, for ratios L/N between 19 and 21 we observe the graph of KRIS* de­ viates a lot (by a factor of more than 100) from the graph of KSAT. This is the area near the crossover point where the percentage of trivially unsatisfiable formulae rises above 50%, however, the percentage of unsatisfiable formulae detected by KRIS* is still below 50% in this area. KRIS* does not detect all trivially unsatisfiable formulae within the time-limit which explains the devia­ tion in performance from KSAT. The reason for KRIS* not detecting all trivially unsatisfiable formulae within the time limit, can be illustrated by the following exam­ ple. Let ¢ be a simplified modal 3CNF formula

where the mij, with 1~i~n, 1~j~3, are modal literals different from p, q, -.p, and -.q. Evidently, ¢ is triv­ ially unsatisfiable. KSAT does the following: Since p and q are unit clauses in ¢, it applies the rule dp_uni t twice to ¢. The rule replaces the occurrences of p and q by T, it replaces the occurrences of -.p and -.q by .l , and it simplifies the formula. The resulting formula is .l. At this point only the rule dp_clash is applicable and KSAT detects that .¢ is unsatisfiable. In contrast, KRIS* proceeds as follows. First it applies the 1\-elim rule n+2 times, eliminating all occurrences of the 1\ op­ erator. Then it applies the V-elim rule to all disjunc­ tions, starting with (m11 V m12 V m13) and ending with (mnl V mn2 V mn3)· This generates 3n subproblems. Each of these subproblems contains the literals p and q and the disjunction -.p V -.q. The rule V-simp1 elimi­ nates -.p V -.q and a final application of the 1\ -clash rule exhibits the unsatisfiability of each subproblem. Obvi­ ously, for n large enough, KRIS* will not be able to finish this computation within the time-limit.

Note, it makes no difference whether KR:IS* elimi­ nates disjunctions by the V-elim rule or the V-elim' rule. The reason for KR:IS* not finishing within the time-limit is that it does not apply the simplification rules V-simp1 and V-simp2 and the /\-clash rule ea­ gerly before any application of the V-elim rule.

Finally, we consider claim (3) conjecturing an easy­ hard-easy pattern, independent of all the parameters of evaluation, in randomly generated modal logic for­ mulae. We have seen in Figure 1 that the mean CPU time consumption of KSAT decreases drastically at the ratio L/N=17.5 for the second sample. This is almost the point, where 50% of the sample formulae are satis­ fiable. This decline resembles the behavior of proposi­ tional SAT decision procedures on randomly generated 3SAT problems. Figure 6 compares the performance of KSAT with the performance of the translation approach on two parameter settings, where the easy-hard-easy pat­ tern is most visible for KSAT. The translatioq approach does not show the peaking behavior of KSAT. The me­ dian CPU time grows monotonically with the size of modal formulae. Thus, the phase transition observed by Giunchiglia and Sebastiani is an artificial phenomenon of KSAT (and KRIS), and not an intrinsic property of the generated modal formulae.

Observe that the peaking behavior occurs in the area where the number of trivially satisfiable sample formulae approaches zero. The following example tries to explain this. Let '1/J be a simplified modal 3CNF formula of the form

where the mij, with 1:S:i:S:n, 1:S:j:S:3, are modal literals different from the modal literals in the first three con­ junctions of '1/J. Assume, '1/J is satisfiable. 0 1 ·r is false in any model of '1/J. In the situation that 0 1 ·r is one of the first split literals chosen by KSAT, it generates a huge search tree without finding a satisfying truth as­ signment before it eventually turns to the case where D1 ·r is assigned .l. This explains the bad behaviour of KsAT on those sample formulae where satisfiability tests in the non-propositional contexts are essential. KRIS* behaves similarly.

In contrast, the translation approach proceeds as fol­ lows. It generates a clause set for '1/J containing

·P(k o Q) V ·de/1 (k) V R(k ox)

where ,!,, g and Q denote Skolem constants and x and y are variables. SPASS applies unit propagation to the first clause followed by subsumption. Three resolvents can be derived: P(k ox) V Q(k o y), ·P(k o Q) V Q(k o y), and R(k o Q) V R(k ox). A factoring step on the last resolvent yields R(k o Q). This means 0 1 ·r is false in any model. An additional inference step computes the unit clause Q(k o y). No further inference is possible on this subset.

7 Conclusion

We have pointed out a number of problems with evalu­ ating the performance of different algorithms for modal reasoning. Our investigations show benchmarking needs to be done with great care. A crucial factor is the quality of the randomly generated problems, which we think are too easy. Further investigations are required concern­ ing the parameter settings and fundamental properties of modal KCNF formulae before we can come to safe conclusions about different theorem proving approaches for modal logic.

A longer version of this paper is available as Research Report MPI-1-97-2-003.