Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR07-023 | 26th February 2007 00:00

The Complexity of Problems for Quantified Constraints



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.

ISSN 1433-8092 | Imprint