Class Tree
Description This benchmark is based on the NP^NP-complete problem of verifying
whether a set of clauses has a minimal model (w.r.t. subset inclusion)
in which some prespecified atoms are true/false [EG, 1995]. The same
scheme as in [JNSSY, 2005] is used: the sets of clauses are randomly
generated using a fixed number of clauses to variables ratio
3.75. This implies that most instances are satisfiable and hence
possessing minimal models. For each instance, the set of clauses is
encoded as a positive disjunctive logic program. Prespecified atoms
are represented using constraints involving default negation.

Parameters:

The number of propositional variables grows from 200 to 400 which implies
that the number of clauses grows from 750 to 1500.

Meanwhile the number of prespecified atoms grows from 4 to 8.

References:

[EG, 1995] T. Eiter and G. Gottlob: On the Computational Cost of
Disjunctive Logic Programming: Propositional Case. In Annals of Mathematics
and Artificial Intelligence, 19, 289-323.

[JNSSY, 2005] T. Janhunen, I. Niemelä, D. Seipel, P. Simons, and J.-H. You:
Unfolding Partiality and Disjunctions in Stable Model Semantics. ACM
Transactions on Computational Logic. To appear.
Encodings
0