Instance Class Disj3SAT

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.


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.


[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.
Submitter Martin Gebser
Compatible Encodings
    Output Predicates