Trival satisfiable and trivial unsatisfiable formulae

We have just seen that a major cause of the difference in computational behaviour of KsatLISP and KRIS is the absence of the preprocessing step in KRIS. To explain the remaining difference we study the quality of the random modal 3CNF formulae. Suppose that we want to test a random modal 3CNF formula with N propositional variables for satisfiability in a Kripke model with only one world. We have to test at most 2^N truth assignments to the propositional variables. Since N <= 5 for the modal formulae under consideration, this is a trivial task, even by the truth table method. We say a random modal 3CNF formula F is trivially satisfiable if F is satisfiable in a Kripke model with only one world. We also say a random modal 3CNF formula F is trivially unsatisfiable if the conjunction of the purely propositional clauses of F is unsatisfiable. Again, testing whether F is trivially unsatisfiable requires only the consideration of 2^N truth assignments. The following graphs show the percentage of satisfiable, trivially satisfiable, unsatisfiable, trivially unsatisfiable, and unsatisfiable formulae in the samples detected by KRIS* of the set of test formulae generated for PS0.

Figure 3: Percentage of trivial problems for PS0
Percentage of trivial problems for PS0
We see that almost all unsatisfiable test formulae are trivially unsatisfiable. This holds also for all the other parameter settings used by Giunchiglia and Sebastiani. This indicates, none of the parameter settings is suited to generate challenging unsatisfiable modal formulae.

Figure 4: Median CPU time performance of KsatLISP and KRIS*
If we consider the graphs in Figures 3 and 4 together, we observe the graph of KRIS* (in Figure 4) deviates a lot (by a factor of more than 100) from the graph of KsatLISP for ratios L/N between 19 and 21. This is the area near the crossover point where the percentage of trivially unsatisfiable formulae rises above 50%, however, the percentage of unsatisfiable formulae detected by KRIS* is still below 50% in this area, that is, KRIS* does not even detect all trivially unsatisfiable formulae within the time-limit.

This phenomenon is linked to the `heuristics' used by KRIS* to select the disjunctions to which it applies the disjunction rule: It simply selects the disjunctions in reverse order in which they appear in the input. As far as the random formulae are considered, the purely propositional disjunctions which cause the unsatisfiability of a trivially unsatisfiable formula might be far apart from each other in the input. Consequently, KRIS* applies the disjunction elimination rule not only to these propositional disjunction, but also to other disjunctions, introducing irrelevant branches into the search space. Backtracking through all these branches might not be completed within the time-limit.

There are several solutions to this problem. First, we could KRIS* with a better heuristics, for example the one used in KsatLISP. Second, we could implement a more intelligent backtracking than the chronological backtracking used in KRIS*. We will not investigate these solutions any further. On the following page we will see that rearranging the disjunction in the input of KRIS* already provides a significant improvement of its performance.


Top: Contents | Previous: KSAT versus KRIS: Simplification | Next: KSAT versus KRIS: The effect of sorting
[an error occurred while processing this directive]