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