ECCC-Report TR07-023https://eccc.weizmann.ac.il/report/2007/023Comments and Revisions published for TR07-023en-usTue, 13 Mar 2007 19:51:51 +0200
Paper TR07-023
| The Complexity of Problems for Quantified Constraints |
Heribert Vollmer,
Michael Bauland,
Elmar BĂ¶hler,
Nadia Creignou,
Steffen Reith,
Henning Schnoor
https://eccc.weizmann.ac.il/report/2007/023In 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.
Tue, 13 Mar 2007 19:51:51 +0200https://eccc.weizmann.ac.il/report/2007/023