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.
MPII research report 97-2-003 we identify three guidelines for generating
more challenging problems.
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
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.
- 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
- 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.
- 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.
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
[an error occurred while processing this directive]