The Complexity of Quantified Constraint Satisfaction Problems under Structural Restrictions

1 Introduction

Quantified constraint satisfaction problems (QCSPs) are a generalization of constraint satisfaction problems (CSPs), where variables may be existentially and universally quantified, and nested quantifications are allowed. This framework is clearly much more expressive than plain existential-CSP, and may be fruitfully exploited for modeling a wide spectrum of problems from several domains.

A QCSP instance (or quantified constraint formula) φ is an expression of the form Q1 ¯ V1 · · · Qm ¯ Vm I, where I is a constraint network (denoted by CN (φ)), Qi is a quantifier in {∃, ∀} (with Qi ̸= Qi+1), and ¯ Vi is a set of variables, for 1 ≤ i ≤ m. The string of quantifiers Q1 · · ·Qm is called the prefix of φ. Recall that a constraint network is a triple I = (Var, ¯ U, C), where Var is a finite set of variables, U is the set of domains U(V ), for each variable V ∈ Var, and C = {C1,C2, . . . ,Cq} is a finite set of constraints. A constraint Ci = (Si, ri) consists of a list of variables Si called constraint scope, and of a relation ri, called constraint relation, providing Ci's allowed combinations of values for the variables in its scope. Sometimes it is more comfortable to denote Ci by its so called constraint atom ri(Si). Then, the network I may be represented by the conjunction of all its constraint atoms. For simplicity, we limit our attention here to closed quantified constraint formulas, where all variables occurring in I are quantified. However, all our results may be easily extended to formulas with free variables.

∗This work was supported by the Austrian Science Fund (FWF) project: Nr. P17222-N04 Complementary Approaches to Constraint Satisfaction.

As an example, consider the following quantified constraint formula φe: ∀S,X, Y, T,R,U, P ∃V,Z ∀W a(S, X, T, R) ∧ b(S, Y, U, P ) ∧ c(T, U, Z) ∧ d(W, X, Z) ∧ e(Y, Z) ∧ f(R, P, V ) ∧ g(X, Y ). This formula is a QCSP instance, whose constraint network CN (φe) is represented by the constraint atoms occurring in the conjunction. The quantifier prefix (short: prefix) of φe is the string ∀∃∀.

Not surprisingly, the increased expressive power of QCSPs comes at a cost. Indeed, while deciding the satisfiability of traditional (i.e., purely existential) CSPs is NP-complete, this problem is PSPACE-complete [Borner et al., 2003], in the general quantified setting. Hence, much effort has been spent to identify tractable classes of QCSPs.

These approaches can be divided into two main groups: techniques that identify tractable classes of QCSPs by exploiting particular properties of constraint relations, and techniques that identify tractable classes by exploiting the structure of constraint scopes, usually known as structural decomposition methods. While several deep results have been already achieved by techniques in the former group (see, e.g., [Borner et al., 2003; Bulatov et al., 2000; Bunind et al., 1995; Chen, 2004a; Creignou et al., 2001; Jeavons et al., 1997]), only a few papers focused on structural decomposition methods, though they were proven to be useful in the non-quantified setting (see, e.g., [Dechter, 2003; Gottlob et al., 2000]).

Recall that the structure of constraint network I is best represented by its associated hypergraph H(I) = (V, H), where V = Var and H = {var (S) | C = (S, r) ∈ C}, and var (S) denotes the set of variables in the scope S of constraint C. Some graph-based techniques are based on the primal graph G (H(I)) = (V,E) of H(I), where two variables are connected in E if they occur together in some hyperedge (i.e., in the scope of some constraint).

Chen recently presented an interesting result about structurally tractable QCSPs [Chen, 2004b]. He describes a polynomial-time algorithm for classes of QCSPs having (primal graphs with) bounded treewidth, fixed domain, and fixed prefix. In fact, the complexity of this algorithm depends dramatically on the number of quantifier alternations and on the size of the largest variable domain. As noted in [Chen, 2004b], the same result has been independently derived by [Feder and Kolaitis, 2004], by exploiting Courcelle's theorem about monadic second order logic on bounded treewidth structures.

Notice that there is no indication that these results are optimal, and in fact several interesting questions arose, and will be the subject of this paper:

(1) Are QCSPs having bounded treewidth tractable if domains are not fixed?

