Generating more challenging problems
There are various approaches for obtaining more challenging problems:
- 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.
- We can investigate whether there exist more appropriate parameter
settings for the random generator of Giunchiglia and Sebastiani.
- 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](gps20km.gif) |
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](20-ksatc.gif) |
![Percentile graph for MTab](20-mtab.gif) |
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