- 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.

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 |
---|---|