Generating more challenging problems

There are various approaches for obtaining more challenging problems:

  1. We can construct more challenging problems by hand. This is the approach taken by Heuerding et al. The set of benchmark formulae can be obtained here.
  2. We can investigate whether there exist more appropriate parameter settings for the random generator of Giunchiglia and Sebastiani.
  3. We can design random generators for different classes of modal formulae.
In the following we focus on the second approach, but we will also discuss a modification of the random generator which will result in more challenging modal formulae. It is quite obvious from the graph showing the effect of simplification on the randomly generated formulae, that the percentage of tautological and contradictory subformulae diminishes while increasing the parameter N. We also observe that increasing the parameter N produces harder problems. Thus, we can generate more challenging problems by increasing N beyond the maximal value of N=5 used before.

The following figure shows the median CPU time performance of KsatC and MTab, a decision procedure for basic modal logic based on an analytic tableaux calculus, on the parameter setting (N=20, M=1, K=3, D=2, P=0.5).

Figure 5: Median CPU time performance of KsatC and MTab
Median CPU time performance of KsatC and MTab
MTab applies the branching rule of analytic tableau to one of the disjunctions containing the modal literal with the highest number of occurrences in the formula under consideration. Before actually applying the branching rule it will test the modal satisfiability of the [] and <> formulae currently on the branch using the (K) rule by way of trial.

Although MTab is implemented in LISP, while KsatC is implemented in C, the performance of MTab is superior for ratios L/N between 16 and 28. The following percentile graphs show that this not only holds for the median CPU time performance.

Figure 6: Percentile graphs of KsatC and MTab
Percentile graph for KsatC Percentile graph for MTab
It is interesting to observe the uniformity of these percentile graphs compared to those presented before.

However, one should note that for ratios L/N greater than 28, the majority of random modal formulae is still trivially unsatisfiable. Thus, increasing the parameter N in the current random generator will not produce challenging unsatisfiable problems. We consider this problem in the following section.

Top: Contents | Previous: A comparison of modal theorem provers: Sorting | Next: Guidelines for generating more challenging problems