(2) May we extend this result to other structural notions, possibly more general than bounded treewidth?

1. Are there different kind of restrictions on quantified constraint formulas that make QCSPs tractable?

The answers to these questions comprise both good news and bad news. We prove strong hardness results, but we also identify new tractable classes of QCSPs, having neither fixed bound on domains nor fixed bound on quantifier alternations. Our main contributions, shown in Figure 1, are the following:

• We prove that, without the fixed domain restriction, even QCSP instances whose structure is a tree and whose prefix is ∀∃ are co-NP-hard. Moreover, adding further alternations we get complete problems for all levels of the polynomial hierarchy. It follows that this problem is PSPACE-complete if there are no bounds on the quantifier prefix.
• On the positive side, we prove that, if the prefix is ∃∀ (or some substring of it), then solving acyclic QCSPs is feasible in LOGCFL and hence in polynomial time. Moreover, this tractability extends to all known generalizations of acyclicity, and in particular to bounded hypertree-width QCSPs [Gottlob et al., 2000].
• We prove that, for fixed domains, the tractability result for bounded treewidth is almost optimal. Indeed, solving QCSPs over the binary domain {0, 1} remains PSPACEcomplete even if the structure is an acyclic hypergraph, whose incidence graph has bounded treewidth, and whose primal graph has small (i.e., logarithmic) treewidth.
• All these results show that traditional structural techniques do not help very much, but for some simple cases and with limited quantification. Indeed, our hardness proofs show that the presence of quantifiers radically alters the structural properties of the constraint scopes. We thus realize that it is worthwhile taking into account how they interact with the scope structure, and in fact considering quantifiers as part of the scope structure itself. Following this idea, we identify a different kind of restriction on quantified constraint formulas that ensure tractability and that is incomparable with the other structural classes. In particular, for any fixed k, we define the class k-GQCSP of k-guarded QCSPs, that are solvable in polynomial time, without any restriction on domains or quantifier alternations.

2 Quantified CSPs

Let I = (Var , U, C) be a constraint network. An assignment σ for a set of variables ¯ V ⊆ Var is a function mapping each variable V ∈ ¯ V onto its domain U(V ) ∈ U. If ¯ V = Var, σ is said complete, otherwise it is a partial assignment. We say that a complete assignment σ satisfies I, denoted by σ |= I, HolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHolesHoles WeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeaveWeave if for each constraint (Si, ri) ∈ C, σ(Si) ∈ ri. An extension of σ to a set ¯ V ′ ⊃ ¯ V is an assignment σ′ for ¯ V ′ such that σ′ (V ) = σ(V ) for each V ∈ ¯ V . We denote by ext (σ, ¯ V ′ ) the set of all the extensions of σ to ¯ V ′ . For the trivial assignment σ∅ for the empty set of variables, ext (σ∅, ¯ V ′ ) is clearly the set of all assignments for ¯ V ′ .

Figure 1: Structural restrictions and (in)tractable QCSPs.

Let φ : Q1 ¯ V1Q2 ¯ V2Q3 ¯ V3 . . .Qm ¯ Vm I be a QCSP instance, and let σ0 be the trivial assignment σ∅. A strategy for φ is any function s such that, for each pair Qi, σi-1, with 1 ≤ i ≤ m, s(Qi, σi-1) is either one assignment in ext (σi-1, ¯ Vi), if Qi = ∃, or the whole set of possible extensions ext (σi-1, ¯ Vi), if Qi = ∀. A complete assignment σm is derivable from a strategy s if there are m1 assignments σ1, . . . , σm-1 such that σi ∈ s(Qi, σi-1), for any 1 ≤ i ≤ m. Then, s is a solution for φ if all derivable assignments satisfy I. A QCSP instance is satisfiable iff it has a solution.

It is worthwhile noting that, in the definition of QCSPs, different variables have different domains, in general. This is especially useful in the quantified setting. However, in the literature, QCSPs are sometimes defined over a unique domain U or, equivalently, with the same domain U(V ) for each variable V . We say that such QCSPs are untyped, in contrast to the general ones, called typed. The following proposition shows that the two formalisms are in fact logically equivalent.

Proposition 2.1 For any QCSP instance φ, there exists an untyped equivalent instance φ′ . Moreover, if CN (φ) is a binary network, φ′ can be computed in polynomial time.

