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