# KSAT versus KRIS: The effect of sorting

In addition to the preprocessing routine which simplifies input formulae, KSAT uses a sorting technique which transforms disjunctions into a canonical form. For example, the two distinct modal atoms [1] (r | p | q) and [1] (q | r | p) will both be transformed into [1] (p | q | r). This sorting technique has two effects which cannot be separated in KSAT.
• The sorting technique allows for further simplification of the input formulae. For example, KSAT can now detect that [1] (r | p | q) | -[1] (p | q | r) is a tautology, while [1] (r | p | q) | [1] (p | q | r) will be transformed into a unit clause [1] (p | q | r).
• The sorting technique changes the number of occurrences of modal atoms. For example, while in ([1] (r | p | q) | [1] (-p | q | r)) & ([1] (q | p | r) | [1] (p | -q | r)) each modal atom occurs only once, after the application of sorting we obtain ([1] (p | q | r) | [1] (-p | q | r)) & ([1] (p | q | r) | [1] (p | -q | r)) where [1] (p | q | r) occurs twice. This will have an effect on the order in which modal atoms will be subject to applications of the branching rule of KSAT. More precisely, it optimises the formula towards the particular heuristic for applications of the branching rule used in KSAT.
Thus, while the sorting technique of KSAT can be seen as a technique enhancing the preprocessing routine, it also affects the search space and the derivations of the core decision procedure itself.

There is a subtle point concerning the implementation of the sorting technique in KSAT: It is only applied to disjunctions, not to conjunctions. For example, [1] -(r & p & q) and [1] -(q & r & p) are not affected by the sorting technique. Note that in the randomly generated modal formulae under consideration, conjunctions will only appear at the top level.

All these considerations raise a problem concerning the question whether we should add the sorting technique to the theorem provers under consideration. Note that for KSAT the ordering of the clauses in a modal 3CNF formula is almost immaterial concerning the order in which (modal) atoms will be subject to applications of the branching rule of KSAT. However, for KRIS and the Logics Workbench the (reverse) order of the clauses in the input is exactly the order in which clauses will be subject to applications of their disjunction elimination rules. Consequently, the sorting technique as implemented in KSAT will not produce the optimial result for the other theorem provers. Therefore, all the experiments in MPII research report 97-2-003 refrain from the use of this technique. Giunchiglia and Sebastiani (1998) stress that the sorting technique is an essential part of KSAT. However, for the parameter settings listed before it is actually KRIS which benefits most from using a variation of this technique.

KSAT versus KRIS* KSAT with sorting versus KRIS* with sorting
The sorting technique used in the case of KRIS* is an extension of the sorting technique used in KSAT. As pointed out above, the ordering of clauses is essential for KRIS. Thus, we reorder the clauses in the input formula to enhance the ability of KRIS to close branches early. We can improve the performance of KRIS* further by adding unit propagation to the preprocessing routine.

Top: Contents | Previous: Trival satisfiable and trivial unsatisfiable formulae | Next: A comparison of modal theorem provers
[an error occurred while processing this directive]