Notice that going from typed to untyped instances may be exponential for non-binary networks, as the former setting allows more succinct and efficient representations.

We remark that all complexity results in this paper hold for both settings. Indeed, we prove membership results and provide algorithms for the general typed setting, and prove hardness results by using either binary networks, or a unique binary domain for all variables.

We say that a class S of hypergraphs has the bounded hypertree width property, denoted by BHTW, if there is a k > 0 such that every hypergraph in S has hypertree width at most k [Gottlob et al., 2000]. Similarly, we define the property BTW, meaning bounded treewidth [Robertson and Seymous, 1986] of the primal graph (of the constraint hypergraph), and the property BITW, meaning bounded treewidth of the incidence graph. Moreover, we say that a class S of hypergraphs has the small hypertree width property, denoted by SHTW, if the hypertree width of every hypergraph H ∈ S is at most log |H|. The small treewidth property STW of primal graphs is defined similarly. We also consider the property ACYCLIC (resp., TREES) of any class of acyclic hypergraphs (resp., primal graphs).

We study how the complexity of QCSPs change as a function of quantifier alternations and of constraint structures. Moreover, we distinguish the case of arbitrary domains, denoted by ANY, and of binary domains, denoted by {0, 1}.

Let ¯Q be a string of quantifier alternations, S a hypergraphs property, and D a domain property in {ANY, {0, 1}}. Then, QCSP( ¯Q, S,D) is the problem of deciding whether an instance φ ∈ class ( ¯Q, S,D) is satisfiable, where class ( ¯Q, S, D) is any class of QCSP instances over domains of kind D, with alternation prefix ¯Q, and whose associated hypergraphs have property S.

3 Structural methods do not help very much

3.1 Some tractable instances

From [Gottlob et al., 2000], we already know that QCSP(∃, BHTW, ANY) is in polynomial time, and the same holds for any structural restriction stronger than bounded hypertree-width. Moreover, it is easy to see that QCSP(∀, BHTW, ANY) is even easier. We next show that also QCSP(∃∀, BHTW, ANY) is tractable.

Let φ be a QCSP instance, I = (Var, U, C) the constraint network of φ, and ¯ Y be a set of universally quantified variables. Let r( ¯X, ¯ Y ′ ) a constraint of I over variable sets ¯X and ¯ Y ′ , where ¯ Y ′ is the set of ¯ Y variables occurring in the scope of r. Denote by cart ( ¯ Y ′ ) the relation containing all combination of values from the domains of variables in ¯ Y ′ , i.e., cart ( ¯ Y ′ ) = ×Y ∈ fi Y ′U(Y ).

Then, define ¯ Y-red (r) as the relation containing all and only those tuples t of relation r such that, for any combination t′ of values for variables ¯ Y ′ , t[ ¯X] · t′ ∈ r. Note that, for the special case ¯ Y ′ = ∅, we get ¯ Y-red (r) = r; for the special case ¯X′ = ∅, we simply require all combinations of values for ¯ Y ′ , that is, ¯ Y-red (r) = r, if r is precisely cart ( ¯ Y ′ ), otherwise it is the empty relation.

Denote by ¯ Y-red (φ) the QCSP obtained from φ by replacing each constraint relation r by ¯ Y-red (r).

Lemma 3.1 For any QCSP φ and set of universally quantified variables ¯ Y , ¯ Y-red (φ) can be computed in logspace.

After the above lemma and exploiting the fact that no useful assignment is lost with this transformation, we can show the following.

Theorem 3.2 QCSP(∃∀, BHTW, ANY) is in polynomial time. Moreover, it is LOGCFL-complete, and hence tractable and parallelizable.

3.2 Encoding Boolean formulas as acyclic QCSPs

To any CNF formula Φ = c1 ∧. . .∧cm over Boolean variables ¯ V = {V1, . . . , Vn}, we associate a binary acyclic constraint network I(Φ) = (Var, U, C) . This constraint network will be used hereafter for characterizing the complexity of acyclic and quasi-acyclic quantified CSPs.

