The Complexity of Problems for Quantified Constraints

作者：Bauland Michael; Boehler Elmar; Creignou Nadia; Reith Steffen; Schnoor Henning; Vollmer Heribert^*

来源：Theory of Computing Systems, 2010, 47(2): 454-490.

DOI：10.1007/s00224-009-9194-6

• Satisfiability problems
• Quantified formulas
• Constraint satisfaction
• Computational complexity

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.

• 出版日期2010-8