In this paper we will look at restricted versions of the evaluation problem, the model checking problem, the equivalence problem, and the counting problem for quantified propositional formulas, both with and without bound on the number of quantifier alternations. The restrictions are such that we consider formulas in conjunctive normal-form with restricted types of clauses (e.g., positive, Horn, linear, etc.). For each of these algorithmic goals we will obtain full complexity classifications, exhibiting on the one hand severe syntactic restrictions of the original problems that are still computationally hard, and on the other hand non-trivial subcases that admit efficient solution algorithms.

Generalizing these results to non Boolean domains, we obtain a number of hardnes results for quantified constraints over arbitrary finite universes.

Some of the results reported in Sect. 5.2 of this paper already appeared in ECCC Report 05-024.