Consider the following CNF formula, that we use as a running example: ¯Φ = (V1 ∨ V2 ∨ V3) ∧ (V1 ∨ ¬V4) ∧ (V1 ∨ V6 ∨ V4) ∧ (V2 ∨ V6). Then, Figure 2 shows the constraint structure (i.e. the constraint hypergraph) of I( ¯Φ). Note that in this case hypergraph and primal graph representations coincide, as CN ( ¯Φ) contains only binary constraints.

The set of variables Var is the union of a set of clause variables ¯ C = {Cj | 1 ≤ j ≤ m} corresponding to the m clauses of Φ, of a set ¯B = {Bi | Vi ∈ ¯ V }, corresponding to the n Boolean variables occurring in Φ, and of two sets ¯ Sc = {Sc j , | 1 ≤ j ≤ m1} and ¯ Sv = {Sv i , | 1 ≤ i ≤ n1} of special variables, called clause selectors and variable selectors, respectively.

For a variable Vi of Φ, the domain of I(Φ) contains literal constants vi and ¬vi associated with its truth-values. Moreover, for any clause cj in which Vi occurs, the domain of I(Φ) contains a literal constant in {vj i , ¬vj i } encoding the truth value for Vi that makes cj true. We denote by li (resp., lj i ) any of these (positive or negative) literals, and by ¬li (resp., ¬lj i ) its complement. Moreover, we denote by satLit (cj) the set of literals that make cj true. E.g., for c2 = (V1 ∨¬V4) in ¯Φ, satLit (c2) = {v2 , ¬v2 4 }.

1 In more detail, the domains of I(Φ) variables are the following: for any variable Cj (corresponding to clause cj of Φ), U(Cj) = satLit (cj); for any Boolean variable Bi, U(Bi) = {vi, ¬vi}; for any clause-selector Sc j , U(Sc j ) = ⋃j ′≥j U(Cj ′ ); finally, for any variable-selector Sv i , U(Sv i ) = ⋃i′≥i U(Bi′ ).

Intuitively, Boolean variables encode a truth-value assignment to Φ, whereas any clause variable Cj chooses some literal in satLit (cj) that satisfies it. Any selector variable may take a value coming from either variable connected to it. Thus, any choice of all variable selectors corresponds to the propagation of a literal value li coming from some Boolean variable Bi in the left branch. Similarly, any choice of clause selectors corresponds to the propagation in the right branch of some literal ljk satisfying some clause cj. If for all possible propagations from both branches, no pair li, ¬lj i of complementary literals meets at the topmost constraint of the network, then the values of Boolean variables encode a satisfying truth-value assignment for Φ. We next describe the constraints in C that implement the above idea, where the indices i and i′ actually are values in the interval [1 . . . n] and where the indices j, j ′ are values in [1 . . .m].

• The topmost constraint (Sv 1 , Sc 1 ), called evaluate, has a constraint relation consisting of {(li, ¬lj i ) | lj i ∈ satLit (cj)}. Note that evaluate is satisfied only by assignments where its variables take complementary literals.
• For any constraint (Sv i , Bi) between a variable-selector Sv i and a Boolean variable Bi, its constraint relation consists of the tuples: {(li, li)} ∪ {(li′ , li) | i′ > i}.
• For any constraint between a pair of adjacent variableselectors (Sv i , Sv i+1 ) and for the constraint (Sv i ,Bn) with i = n - 1, the constraint relation is {(li′ , li′ ) | i′ > i} ∪ {(li, li′ ) | i′ > i}.
• For any constraint (Sc j ,Cj) between a clause-selector Sc j and a clause variable Cj, its constraint relation consists of the tuples: {(ljh , ljh ) | ljh ∈ satLit (cj)} ∪ {(lj ′ k , ljh ) | ljh ∈ satLit (cj), lj ′ k ∈ satLit (cj ′ ), j ′ > j}.
• For any constraint between a pair of adjacent clauseselectors (Sc j , Sc j+1 ) and for the constraint (Sc j , Cm) with j = m - 1, the constraint relation consists of the tuples: {(lj ′ h , lj ′ h ) | lj ′ h ∈ satLit (cj ′ ), j ′ > j} ∪ {(ljk , lj ′ h ) | ljk ∈ satLit (cj), lj ′ h ∈ satLit (cj ′ ), j ′ > j}.

