Class Tree  

Description 
This benchmark is based on the NP^NPcomplete 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, 289323. [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 
