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