If µ is a truth-value assignment for all variables ¯ V of Φ, then, σµ, denotes the assignment such that σµ(Bi) = vi if µ(Vi) = true, and σµ(Bi) = ¬vi if µ(Vi) = false.

Lemma 3.3 Let µ be a truth-value assignment for all variables ¯ V of Φ and σµ the corresponding assignment for ¯B. Then, µ is a satisfying assignment for Φ if and only if there exists an assignment σ′ ∈ ext (σµ, ¯ C) such that, for every σ′′ ∈ ext (σ′ , ¯ Sv ∪ ¯ Sc ), σ′′ ̸|= I(Φ) holds.

After this lemma, we immediately get that, even for acyclic binary constraint networks with just two quantifier alternations, solving a quantified CSP is intractable.

Theorem 3.4 QCSP(∀∃, TREES, ANY) is co-NP-hard.

Proof. From a CNF Boolean formula Φ, we build in polynomial time QC(Φ) = ∀ ¯B, ¯ C ∃¯ S I(Φ), where I(Φ) is the acyclic constraint network associated with Φ. From Lemma 3.3, satisfying assignments for Φ are in one-to-one correspondence with assignments to the variables in ¯B and ¯ C such that all their complete extensions do not satisfy I(Φ). Thus, Φ is not satisfiable iff QC(Φ) is satisfiable. ✷

3.3 Intractable acyclic instances

After having shown in the previous section the tractability for ∃∀ and the intractability for ∀∃, we now settle the complexity of acyclic QCSPs with arbitrary quantifier prefixes.

Theorem 3.5 For any natural number m ≥ 1,

1. QCSP((∀∃)m∀, BHTW, ANY) is ΠP2m-1 -complete, and hardness holds for QCSP((∀∃)m, TREES, ANY), too;
2. QCSP((∃∀)m∃∀, BHTW, ANY) is ΣP2m-complete, and hardness holds for QCSP((∃∀)m∃, TREES, ANY), too.

Proof. For space limitations we only prove Hardness for Point 2, here. For any m ≥ 1, consider the ΣP2m-complete problem of deciding whether a quantified Boolean formula Ψ′ = ∃V1∀V2 · · · ∀V2m¬Φ is satisfiable, where Φ is in CNF. From this formula, we build in polynomial time the following instance of QCSP((∃∀)m∃, TREES, ANY): QC(Ψ′ ) = ∃B1∀B2 · · · ∀B2m, ¯ C ∃¯ S I(Φ). From Lemma 3.3, it can be seen easily that Ψ′ is satisfiable iff QC(Ψ′ ) is satisfiable.

Membership. The proof is by induction. First observe that, given any instance Q = ∃ ¯ V1∀ ¯ V2φ of QCSP(∃∀, BHTW, ANY), its complementary problem Qc (deciding whether for all assignment σ to ¯ V1 there exists an extension to ¯ V2 that does not satisfy φ) is in LOGCFL and hence in polynomial time, by Theorem 3.2 and the fact that LOGCFL is closed under complementation. Then, we prove the basis of the induction, m = 1. The problem QCSP(∀∃∀, BHTW, ANY) is in ΠP1 = co-NP. Indeed, let Q = ∀¯ V1∃ ¯ V2∀ ¯ V3φ be any instance of this problem. Then, its complement can be decided in NP: guess an assignment σ to ¯ V1 and check that for all assignment σ′ ∈ ext (σ, ¯ V2) there is a complete assignment σ′′ ∈ ext (σ′ , ¯ V3) that does not satisfy all the constraints in φ. From the observation above, this check is feasible in polynomial time. Moreover, QCSP(∃∀∃∀, BHTW, ANY) is in ΣP2 , as any instance of this problem may be solved by a non-deterministic Turing machine with an oracle for QCSP(∀∃∀, BHTW, ANY). The induction step is a simple adaptation of the above reasoning for any m > 1. ✷

Corollary 3.6 The quantified constraint satisfaction problem (on arbitrary domain) is PSPACE-complete, even if restricted on constraint networks whose structure is a tree.

3.4 Fixed domain helps only with fixed arity

We now show that hypergraph acyclicity does not help in making easy the QCSP problem, even if we consider Boolean domains only. The same holds even in case we additionally require that the incidence graph has bounded treewidth, and the primal graph has small (logarithmic) treewidth. This entails that the problem remains intractable as long as we have non-fixed arities, even for very simple constraint interactions.

