The Complexity of Problems for Quantified Constraints

In this paper we are interested in quantified propositional formulas in conjunctive normal form with “clauses” of arbitrary shapes. i.e., consisting of applying arbitrary relations to variables. We study the complexity of the evaluation problem, the model checking problem, the equivalence problem, and the counting problem for such formulas, both with and without a bound on the number of quantifier alternations. For each of these computational goals we get full complexity classifications: We determine the complexity of each of these problems depending on the set of relations allowed in the input formulas. Thus, on the one hand we exhibit syntactic restrictions of the original problems that are still computationally hard, and on the other hand we identify non-trivial subcases that admit efficient algorithms.