Guidelines for generating more challenging problems

There is an obvious, although extreme, solution to the problem of avoiding the random generation of trivially unsatisfiable modal formulae: If we set the parameter P to 0.0, then a random 3CNF formulae will not contain purely propositional clauses. By definition, such random 3CNF formulae cannot be trivially unsatisfiable. Furthermore, we have to ensure that not too many unary and binary clauses occur in random 3CNF formulae. Thus, we also have to exclude the possibility that too many contradictory subformulae are generated. Finally, we observed in our experiments with modal formulae produced by the random generator of Giunchiglia and Sebastiani that increasing the parameter M, that is, the maximal modal depth, makes the formulae easier. Thus, we should restrict the parameter M to small values.

In MPII research report 97-2-003 we identify three guidelines for generating more challenging problems.

  1. Parameters that have no significant influence on the ``difficulty'' of the randomly generated formulae should be set to the smallest possible value. This applies to the parameters M and D. That is, we restrict our attention to random modal 3CNF formulae of degree one using only one modality.
  2. We have to avoid generating trivially unsatisfiable modal formulae. A straightforward solution is to require that all literals of a 3CNF clause of modal degree 1 are expressions of the form []p or ~[]p where p is a random modal 3CNF clause of propositional variables. This amounts to setting the parameter P to zero.
  3. For all occurrences of []p in a random modal 3CNF formula of degree 1, p has to be a non-tautologous clause containing exactly three differing literals.
In line with the second guideline one may consider excluding also trivially satisfiable modal formulae. However, this amounts to doing preliminary satisfiability checks of the generated modal formulae in order to identify and reject the trivially satisfiable ones. For the moment, we do not perform these checks. The parameters not fixed by the three guidelines are the number N of propositional variables and the number K of literals in any clause. We choose to fix K=3.

Note that these guidelines still allow that a random modal 3CNF formula contains tautological clauses, for example, [] (p | -q | r) | -[](p | r | -q) | [](p | -r | q). However, the number of such tautological clauses actually occurring in randomly generated formulae is very small and does not influence the hardness of the overall set of randomly generated formulae. In the experiments of Giunchiglia, Giunchiglia, Sebastiani, and Tachella (1998) such tautological clauses have been excluded. Nevertheless, their results are without restriction comparable to ours.

An effect that we haven't observed and has later been pointed out by Ian Horrocks is that random modal 3CNF formulae generated according to the guidelines above are harder for modal depth M=2 in comparison to M=1. In fact, they are too hard for most of the existing decision procedures. Thus, we restrict ourselves to parameter settings with M=1.

It is important to stress that it is not the intention of these guidelines to limit empirical comparisons to just those formulae generated according to them. The major purpose of the guidelines is to demonstrate that there are suitable random generators and parameter settings which allow us to obtain hard random modal formulae, in particular, hard unsatisfiable random modal formulae.

Top: Contents | Previous: Generating more challenging problems | Next: Revised comparison of modal theorem provers