Theorem 3.7 For any natural number m ≥ 1,

• QCSP((∀∃)m, ACYCLIC ∩ BITW ∩ STW, {0, 1}) is ΠP2m-1 - complete;
• QCSP((∃∀)m∃, ACYCLIC ∩ BITW ∩ STW, {0, 1}) is ΣP2mcomplete.

Proof. Let Φ be a Boolean formula, and I(Φ) = (Var , U, C) its associated acyclic constraint network. We consider the network I ′ (Φ) = (Var ′ , {0, 1}, C ′ ), defined as follows. For each variable X ∈ Var, Var ′ contains |U(X)| distinct variables X1, ...,Xlog |U(X)|, with domain U ′ (Xi) = {0, 1} for each Xi. For each constraint r(X, Y ) in C, C ′ contains a constraint r′ (X1, ...,Xlog |U(X)|, Y1, ..., Ylog |U(Y )|), whose constraint relation is such that, for each tuple (xi, yj) in r, r′ contains the tuple (enc(xi), enc(yj)), where the string of bits enc(xi) (resp. enc(yj)) is the binary encoding of domain value xi (resp. xj). The right-bottom box in Figure 2 shows a portion of the constraint network I ′ ( ¯Φ) associated to the formula ¯Φ of our running example. Observe that the constraint network I ′ (Φ) is in ACYCLIC ∩ BITW ∩ STW. Indeed, the hypergraph associated to I ′ (Φ) is acyclic, and the number of variables in each hyperedge is bounded by 2 log c, where c is the size of largest domain over all the variables in Var. Therefore, the treewidth of the primal graph is at most 2 log c. Moreover, it is easy to check that the treewidth of the incidence graph of I ′ (Φ) is 3. Finally, observe that there exists a one-to-one correspondence between assignments to variables in I(Φ) and in I ′ (Φ), and thus the result immediately follows from Theorem 3.5. ✷

Corollary 3.8 The quantified constraint satisfaction problem is PSPACE-complete, even if restricted on Boolean constraint networks whose structure is in ACYCLIC ∩ BITW ∩ STW.

4 Guarded formulas and tractable CSPs

In this section, we describe a wide class of quantified constraint formulas that are tractable, even if there is no constant bound on domain sizes or quantifier alternations. Recall that any QCSP instance φ may be represented by a logical expression, as shown in Section 1 for QCSP φe. Technically, let us denote the pure logical formula of φ (without the encoding of relations, domains, etc.) by form(φ).

Following [Kolaitis et al., 2000], we denote by FO∧,+ the fragment of first order sentences where arbitrary quantifications and conjunctions are allowed, but where negations and disjunctions are forbidden. They observed that the existential fragment ∃FO∧,+ of FO∧,+ has the same expressive power as the constraint satisfaction problems. By allowing any kind of quantifiers, this observation may be clearly extended to the connection between general FO∧,+ formulas and quantified constraint formulas. Notice that, in this more general setting, there are different equivalent logical representation of the same instance. For example, one may use parentheses for distinguishing subformulas and delimiting quantifier scopes. In this section, we represent QCSPs by FO∧,+ formulas that are not necessarily in the traditional prenex form. Notice, however, that each FO∧,+ formula can be easily transformed into an equivalent prenex formula.

4.1 The fragment k-GQCSP of k-guarded QCSPs

We show that, for each constant k, a simple and appealing fragment of FO∧,+ is decidable in polynomial time. Since we have no bound on the number of variables in a formula, we assume w.l.o.g. that each variable is quantified over only once, i.e., quantified variables are not reused. In the following, we denote by free (ψ) the free variables of a logical formula ψ.

Definition 4.1 The class k-GQCSP of k-guarded QCSPs consists of those QCSPs instances φ whose formula form(φ) belongs to the fragment G∗k of FO∧,+ defined as follows. G∗k is the smallest subset of FO∧,+ such that:

