Let A be an idempotent algebra on a finite domain. We combine results of Chen [11], Zhuk [24] and Carvalho et al. [7] to argue that if A satisfies the polynomially generated powers property (PGP), then QCSP(Inv(A)) is in NP. We then use the result of Zhuk to prove a converse, that if Inv(A) satisfies the exponentially generated powers property (EGP), then QCSP(Inv(A)) is co-NP-hard. Since Zhuk proved that only PGP and EGP are possible, we derive a full dichotomy for the QCSP, justifying the moral correctness of what we term the Chen Conjecture (see [12]). We examine in closer detail the situation for domains of size three. Over any finite domain, the only type of PGP that can occur is switchability. Switchability was introduced by Chen in [11] as a generalisation of the already-known Collapsibility [9]. For three-element domain algebras A that are Switchable, we prove that for every finite subset ∆ of Inv(A), Pol(∆) is Collapsible. The significance of this is that, for QCSP on finite structures (over three-element domain), all QCSP tractability explained by Switchability is already explained by Collapsibility. Finally, we present a three-element domain complexity classification vignette, using known as well as derived results.  ACM Subject Classification F.2.2 Nonnumerical Algorithms and Problems Keywords and phrases A large body of work exists from the past twenty years on applications of universal algebra to the computational complexity of constraint satisfaction problems (CSPs) and a number of celebrated results have been obtained through this method. One considers the problem CSP(B) in which it is asked whether an input sentence ϕ holds on B, where ϕ is primitive positive, that is using only ∃, ∧ and =. The CSP is one of a wide class of model-checking problems obtained from restrictions of first-order logic. For almost every one of these classes, we can give a complexity classification [18]: the two outstanding classes are CSPs and its popular extension quantified CSPs (QCSPs) for positive Horn sentences -where ∀ is also present -which is used in Artificial Intelligence to model non-monotone reasoning or uncertainty [15]. The outstanding conjecture in the area is that all finite-domain CSPs are either in P or are NP-complete, something surprising given these CSPs appear to form a large microcosm of NP, and NP itself is unlikely to have this dichotomy property. This Feder-Vardi conjecture [16], given more concretely in the algebraic language in [6], remains unsettled, but is now Conjecture 1 (Chen Conjecture). Let B be a finite relational structure expanded with all constants. If Pol(B) has PGP, then QCSP(B) is in NP; otherwise QCSP(B) is Pspacecomplete. In [12], Conjecture 6 gives the NP membership and Conjecture 7 the Pspace-completeness. We now know from [24] and [7] that the NP membership of Conjecture 6 is indeed true. The most interesting result of this paper is Theorem 1 below, but note that we permit infinite signatures (languages) although our domains remain finite. This aspect of our work will be discussed in detail later. Zhuk has previously proved [24] that only the cases PGP and EGP may occur, as well even in the non-idempotent case. With infinite languages, the NP-membership for Theorem 1 is no longer immediate from [7], but requires a little extra work. We are also able to refute the following form. Conjecture 2 (Alternative Chen Conjecture). Let A be an idempotent algebra on a finite domain A. If A satisfies PGP, then for every finite subset ∆ ⊆ Inv(A), QCSP(∆) is in NP. Otherwise, there exists a finite subset ∆ ⊆ Inv(A) so that QCSP(∆) is co-NP-hard. In proving Theorem 1 we are saying that the complexity of QCSPs, with all constants included, is classified modulo the complexity of CSPs. In this manner, our result follows in the footsteps of the similar result for the Valued CSP, which has also had its complexity classified modulo the CSP, as culminated in the paper [17]. For a finite-domain algebra A we associate a function f A : N → N, giving the cardinality of the minimal generating sets of the sequence A, for all m. The question then arises as to the growth rate of f and specifically regarding the behaviours constant, logarithmic, linear, polynomial and exponential. Wiegold proved in [23] that if A is a finite semigroup then f A is either linear or exponential, with the former prevailing precisely when A is a monoid. This dichotomy classification may be seen as a gap theorem because no growth rates intermediate between linear and exponential may occur. We say A enjoys the polynomially generated powers property (PGP) if there exists a polynomial p so that f A = O(p) and the exponentially generated powers property (EGP) if there exists a constant b so that f A = Ω(g) where Thus, a 1 , a 2 , . . . , a k are the indices where the tuple switches value. Note that these are not the original definitions, which we will see shortly, but they are proved equivalent to the original definitions (at least for finite signatures) in [7]. Moreover, these are the definitions that we will use. We say that A is collapsible (switchable) if there exists k such that it is k-collapsible (k-switchable). We note that Zhuk uses this definition of switchability in [24] in which he proved that the only kind of PGP for finite-domain algebras is switchability. Let us capitalise Collapsibility and Switchability to indicate Chen's original definitions from [11] are used, following an example for arithmetic versus Arithmetic by Raymond Smullyan in [22]. There is the potential for confusion at the start of the sentence but, as was the case with Smullyan, the two will transpire to be interchangeable throughout our discourse. It is straightforward to see that k-Switchability implies k-switchability and k-Collapsibility implies k-collapsibility. The converses, for finite signatures, also hold, but this requires rather more work [7]. For any finite algebra, k-Collapsibility implies k-Switchability. and for any 2-element algebra, k-Switchability implies k-Collapsibility. Chen originally introduced Switchability because he found a 3-element algebra that enjoyed the PGP but was not Collapsible [11]. He went on to prove that Switchability of A implies that the corresponding QCSP is in P, what one might informally state as QCSP(Inv(A)) in P, where Inv(A) can be seen as the structure over the same domain as A whose relations are precisely those that are preserved by (invariant under) all the operations of A. However, the QCSP was traditionally defined only on finite sets of relations (else the question arises as to encoding), thus a more formal definition might be that, for any finite subset ∆ of Inv(A), QCSP(∆) is in P. What we prove in this paper is that, as far as the QCSP is concerned, Switchability on a three-element algebra A is something of a mirage. What we mean by this is that when A is Switchable, for all finite subsets ∆ of Inv(A), already Pol(∆) is Collapsible. Thus, for QCSP complexity for three-element structures, we do not need the additional notion of Switchability to explain tractability, as Collapsibility will already suffice. Since these notions were originally introduced in connection with the QCSP this is particularly surprising. Note that the parameter k of Collapsibility is unbounded over these increasing finite subsets ∆ while the parameter of Switchability clearly remains bounded. In some way we are suggesting that Switchability itself might be seen as a limit phenomenon of Collapsibility. Our use of infinite languages (i.e. signatures, since we work on a finite domain) is the only controversial part of our discourse and merits special discussion. We wish to argue that a necessary corollary of the algebraic approach to (Q)CSP is a reconciliation with infinite languages. The traditional approach to consider arbitrary finite subsets of Inv(A) is unsatisfactory in the sense that choosing this way to escape the -naturally infinite -set Inv(A) is as arbitrary as the choice of encoding required for infinite languages. However, the difficulty in that choice is of course the reason why this route is often eschewed. The first possibility that comes to mind for encoding a relation in Inv(A) is probably to list C V I T 2 0 1 6 23:4 The complexity of quantified constraints using the algebraic formulation its tuples, while the second is likely to be to describe the relation in some kind of "simple" logic. Both these possibilities are discussed in [14], for the Boolean domain, where the "simple" logic is the propositional calculus. For larger domains, this would be equivalent to quantifier-free propositions over equality with constants. Both Conjunctive Normal Form (CNF) and Disjunctive Normal Form (DNF) representations are considered in [14] and a similar discussion in [3] exposes the advantages of the DNF encoding. The point here is that testing non-emptiness of a relation encoded in CNF may already be NP-hard, while for DNF this will be tractable. Since DNF has some benign properties, we might consider it a "nice, simple" logic while for "simple" logic we encompass all quantifier-free sentences, that include DNF and CNF as special cases. The reason we describe this as "simple" logic is to compare against something stronger, say all first-order sentences over equality with constants. Here recognising non-emptiness becomes Pspace-hard and since QCSPs already sit in Pspace, this complexity is unreasonable. For the QCSP over infinite languages Inv(A), Chen and Mayr [13] have declared for our first, tuple-listing, encoding. In this paper we will choose the "simple" logic encoding, occasionally giving more refined results for its "nice, simple" restriction to DNF. Our choice of the "simple" logic encoding over the tuple-listing encoding will ultimately be justified by the (Revised) Chen Conjecture holding for "simple" logic yet failing for tuple-listings. Note that our demonstration of the (Revised) Chen Conjecture for infinite languages with the "simple" logic encoding does not resolve the original Chen Conjecture for finite languages B with constants because QCSP(Inv(Pol(B))) could conceivably have higher complexity than QCSP(B) due to a succinct representation of relations in Inv(Pol(B)). Indeed, this belies one justification for the preferential study of finite subsets of Inv(Pol(B)), since for finite signature B we can then say QCSP(B) and QCSP(Inv(PolB)) must have the same complexity. Note that for finite relational bases B , B of Inv(Pol(B)), QCSP(B ) and QCSP(B ) must have the same complexity. Further, we do not know of any concrete finite B with constants, so that QCSP(Inv(Pol(B))) and QCSP(B) have different complexity. Let us consider examples of our encodings. For the domain {1, 2, 3}, we may give a binary relation either by the tuples {(1, 2), (2, 1), (2, 3), (3, 2), (1, 3), (3, 1), (1, 1)} or by the "simple" logic formula (x = y ∨ x = 1). For the domain {0, 1}, we may give the ternary (not-all-equal) relation by the tuples {(1, 0, 0), (0, 1, 0), (0, 0, 1), (1, 1, 0), (1, 0, 1), (1, 1, 0)} or by the "simple" logic formula (x = y ∨ y = z). In both of these examples, the simple formula is also in DNF. Nota Bene. The results of this paper apply for the "simple" logic encoding as well as the "nice, simple" encoding in DNF except where specifically stated otherwise. These exceptions are Proposition 2 and Corollary 10 (which uses the "nice, simple" DNF) and Proposition 4 (which uses the tuple encoding). This paper is the merger of [20, 19], neither of which was submitted for publication, considerably extended. Let [k] := {1, . . . , k}. A k-ary polymorphism of a relational structure B is a homomorphism f from B k to B. Let Pol(B) be the set of polymorphisms of B and let Inv(A) be the set of relations on A which are invariant under (each of) the operations of some finite algebra A. Pol(B) is an object known in Universal Algebra as a clone, which is a set of operations C. Carvalho et al. containing all projections and closed under composition (superposition). A term operation of an algebra A is an operation which is a member of the clone generated by A. We will conflate sets of operations over the same domain and algebras just as we do sets of relations over the same domain and constraint languages (relational structures). Indeed, the only technical difference between such objects is the movement away from an ordered signature, which is not something we will ever need. A reduct of a relational structure B is a relational structure B over the same domain obtained by forgetting some of the relations. If ∆ is some finite subset of Inv(A), then we may view ∆ a being a finite reduct of the structure (associated with) Inv(A). A We recall QCSP(B), where B is some structure on a finite-domain, is a decision problem with input φ, a pH-sentence (i.e. using just ∀, ∃, ∧ and =) involving (a finite set of) relations of B, encoded in propositional logic with equality and constants. The yes-instances are those φ for which B |= φ. If the input sentence is restricted to have alternation Π k then the corresponding problem is designated Π k -CSP(B). We now recall some terminology due to Chen [9, 11], for his natural adaptation of the model checking game to the context of pH-sentences. We shall not need to explicitly play these games but only to handle strategies for the existential player. This will enable us to give the original definitions for Collapsibility and Switchability. An adversary B of length m ≥ 1 is an m-ary relation over A. When B is precisely the set B 1 × B 2 × . . . × B m for some non-empty subsets B 1 , B 2 , . . . , B m of A, we speak of a rectangular adversary (we will sometimes specify this as a tuple rather than a product). Let φ be a pH-sentence with universal variables x 1 , . . . , x m and quantifier-free part ψ. We write A |= φ B and say that the existential player has a winning strategy in the (A, φ)-game against adversary B iff there exists a set of Skolem functions {σ x : '∃x' ∈ φ} such that for any assignment π of the universally quantified variables of φ to A, where π(x 1 ), . . . , π(x m ) ∈ B, the map h π is a homomorphism from D ψ (the canonical database) to A, where , if x is a universal variable; and, (Here, Y x denotes the set of universal variables preceding x and π| Yx the restriction of π to Y x .) Clearly, A |= φ iff the existential player has a winning strategy in the (A, φ)-game against the so-called full (rectangular) adversary A × A × . . . × A (which we will denote hereafter by A m ). We say that an adversary B of length m dominates an adversary B of length m when B ⊆ B. Note that B ⊆ B and A |= φ B implies A |= φ B . We will also consider sets of adversaries of the same length, denoted by uppercase Greek letters as in Ω m (here the length is m); and, sequences thereof, which we denote with bold uppercase Greek letters as in Ω = Ω m m∈N . We will write A |= φ Ωm to denote that A |= φ B holds for every adversary B in Ω m . Let f be a k-ary operation of A and A, B 1 , . . . , B k be adversaries of length m. We say that A is reactively composable from the adversaries B 1 , . . . , B k via f , and we write A f (B 1 , . . . , B k ) iff there exist partial functions g The complexity of quantified constraints using the algebraic formulation for every j in [k], the values g a 2 ) . Reactive composition plays a key role in the proof of our main theorem but its use appears only in other papers that we will cite. Ordinary composition is the only type of reactive composition that will be used in this paper. The Chen Conjecture We need to revisit the main result of [7] to show that it holds not just for finite signatures but for infinite signatures also. In its original the following theorem discussed "projective sequences of adversaries, none of which are degenerate". This includes Switching adversaries and we give it in this latter form. We furthermore remove some parts of the theorem that are not currently relevant to us. [(i ) ⇒ (i).] By contraposition, if (i) fails then it fails on some specific pH-sentence ψ which only mentions a finite number of relations of A . Thus (i ) also fails on some finite reduct of A mentioning these relations. [(vi ) ⇒ (vi m . Note that in (vi ) ⇒ (vi) above we did not need to argue uniformly across the different (a 1 , . . . , a m ) and it is enough to find an infinitely recurring operation for each of these individually. The following result is essentially a corollary of the works of Chen and Zhuk [11, 24] via [7]. Proof. We know from Theorem 7 in [24] that A is Switchable, whereupon we apply Corollary 5, (vi) ⇒ (i). By considering instances whose universal variables involve only the polynomial number of tuples from the Switching Adversary, one can see that QCSP(Inv(A)) reduces to a polynomial number of instances of CSP(Inv(A)) and is therefore in NP. Further details of the NP algorithm are given in Corollary 38 of [7] but the argument here follows exactly Section 7 from [11], in which it was originally proved that Switchability yields the corresponding QCSP in NP. Note that Chen's original definition of Switchability, based on adversaries and reactive composability, plays a key role in the NP membership algorithm in Theorem 6. It is the result from [7] that is required to reconcile the two definitions of switchability as equivalent, and indeed Corollary 5 is needed in this process for infinite signatures. If we were to use just our definition of switchability then it is only possible to prove, à la Proposition 3.3 in [11], that the bounded alternation Π n -CSP(Inv(A)) is in NP. Thus, using just the methods from [11] and [24], we can not prove the Revised Chen Conjecture, but rather some bounded alternation (re)revision. Suppose there exist α, β strict subsets of A so that α ∪ β = A, define the relation Strictly speaking, the α and β are parameters of τ k but we dispense with adding them to the notation since they will be fixed at any point C V I T 2 0 1 6 23:8 The complexity of quantified constraints using the algebraic formulation in which we invoke the τ k . The purpose of the relations τ k is to encode co-NP-hardness through the complement of the problem (monotone) 3-not-all-equal-satisfiability (3NAESAT). Let us introduce also the important relations σ k (x 1 , y 1  Proof. We will argue that τ k is definable by the conjunction Φ of 3 k instances of σ k that each consider the ways in which two variables may be chosen from each of the ( where ∼ is infix for ρ) . We need to show that this conjunction Φ entails τ k (the converse is trivial). We will assume for contradiction that Φ is satisfiable but τ k not. In the first instance of σ k of Φ some atom must be true, and it will be of the form x i ∼ y i or y i ∼ z i or x i ∼ z i . Once we have settled on one of these three, p i ∼ q i , then we immediately satisfy 3 k−1 of the conjunctions of Φ, leaving 2 · 3 k−1 unsatisfied. Now, we can not evaluate true any of the others among contradicting our assumption. Thus we are now down to looking at variables with subscript other than i and in this fashion we have made the space one smaller, in total k − 1. Now, we will need to evaluate in Φ some other atom of the form x j ∼ y j or y j ∼ z j or x j ∼ z j , for j = i. Once we have settled on one of these three then we immediately satisfy 2 · 3 k−2 of the conjunctions remaining of Φ, leaving 2 2 · 3 k−2 still unsatisfied. Iterating this thinking, we arrive at a situation in which 2 k clauses are unsatisfied after we have gone through all k subscripts, which is a contradiction. Proof. We know from Lemma 11 in [24] that there exist α, β strict subsets of A so that α ∪ β = A and the relation σ k is in Inv(A), for each k ∈ N. From Lemma 7, we know also that τ k is in Inv(A), for each k ∈ N. We will next argue that τ k enjoys a relatively small specification in DNF (at least, polynomial in k). We first give such a specification for ρ (x, y, z). which is constant in size when A is fixed. Now it is clear from the definition that the size of τ n is polynomial in n. We will now give a very simple reduction from the complement of 3NAESAT to QCSP(Inv(A)). 3NAESAT is well-known to be NP-complete [21] and our result will follow. Take an instance φ of 3NAESAT which is the existential quantification of a conjunction of k atoms NAE (x, y, z). Thus ¬φ is the universal quantification of a disjunction of k atoms x = y = z. We build our instance ψ of QCSP(Inv(A)) from ¬φ by transforming the quantifier-free part (¬φ ∈ co-3NAESAT implies ψ ∈ QCSP(Inv(A)).) From an assignment to the universal variables v 1 , . . . , v m of ψ to elements x 1 , . . . , x m of A, consider elements x 1 , . . . , x m ∈ {0, 1} according to , and x i ∈ α ∩ β implies we don't care, so w.l.o.g. say x i = 0. C. Carvalho et al. The disjunct that is satisfied in the quantifier-free part of ¬φ now gives the corresponding disjunct that will be satisfied in τ k . (ψ ∈ QCSP(Inv(A)) implies ¬φ ∈ co-3NAESAT.) From an assignment to the universal variables v 1 , . . . , v m of ¬φ to elements x 1 , . . . , x m of {0, 1}, consider elements x 1 , . . . , x m ∈ A according to x i = 0 implies x i is some arbitrarily chosen element in α \ β, and x i = 1 implies x i is some arbitrarily chosen element in β \ α. The disjunct that is satisfied in τ k now gives the corresponding disjunct that will be satisfied in the quantifier-free part of ¬φ. The demonstration of co-NP-hardness in the previous theorem was inspired by a similar proof in [2]. Note that an alternative proof that τ k is in Inv(A) is furnished by the observation that it is preserved by all αβ-projections (see [24]). We note surprisingly that co-NP-hardness in Theorem 8 is optimal, in the sense that some (but not all!) of the cases just proced co-NP-hard are also in co-NP. Proposition 1. Let α, β strict subsets of A := {a 1 , . . . , a n } so that α ∪ β = A and α ∩ β = ∅. Then QCSP(A; {τ k : k ∈ N}, a 1 , . . . , a n ) is in co-NP. Proof. Assume |A| > 1, i.e. n > 1 (note that the proof is trivial otherwise). Let φ be an input to QCSP(A; {τ k : k ∈ N}, a 1 , . . . , a n ). We will now seek to eliminate atoms v = a (a ∈ {a 1 , . . . , a n }) from φ. Suppose φ has an atom v = a. If v is universally quantified, then φ is false (since |A| > 1). Otherwise, either the atom v = a may be eliminated with the variable v since v does not appear in a non-equality relation; or φ is false because there is another atom v = a for a = a ; or v = a may be removed by substitution of a into all non-equality instances of relations involving v. This preprocessing procedure is polynomial and we will assume w.l.o.g. that φ contains no atoms v = a. We now argue that φ is a yes-instance iff φ is a yes-instance, where φ is built from φ by instantiating all existentially quantified variables as any a ∈ α ∩ β. The universal φ can be evaluated in co-NP (one may prefer to imagine the complement as an existential ¬φ to be evaluated in NP) and the result follows. In fact, this being an algebraic paper, we can even do better. Let B signify a set of relations on a finite domain but not necessarily itself finite. For convenience, we will assume the set of relations of B is closed under all co-ordinate projections and instantiations of constants. Call B existentially trivial if there exists an element c ∈ B (which we call a canon) such that for each k-ary relation R of B and each i ∈ [k], and for every x 1 , . . . , x k ∈ B, whenever (x 1 , . . . , We want to expand this class to almost existentially trivial by permitting conjunctions of the form v = a i or v = v with relations that are existentially trivial. Lemma 9. Let α, β be strict subsets of A := {a 1 , . . . , a n } so that α ∪ β = A and α ∩ β = ∅. The set of relations pp-definable in (A; {τ k : k ∈ N}, a 1 , . . . , a n ) is almost existentially trivial. Proof. Consider a formula with a pp-definition in (A; {τ k : k ∈ N}, a 1 , . . . , a n ). We assume that only free variables appear in equalities since otherwise we can remove these equalities by substitution. Now existential quantifiers can be removed and their variables instantiated as the canon c. Indeed, their atoms τ n may now be removed since they will always be satisfied. Thus we are left with a conjunction of equalities and atoms τ n , and the result follows. The complexity of quantified constraints using the algebraic formulation Proof. The argument here is quite similar to that of Proposition 1 except that there is some additional preprocessing to find out variables that are forced in some relation to being a single constant or pairs of variables within a relation that are forced to be equal. In the first instance that some variable is forced to be constant in a k-ary relation, we should replace with the (k − 1)-ary relation with the requisite forcing. In the second instance that a pair of variables are forced equal then we replace again the k-ary relation with a (k − 1)-ary relation as well as an equality. Note that projecting a relation to a single or two co-ordinates can be done in polynomial time because the relations are encoded in DNF. After following these rules to their conclusion one obtains a conjunction of equalities together with relations that are existentially trivial. Now is the time to propagate variables to remove equalities (or find that there is no solution). Finally, when only existentially trivial relations are left, all remaining existential variables may be evaluated to the canon c. Corollary 10. Let α, β be strict subsets of A := {a 1 , . . . , a n } so that α ∪ β = A and α ∩ β = ∅. Then QCSP(Inv(Pol(A; {τ k : k ∈ N}, a , . . . , a n ))) is in co-NP under the DNF encoding. This last result, together with its supporting proposition, is the only time we seem to require the "nice, simple" DNF encoding, rather than arbitrary propositional logic. We do not require DNF for Proposition 1 as we have just a single relation in the signature for each arity and this is easy to keep track of. We note that the set of relations {τ k : k ∈ N} is not maximal with the property that with the constants it forms a co-clone of existentially trivial relations. One may add, for example, α × β ∪ β × α. The following, together with our previous results, gives the refutation of the Alternative Chen Conjecture. Proposition 3. Let α, β strict subsets of A := {a 1 , . . . , a n } so that α ∪ β = A and α ∩ β = ∅. Then, for each finite signature reduct B of (A; {τ k : k ∈ N}, a 1 , . . . , a n ), QCSP(B) is in NL. Proof. We will assume B contains all constants (since we prove this case gives a QCSP in NL, it naturally follows that the same holds without constants). Take m so that, for each τ i ∈ B, i ≤ m. Recall from Lemma 7 that τ i is pp-definable in σ i . We will prove that the structure B given by (A; {σ k : k ≤ m}, a 1 , . . . , a n ) admits a (3m + 1)-ary near-unanimity operation f as a polymorphism, whereupon it follows that B admits the same near-unanimity polymorphism. We choose f so that all tuples whose map is not automatically defined by the near-unanimity criterion map to some arbitrary a ∈ α ∩ β. To see this, imagine that this f were not a polymorphism. Then some (3m + 1) tuples in σ i would be mapped to some tuple not in σ i which must be a tuple t of elements from α \ β ∪ β \ α. Note that column-wise this map may only come from (3m + 1)-tuples that have 3m instances of the same element. By the pigeonhole principle, the tuple t must appear as one of the (3m + 1) tuples in σ i and this is clearly a contradiction. It follows from [9] that QCSP(B) reduces to a polynomially bounded ensemble of n 3m · n · n 3m instances CSP(B), and the result follows. Proposition 4. Let α := {0, 1} and β := {0, 2}. Then, QCSP({0, 1, 2}; {τ k : k ∈ N}, 0, 1, 2) is in P under the tuple encoding. Proof. Consider an instance φ of this QCSP of size n involving relation τ m but no relation τ k for k > m. The number of tuples in τ m is > 3 m . Following Proposition 1 together with its C. Carvalho et al. proof, we may assume that the instance is strictly universally quantified over a conjunction of atoms (involving also constants). Now, a universally quantified conjunction is true iff the conjunction of its universally quantified atoms is true. We can further say that there are at most n atoms each of which involves at most 3m variables. Therefore there is an exhaustive algorithm that takes at most O(n · 3 3m ) steps with is O(n 4 ).
If we take the tuple-listing encoding of relations instead of quantifier-free logic with constants and equality, Theorem 5 is known to fail REF .
The Complexity of Quantified Constraints Using the Algebraic Formulation
MFCS
Computer Science Mathematics