KSAT versus KRIS: The effect of simplification

Giunchiglia and Sebastiani (1996b) compared their system KSAT, later renamed to KsatLISP, with the tableaux-based prover KRIS. KsatLISP uses a preprocessing routine which eliminates tautological and contradictory subformulae from the input formula. Thus, for the randomly generated modal formulae under consideration, KsatLISP will take advantage of the reduction in the size of the formulae described in the previous section which also leads to a reduction in the size of the search space. However, KRIS uses no comparable preprocessing routine nor has it other means to efficiently deal with the redundancies in the random modal formulae. In fact, at the time of the comparison, KsatLISP was the only theorem prover with the appropriate simplificaiton rules.

Since the preprocessing routine is not an intrinsic part of the decision procedures, for the comparison of the procedures either all procedures should utilize the preprocessing or none of them. Simplification of the generated modal formulae is reasonable, so we have added the preprocessing function to all the theorem provers in our experiments. The combined procedures will be denoted by KRIS*, LWB* (Logics Workbench plus preprocessing), etc.

The following graphs show the impact of this alteration on the relative performance of KsatLISP versus KRIS.

Figure 2: Median CPU time performance of KsatLISP, KRIS, and KRIS*
KsatLISP versus KRIS KsatLISP versus KRIS*

While the graph on the left-hand side resembles the graph given in Giunchiglia and Sebastiani (1996b), the graph on the right-hand side shows that the major factor responsible for the inferior performance of KRIS has been the absence of appropriate simplificatin rules.

Top: Contents | Previous: A random generator for modal formulae | Next: Trival satisfiable and trivial unsatisfiable formulae
[an error occurred while processing this directive]