• every atom belongs to G∗k ;
• if φ1 and φ2 ∈ G∗k , then φ1 ∧ φ2 ∈ G∗k ;
• let α1, . . . , αi be atoms, where i ≤ k, and let ψ be a formula in G∗k . If the free variables free (ψ) ⊆ var (α1) ∪ · · · ∪ var (αi), then, for each tuple of variables ¯ y and each quantifier Q ∈ {∃, ∀}, the formula ψ′ : Q¯ y(α1 ∧ · · · ∧ αi ∧ ψ) belongs to G∗k . The set of atoms {α1, . . . , αi} is referred to as the guard of ψ′ and is denoted by guard(ψ′ ). ✷

Example 4.2 Consider again QCSP instance φe presented in the Introduction, and the following equivalent instance, where form(φe) is rewritten as

• ψ = ∀S,X, Y, T,R,U, P( a(S,X, T,R) ∧ b(S, Y,U, P) ∧ ∃V f(R, P, V ) ∧ ∃Z ( g(X, Y ) ∧ c(T,U,Z) ∧ ∀W d(W,X,Z) ∧ e(Y,Z) ) )

This is a 2-guarded constraint formula, i.e., ψ ∈ G∗2 . The guard of formula ψ is guard(ψ) = {a(S,X, T,R), b(S, Y,U, P)}. For the formulas ψ1 = ∃V f(R, P, V ), ψ2 = ∃Z ( g(X, Y ) ∧ c(T,U,Z) ∧ ∀W d(W,X,Z) ∧ e(Y,Z) ) and ψ3 = ∀W d(W,X,Z), we have the following guards: guard(ψ1) = {f(R, P, V )}, guard(ψ2) = {g(X, Y ), c(T,U,Z)}, and guard(ψ3) = {d(W,X,Z)}. ✷

Note that the above definition of k-guardedness is congenial to the specific syntax of quantified CSPs and differs from that of k-guarded first order logic [Andreka et al., 1998; Gr¨ adel, 1999]. In the standard formalisms of the guarded fragment GF of first order logic or of the k-guarded fragment GFk of first order logic [Gottlob et al., 2003], the guards of an existentially quantified subformula ψ are added conjunctively to ψ (guard(ψ) ∧ ψ), just as for G∗k . However, the guards of a universal formula ψ are added in form of an implication: guard(ψ) → ψ. This is much more natural, since these logics have negation and guardedness needs to be correctly preserved under negations. For example, the negation of a guarded formula ¬∃¯ Y (g( ¯ Y ) ∧ ψ( ¯ Y )) is logically equivalent to ∀¯ Y (g( ¯ Y ) → ¬ψ( ¯ Y )). Since the logic FO∧,+ of constraint formulas has conjunction (∧) as unique binary connective, it is syntactically impossible to express an implication guard(ψ) → ψ in FO∧,+ (in fact, this is also semantically impossible). On the other hand, since negation is missing in FO∧,+, no problems involving "wrong guards" can arise through negation when using the natural (but nonstandard) guards introduced for the above defined fragments G∗k of FO∧,+.

For the k-guarded fragment GFk of first order logic (i.e., for the standard k-guarded fragment) the following tractability result was shown in [Gottlob et al., 2003]:

Proposition 4.3 The combined complexity of evaluating a GFk formula φ over a set of finite relations D is in O(|φ| × |D|k ).

Let us now show that also the class k-GQCSP of kguarded QCSPs is tractable, notwithstanding the "nonstandard" guards for universally quantified subformulas.

Lemma 4.4 There is an algorithm TRANSFORM which for each QCSP φ ∈ k-GQCSP computes a pair (D, φ∗ ) where D is a finite database and φ∗ ∈ GFk, such that φ is satisfied iff D |= φ∗ . The TRANSFORM algorithm runs in logspace.

Proof. Let φ ∈ k-GQCSP, and let R be the set of constraint relations of CN (φ). Consider a subformula ψ′ = ∀ ¯ Y (guard(ψ) ∧ ψ) of form(φ), where ∀ ¯ Y is a maximal prefix of universally quantified variables, and where guard(ψ) is a conjunction of m atoms ri( ¯ Yi, ¯ Xi), with 1 ≤ i ≤ m ≤ k, where ¯ Yi are the variables in its scope included in ¯ Y , and ¯ Xi its other variables, hence ¯ Xi ∩ ¯ Y = ∅. For 1 ≤ i ≤ m, we denote by ri↓ the relation obtained from the constraint relation ri by keeping all ¯ Yi-columns and projecting out all ¯ Xi columns, i.e., ri↓ := ∏ fi Yi ri.

