The problem is to decide whether a quantified boolean formula (QBF) F defined as:

F = FORALL Y EXISTS X G

(where X and Y are disjoint sets of variables and G is a CNF formula over variables from X union Y) is true. That is, we want to know whether it is true that for each truth assignment to the variables in Y there is a truth assignment to the variables in X which makes G true.

INPUT: Sets of variables X and Y, CNF formula G

OUTPUT: message YES if G holds; otherwise NO.

DATA SETS:

qbf1.edb

qbf2.edb

qbf3.edb

qbf4.edb

qbf5.edb

qbf6.edb

qbf7.edb

qbf8.edb

qbf9.edb

NOTES:

- Each data set is prepared as follows: fact exists(x) states that x is a variable under the scope of the existential quantifier, fact forall(y) states that y is a variable under the scope of the universal quantifier; predicate conjunct is used to define conjuncts of the formula G