TR06-160 Authors: Tomas Feder, Phokion G. Kolaitis

Publication: 31st December 2006 20:24

Downloads: 984

Keywords:

Quantified constraint satisfaction is the generalization of

constraint satisfaction that allows for both universal and existential

quantifiers over constrained variables, instead

of just existential quantifiers.

We study quantified constraint satisfaction problems ${\rm CSP}(Q,S)$, where $Q$ denotes

a pattern of quantifier alternation ending in exists or the set of all possible

alternations of quantifiers, and $S$ is a set of relations constraining

the combinations of values that the variables may take.

These problems

belong to the corresponding level of the polynomial hierarchy or in PSPACE,

depending on whether $Q$ is a fixed pattern of quantifier alternation

or the set of all possible alternations of quantifiers.

We also introduce and study the

quantified constraint satisfaction problems ${\rm CSP'}(Q,S)$

in which the universally quantified variables are restricted to range

over given subsets of the domain.

We first show that ${\rm CSP}(Q,S)$ and ${\rm CSP'}(Q,S)$

are polynomial-time equivalent to

the problem of evaluating certain syntactically restricted

monadic second-order formulas on finite structures.

After this, we establish three broad sufficient conditions for polynomial-time

solvability

of ${\rm CSP'}(Q,S)$ that are based on closure functions; these results

generalize and extend earlier results by other researchers

about polynomial-time solvability of ${\rm CSP}(Q,S)$.

Our study culminates with a

dichotomy theorem for the complexity of list ${\rm CSP'}(Q,S)$,

that is, ${\rm CSP'}(Q,S)$ where the relations of $S$ include

every subset of the domain of $S$. Specifically, list

${\rm CSP'}(Q,S)$ is either solvable in polynomial-time or complete

for the corresponding level of the polynomial hierarchy, if

$Q$ is a fixed pattern of quantifier alternation (or PSPACE-complete

if $Q$ is the set of all possible alternations of quantifiers).

The proofs are based on a more general unique sink property formulation.