Assume that for some 1 ≤ i ≤ m, ri↓ is not equal to the Cartesian product cart ( ¯ Yi) of ¯ Yi domains. That is, ri↓ does not consist of precisely all possible combinations of constants for all ¯ Y variables occurring in ri. Then one tuple ¯a of such constants is not in ri ↓ and thus the atom ri( ¯ Yi, ¯ Xi) cannot be satisfied for the substitution ¯ Yi = ¯a. Since ri occurs positively in φ, φ cannot be satisfied. The key observation is thus that, whenever φ is satisfied, for 1 ≤ i ≤ m, ri ↓ must be equal to cart ( ¯ Yi). Algorithm TRANSFORM starts by checking whether this is true. From Lemma 3.1, this check can be implemented to run in logspace: just compute ¯ Y-red (ri ↓), and check that it is not empty. If this test fails for at least one guard relation ri, then TRANSFORM outputs the formula false. Otherwise, let gψ be a new constraint atom with constraint scope ¯ Y , whose relation is the join of the ri↓ relations. Now, consider the set of free variables ¯X = free (ψ′ ). If ¯X ̸= ∅, since φ is a k-guarded formula, there are at most k atoms in φ that cover ¯X. Let gψ′ be a new constraint atom with constraint scope ¯X, whose relation is the projection over ¯X of the join of these guard atoms. Moreover, let g be a new constraint atomwith constraint scope ¯X ∪ ¯ Y , whose relation is the join of gψ and gψ′ (or just gψ, if ¯X is empty). Note that, since k is fixed, TRANSFORM may compute g from its input φ in logspace. Then, TRANSFORM replaces our subformula ψ′ = ∀¯ Y (guard(ψ)∧ψ) by the equivalent subformula ψ′′ = ∀¯ Y (g → guard(ψ) ∧ ψ). Note that this transformation does not change the set of free variables, as free (ψ′ ) = free (ψ′′ ). Thus, the set of atoms that cover these variables and acts as the guard of ψ′ in form(φ) will be the guard of ψ′′ in the new formula.

After having done this for all universal guarded subformulas, TRANSFORM has generated a formula φ∗ ∈ GFk. Let D the database consisting of all constraint relations of CN (φ) plus all relations like g computed for modifying the universal quantifications. It can be seen that φ is satisfiable iff D |= φ∗ . Moreover, the entire algorithm runs in logspace. ✷

Theorem 4.5 For each fixed k, the satisfiability of any QCSP in the class k-GQCSP can be checked in polynomial time.

Proof. Follows from Lemma 4.4 and Proposition 4.3. ✷

4.2 Extending the k-GQCSP fragment

When looking at the fragment k-GQCSP, and even more generally, at QCSPs in which universal quantifiers appear, we observe that the expressive power of universal quantification is rather poor. In fact, as already observed in the proof of Lemma 4.4, a subformula ∀¯ Y r( ¯ Y , ¯X) can only be true if the projection over ¯ Y of r is equal to the cartesian product cart ( ¯ Y ) representing the set of all tuples that can be composed from all possible domain elements from the respective domains. This is a rather stringent condition. On the other hand, by standard k-guards of the form (r1 ∧ r2 ∧ · · · ∧ rm) → ψ, we can express some other interesting properties. For example by standard guards, one may express an inclusion dependency stating that part of one constraint relation must be contained in another constraint relation. To add expressive power, we thus suggest to allow the use of standard guards together with conjunctively specified guards (for universally quantified subformulas). We thus define the fragment k-GQCSP+ just as k-GQCSP in Definition 4.1 with the following addition: If the free variables free (ψ) ⊆ var (α1) ∪ · · · ∪ var (αi), then, for each tuple of variables ¯ y the formula ψ′ : ∀¯ y(((α1 ∧ · · · ∧ αi) → ψ) belongs to G∗k .

After the results in Section 4.1, it is easy to see that, for each fixed k, the satisfiability of any QCSP in the class k-GQCSP+ can be checked in polynomial time. Moreover, we are able to show that k-GQCSP+ is strictly more expressive than k-GQCSP (for space reasons, we defer the proof to the full paper).