Tractable Set Constraints

1 Introduction

Constraint satisfaction problems are computational problems where, informally, the input consists of a finite set of variables and a finite set of constraints imposed on those variables; the task is to decide whether there is an assignment of values to the variables such that all the constraints are simultaneously satisfied. Set constraint satisfaction problems are special constraint satisfaction problems where the values are sets, and the constraints might, for instance, force that one set y includes another set x, or that one set x is disjoint to another set y. The constraints might also be ternary, such as the constraint that the intersection of two sets x and y is contained in z, in symbols (x ∩ y) ⊆ z.

To systematically study the computational complexity of constraint satisfaction problems, it has turned out to be a fruitful approach to consider constraint satisfaction problems CSP(Γ) where the set of allowed constraints is formed from a fixed set Γ of relations R ⊆ Dk over a common domain D. This way of parametrizing the constraint satisfaction problem by a constraint language Γ has lead to many strong algorithmic results [Bulatov and Dalmau, 2006; Idziak et al., 2007; Barto and Kozik, 2009; Bodirsky and Kutz, 2007], and to

Alex Krimkevich

Stanford University Department of Computer Science Stanford, CA, USA

many powerful hardness conditions for large classes of constraint satisfaction problems [Schaefer, 1978; Bulatov et al., 2005; Bulatov, 2003; 2006; Bodirsky and K´ara, 2009].

A set constraint language Γ is a set of relations R ⊆ (P(N))k where the common domain D = P(N) is the set of all subsets of the natural numbers; moreover, we require that each relation R can be defined by a Boolean combination of equations over the signature ⊓, ⊔, and c, which are function symbols for intersection, union, and complementation, respectively. Details of the formal definition and many examples of set constraint languages can be found in Section 3. The choice of N is just for notational convenience; as we will see, we could have selected any infinite set for our purposes. In the following, a set constraint satisfaction problem (set CSP) is a problem of the form CSP(Γ) for a set constraint language Γ. It has been shown by Marriott and Odersky [Marriott and Odersky, 1996] that all set CSPs are contained in NP; they also showed that the largest set constraint language, which consists of all relations that can be defined as described above, has an NP-hard set CSP.

Drakengren and Jonsson [Drakengren and Jonsson, 1998] initiated the search for set CSPs that can be solved in polynomial time. They showed that CSP({⊆, ||, ̸=}) can be solved in polynomial time, where

• x ⊆ y holds iff x is a subset of or equal to y;
• x || y holds iff x and y are disjoint sets; and
• x ̸= y holds iff x and y are distinct sets.

They also showed that CSP(Γ) can be solved in polynomial time if all relations in Γ can be defined by formulas of the form

where x0, . . . , xk, y0, . . . , yk are not necessarily distinct variables. We will call the set of all relations that can be defined in this way Drakengren and Jonsson's set constraint language. It is easy to see that the algorithm they present runs in time quadratic in the size of the input.

On the other hand, Drakengren and Jonsson [Drakengren and Jonsson, 1998] show that if Γ contains the relations defined by formulas of the form

the problem CSP(Γ) is NP-hard.

Contributions and Outline. We present a significant extension of Drakengren and Jonsson's set constraint language (Section 3) whose CSP can still be solved in quadratic time in the input size (Section 6); we call this set constraint language EI. Unlike Drakengren and Jonsson's set constraint language, our language also contains the ternary relation defined by (x ∩ y) ⊆ z, which is a relation that is of particular interest in description logics - we will discuss this below. Moreover, we show that any further extension of EI contains a finite sublanguage with an NP-hard set CSP (Section 7), using concepts frommodel theory and universal algebra. In this sense, we present a maximal tractable class of set constraint satisfaction problems.

Our algorithm is based on the concept of independence in constraint languages which was discovered several times independently in the 90's [Koubarakis, 2001; Jonsson and B¨ackstr¨om, 1998; Marriott and Odersky, 1996] - also see [Broxvall et al., 2002; Cohen et al., 2000]; however, we apply this concept twice in a novel, nested way, which leads to a two level resolution procedure that can be implemented to run in quadratic time. The technique we use to prove the correctness of the algorithm is also an important contribution of our paper, and we believe that a similar approach can be applied in many other contexts; our technique is inspired by the already mentioned connection to universal algebra. Due to space limitations, all proofs have been omitted; they will appear in the long version of this paper.

Application Areas and Related Literature

Set Constraints for Programming Languages. Set constraints find applications in program analysis; here, a set constraint is of the formX ⊂ Y , where X and Y are set expressions. Examples of set expressions are 0 (denoting the empty set), set-valued variables, and union and intersection of sets, but also expressions of the form f(Z1, Z2) where f is a function symbol and Z1, Z2 are again set expressions. Unfortunately, the worst-case complexity of most of the reasoning tasks considered in this setting is very high, often EXPTIMEhard; see [Aiken, 1994] for a survey.

More recently, it has been shown that the quantifier-free combination of set constraints (without function symbols) and cardinality constraints (quantifier-free Pressburger arithmetic) has a satisfiability problem in NP [Kuncak and Rinard, 2007]. This logic (called QFBAPA) is interesting for program verification [Kuncak et al., 2006]. The question whether the approach presented in this paper can also be applied to search for polynomial-time tractable fragments of QFBAPA is left as an open problem.

Tractable Description Logics. Description logics are a family of knowledge representation formalisms that can be used to formalize and reason with concept definitions. The computational complexity of most of the computational tasks that have been studied for the various formalisms is usually quite high. However, in the last years a series of description logics (for example EL, EL++, Horn-FL0, and various extensions and fragments [K¨usters and Molitor, 2002; Baader et al., 2005; Kr¨otzsch et al., 2006]) has been discovered where crucial tasks such as e.g. entailment, concept satisfiability and knowledge base satisfiability can be decided in polynomial time.

Two of the basic assertions that can be made in EL++ and Horn-FL0 are C1||C2 (there is no C1 that is also C2) and C1 ∩ C2 ⊆ C3 (every C1 that is C2 is also C3), for concept names C1, C2, C3. These are EI set constraints, and the latter has not been treated in the framework of Drakengren and Jonsson. None of the description logics with a tractable knowledge base satisfiability problem contains all EI set constraints.

Spatial Reasoning. Several spatial reasoning formalisms (like RCC-5 and RCC-8) are closely related to set constraint satisfaction problems. These formalisms allow to reason about relations between regions; in the fundamental formalism RCC-5, one can think of a region as a non-empty set, and possible (binary) relationships are containment, disjointness, equality, overlap, and disjunctive combinations thereof. Thus, the exclusion of the empty set is the most prominent difference between the set constraint languages studied by Drakengren and Jonsson in [Drakengren and Jonsson, 1998] (which are contained in the class of set constraint languages considered here), and RCC-5 and its fragments.

2 Constraint Satisfaction Problems

To use existing terminology in logic and model theory, it will be convenient to formalize constraint languages as (relational) structures (see e.g. [Hodges, 1993]). A structure Γ is a tuple (D; f Γ 1 , f Γ 2 , . . . ,RΓ 1 , RΓ 2 , . . . ) where D is a set (the domain of Γ), each f Γ i is a function from Dki → D (where ki is called the arity of f Γ i ), and each RΓ i is a relation over D, i.e., a subset of Dli (where li is called the arity of RΓ i ). For each function f Γ i we assume that there is a function symbol which we denote by fi, and for each relation RΓ i we have a relation symbol which we denote by Ri. Constant symbols will be treated as 0-ary function symbols. The set τ of all relation and function symbols for some structure Γ is called the signature of Γ, and we also say that Γ is a τ-structure. If the signature of Γ only contains relation symbols and no function symbols, we also say that Γ is a relational structure. In the context of constraint satisfaction, relational structures Γ are also called constraint languages, and a constraint language Γ′ is called a sublanguage (or reduct) of a constraint language Γ if the relations in Γ′ are a subset of the relations in Γ (and Γ is called an expansion of Γ′ ).

Let Γ be a relational structure with domain D and a finite signature τ. The constraint satisfaction problem for Γ is the following computational problem, also denoted by CSP(Γ): given a finite set of variables V and a conjunction Φ of atomic formulas of the form R(x1, . . . , xk), where x1, . . . , xk ∈ V and R ∈ τ , does there exists an assignment s : V → D such that for every constraint R(x1, . . . , xk) in the input we have that (s(x1), . . . , s(xk)) ∈ RΓ?

The mapping s is also called a solution to the instance Φ of CSP(Γ), and the conjuncts of Φ are called constraints.

Note that we only introduce constraint satisfaction problems CSP(Γ) for finite constraint languages, i.e., relational structures Γ with a finite relational signature.

3 Set Constraint Languages

In this section, we give formal definitions of set constraint languages. Let S be the structure with domain P(N), the set of all subsets of natural numbers, and with signature {⊓, ⊔, c, 0, 1}, where

• ⊓ is a binary function symbol that denotes intersection, i.e., ⊓S = ∩;
• ⊔ is a binary function symbol for union, i.e., ⊔S = ∪;
• c is a unary function symbol for complementation, i.e., cS is the function that maps S ⊆ N to N \ S;
• 0 and 1 are constants (treated as 0-ary function symbols) denoting the empty set ∅ and the full set N, respectively.

Sometimes, we simply write ⊓ for the function ⊓S and ⊔ for the relation ⊔S , i.e., we do not distinguish between function symbol and respective relation. We use the symbols ⊓, ⊔ and not the symbols ∩, ∪ to prevent confusion with metamathematical usages of ∩ and ∪ in the text.

A set constraint language is a relational structure with a set of relations with a quantifier-free first-order definition in S; we always allow equality in first-order formulas. For example, the relation {(x, y, z) ∈ P(N)3 | x ∩ y ⊆ z} has the quantifier-free first-order definition z ⊓ (x ⊓ y) = x ⊓ y over S.

Theorem 1 (Follows from Theorem 5.8 in [Marriott and Odersky, 1996]). Let Γ be a set constraint language with a finite signature. Then CSP(Γ) is in NP.

It is well-known that the structure (P(N); ⊔, ⊓, c, 0, 1) is a Boolean algebra, with

• 0 playing the role of false, and 1 playing the role of true;
• c playing the role of ¬;
• ⊓ and ⊔ playing the role of ∧ and ∨, respectively.

To not confuse logical connectives with the connectives of Boolean algebras, we always use the symbols ⊓, ⊔, and c instead of the usual function symbols ∧, ∨, and ¬ in Boolean algebras. To facilitate the notation, we also write ¯ x instead of c(x), and x ̸= y instead of ¬(x = y).

We assume that all terms t over the functional signature {⊓, ⊔, c, 0, 1} are written as t = bigsqcapni=1 ⊔ni j=1 lij where lij is either of the form ¯x or of the form x for a variable x (every term over {⊓, ⊔, c, 0, 1} can be re-written into an equivalent term of this form, using the usual laws of Boolean algebras [Boole, 1847]). We allow the special case n = 0 (in which case t becomes 1), and the special case ni = 0 (in which case ⊔ni j=1 lij becomes 0). We refer to ci := {lij | 1 ≤ j ≤ ni} as an (inner) clause of t, and to lij as an (inner) literal of ci. We say that a set of inner clauses is satisfiable if there exists an assignment from V → P(N) such that for all inner clauses, the union of the evaluation of all literals equals N (this is the case if and only if the formula t = 1 has a satisfying assignment).

We assume that all quantifier-free first-order formulas φ over the signature {⊓, ⊔, c, 0, 1} are written as φ = ∧mi=1 ∨mi j=1 Lij where Lij is either of the form t = 1 (a positive (outer) literal) or of the form t ̸= 1 (a negative (outer) literal). Again, it is well-known and easy to see that we can for every quantifier-free formula find an equivalent formula in this form. We refer to Ci := {Lij | 1 ≤ j ≤ mi} as an (outer) clause of φ, and to Lij as an (outer) literal of φ. Whenever convenient, we identify φ with its set of clauses. In the following, when we write formula we always mean a formula over the signature {⊔, ⊓, c, 0, 1}.

4 EI Set Constraints

To define EI set constraints, we need to introduce a series of important functions defined on subsets of natural numbers.

Definition 2. Let

• i : (P(N))2 →P(N) be the function that maps (S1, S2) to the set {2x | x ∈ S1} ∪ {2x + 1 | x ∈ S2};
• F be the mapping that maps S ⊆ N to the set of finite non-empty subsets of S;
• f : N → F(N) be a bijection between N and the set of finite non-empty subsets of N (since both sets are countable, such a bijection exists );
• e : P(N) →P(N) be f -1 ◦F (first apply F, then apply the inverse of f);
• ei be the operation defined by ei(x, y) ↦→ e(i(x, y)).

Definition 3. Let f : (P(N))k → P(N) be a function, and R ⊆ P(N)l be a relation. Then we say that f preserves R if the following holds: for all t1 , . . . , tk ∈ (P(N))l we have that (f(t11 , . . . , tk1 ), . . . , f(t1l , . . . , tkl )) ∈ R if ti ∈ R for all i ≤ k. We say that f strongly preserves R is f preserves both R and (P(N))l \ R. If φ is a first-order formula that defines a relation R over S, and f preserves (strongly preserves) R, then we also say that f preserves (strongly preserves) φ.

Note that if a relation R is (strongly) preserved by e and by i, then it is also (strongly) preserved by their composition ei. Definition 4. The set of all relations with a quantifier-free first-order definition over S that are preserved by the operation ei is denoted by EI.

Proposition 9 shows that EI has a large subclass, called Horn-Horn, which has an intuitive syntactic description. In Section 5 we also present many examples of relations that are from EI and of relations that are not from EI. Before, we have to verify some properties of the functions i and e.

Proposition 5. The mapping i is an isomorphism between S2 and S.

We write x ⊑ y as a shortcut for x ⊓ y = x.

Proposition 6. The function e has the following properties.

• e is injective,
• e strongly preserves {1}, {0}, and ⊓, and
• e forgets unions, i.e., for all x, y, z ∈ P(N) such that x ⊔ y = z, not x ⊑ y, and not y x, we have that e(x) ⊔ e(y) e(z). ⊑

Note that in particular e preserves ⊑, and that e(c(x)) ⊑ c(e(x)).

5 Horn-Horn Set Constraints

A large and important subclass of EI set constraints is the class of Horn-Horn set constraints.

Definition 7. A quantifier-free first-order formula is called Horn-Horn if

• every outer clause is Horn, i.e., contains at most one positive outer literal;
• every inner clause is Horn, i.e., contains at most one positive inner literal.

Relations defined by a conjunction of outer Horn clauses are also called Horn. Relations defined by a Horn-Horn formula over S are also called Horn-Horn.

Proposition 8. Every Horn relation is preserved by i.

Proposition 9. Every Horn-Horn relation is preserved by e and i; in particular, it is from EI.

Proof. Suppose that R has a Horn-Horn definition φ over S with variables V . Since R is in particular Horn, it is preserved by i by Proposition 8.

Now we verify that R is preserved by e. Recall that the operation e preserves ⊓ and is injective (Proposition 6). Note that the formula x ⊔ y1 ⊔ · · · ⊔ yl = 1 can be equivalently written as x ⊓ y1 ⊓ · · · ⊓ yl = y1 ⊓ · · · ⊓ yl. By an easy induction, one shows that e also preserves this clause, and by injectivity it even strongly preserves this clause. It follows that e preserves formulas of the form t = 1 when all inner clauses of t are Horn, and similarly that e also preserves formulas of the form t ̸= 1 when all inner clauses of t are Horn. Now, every tuple t ∈ R must satisfy at least one literal in each outer clause of φ, and hence e(t) satisfies the same outer clause, which is what we had to show.

Examples.

1. The disjointness relation || is Horn-Horn: it has the definition ¯x ⊔ ¯ y = 1.
2. The relation {(x, y, u, v) | x ̸= y ∨u = v} can easily be seen to be Horn-Horn as well.
3. The ternary relation {(x, y, z) | x ∩ y ⊆ z}, which we have encountered above, has the Horn-Horn definition ¯x ⊔ ¯ y ⊔ z = 1.
4. Examples of relations that are clearly not Horn-Horn: {(x, y) | x ⊔ y = 1} is violated by e, and {(x, y, z) | (x = y) ∨ (y = z)} is violated by i.
5. The formula

is not Horn-Horn; more interestingly, it can be shown that it is from EI, but there is no equivalent Horn-Horn formula, since the relation is not preserved by i.

Combining the last example with Proposition 9, we get the following result.

Corollary 10. The set of relations admitting a Horn-Horn definition is strictly contained in EI.

We prepare now some results that can be viewed as a partial converse of Proposition 9.

Definition 11. A quantifier-free first-order formula φ is called reduced if it is in conjunctive normal form (CNF) and if every formula obtained from φ by removing an outer literal or an inner literal is not equivalent to φ over S.

Lemma 12. Every quantifier-free formula is over S equivalent to a reduced formula.

We first prove the converse of Proposition 8.

Proposition 13. Let φ be a reduced formula that is preserved by i. Then each outer clause of φ is Horn.

Definition 14. Let φ be a formula with variable set V , and let s : V → P(N) be a mapping. Then an assignment of the form x ↦→ e(s(x)) is called a core assignment (for V ). A reduced formula φ with variable set V is called strongly reduced if

• all negative outer literals are of the form x ̸= 1 or x ̸= 1, where x is a variable,
• every outer clause is Horn, and
• whenever φ′ is obtained fromφ by removing an inner literal or an outer literal fromφ, there is a core assignment that satisfies φ but not φ′ .

Lemma 15. For every quantifier-free formula φ there exists a strongly reduced formula φ′ with the same set of variables V such that φ and φ′ have the same core assignments.

For every quantifier-free formula φ, we call a strongly reduced formula φ′ as constructed in Lemma 15 from φ a core formula for φ.

Proposition 16. Let φ be a formula preserved by ei, and let φ′ be a core formula for φ. Then φ′ is Horn-Horn.

Proposition 17. Let Γ be a finite set constraint language from EI. Then CSP(Γ) can be reduced in linear time to the problem to find a satisfying assignment for a given set of HornHorn clauses.

Proof. Let Φ be an instance of CSP(Γ), and let V be the set of variables that appear in Φ. For each constraint R(x1, . . . , xk) from Φ, let φR be a reduced formula that defines R over S (which exists by Lemma 12), and let ψR be the core formula for φR (which exists by Lemma 15). By Proposition 16, the formula ψR is Horn-Horn.

We claim that Φ is a satisfiable instance of CSP(Γ) if and only if the set Ψ of all Horn-Horn clauses of formulas ψR obtained in the described manner is satisfiable.

If Φ has a solution s : V → P(N), then the core assignment x ↦→ ei(s(x), s(x)) is also a solution because Γ is preserved by ei; but then for each R the core-formula ψR is satisfied by this assignment. We have thus found an assignment that satisfies Ψ. Conversely, if Ψ has an assignment, then it also has a core assignment, since Ψ is Horn-Horn and therefore preserved by e. Then the same assignment will also satisfy all the formulas φR, and therefore is a solution to Φ.

6 Algorithm for Horn-Horn Constraints

This section concludes the proof that CSP(Γ) is tractable when all relations in Γ are from EI. By Proposition 17, it suffices to give an efficient algorithm that takes as input a set Φ of Horn-Horn clauses and decides satisfiability of Φ over S = (P(N); ⊔, ⊓, c, 0, 1). We first discuss an important subroutine of our algorithm, which we call the inner resolution algorithm.

Inner-Res(Φ) // Input: A finite set Φ of inner Horn clauses // Accepts iff Φ is satisfiable During the entire algorithm: if Φ contains an empty clause, then reject. Repeat If Φ contains a positive unit clause {x} then Remove all clauses where the literal x occurs. Remove the literal ¯x from all clauses. End if Until no clause changes. Accept

Lemma 18. Let Ψ be a set of inner Horn clauses. Then Inner-Res(Ψ ∪ {x1 = 1, . . . , xk = 1, y0 = 1, . . . , yl = 1}) rejects if and only if Ψ implies that x1⊔· · ·⊔xk⊔y1⊔· · ·⊔yl = 1.

Outer-Res(Φ) // Input: A finite set Φ of Horn-Horn clauses // Accepts iff Φ is satisfiable over (P(N); ⊓, ⊔, c, 0, 1) During the entire algorithm: if Φ contains an empty outer clause, then reject. Repeat Let Ψ be the set of all inner Horn clauses of terms t from positive unit clauses {t = 1} in Φ. If Inner-Res rejects Ψ, then reject. For each negative literal t ̸= 1 in clauses from Φ For each inner clause D = {x1, . . . , xk, y1, . . . , yl} of t Call Inner-Res on Ψ ∪ {x1 = 1, . . . , xk = 1, y0 = 1, . . . , yl = 1} If Inner-Res rejects then remove clause D from t End for If all clauses in t have been removed, then Remove outer literal t ̸= 1 from its clause End for Until no outer literal is removed Accept

Theorem19. The algorithm 'Outer-Res' in Figure 2 decides satisfiability for sets of Horn-Horn clauses in quadratic time.

Proof. We first argue that if the algorithm rejects Φ, then Φ has indeed no solution. The algorithm only rejects when it detects an empty clause. Observe that only negative literals get removed from clauses, and that a negative literal t ̸= 1

only gets removed from a clause when Inner-Res rejects Ψ ∪ {x1 = 1, . . . , xk = 1, y0 = 1, . . . , yl = 1} for each inner clause {x1, . . . , xk, y1, . . . , yl} of t. By Lemma 18, if InnerRes rejects Ψ ∪ {x1 = 1, . . . , xk = 1, y0 = 1, . . . , yl = 1} then Ψ implies that x1 ⊔ · · · ⊔ xk ⊔ y1 ⊔ · · · ⊔ yl = 1. Hence, the positive unit clauses imply that t = 1 and therefore the literal t ̸= 1 can be removed from the clause without affecting satisfiability.

Thus, it suffices to construct a solution when the algorithm accepts. Let Ψ be the set of all inner clauses of terms from positive unit clauses at the final stage, when the algorithm accepts. For each remaining negative outer literal {t ̸= 1} and each remaining inner clause D = {x1, . . . , xk, y1, . . . , yl} of t there exists an assignment αD from V → P(N) that satisfies Ψ ∪ {x1 ⊔ · · · ⊔ xk ⊔ y1 ⊔ · · · ⊔ yl ̸= 1}: otherwise, by Lemma 18, the inner resolution algorithm would have rejected Ψ ∪ {x1 = 1, . . . , xk = 1, y0 = 1, . . . , yl = 1}, and would have removed {t ̸= 1} from Φ. Let D1, . . . , Ds be an enumeration of all remaining inner clauses D that appear in all remaining negative outer literals.

We claim that the core assignment s : V → P(N) given by

x ↦→ e(i(αD1 (x), i(αD2 (x), . . . i(αDs-1 (x), αDs (x)) . . . )))

satisfies all clauses in Φ (where i is as in Proposition 5 and e is as in Proposition 6). Let C be a clause from Φ. By assumption, at the final stage of the algorithm, the clause C is still non-empty. Also note that since all formulas in the input were Horn-Horn, they contain at most one positive literal (Proposition 13). This holds in particular for C, and we therefore only have to distinguish the following cases:

• At the final state of the algorithm, C still contains a negative literal t ̸= 1. Since t ̸= 1 has not been removed, there must be a remaining inner clause D = {x1, . . . , xk, y1, . . . , yl} of t. Observe that s(x0) ⊔ · · · ⊔ s(xk) ⊔ s(y1) ⊔ · · · ⊔ s(yl) = 1 if and only if αDj (x0)⊔· · ·⊔αDj (xk)⊔αDj (y1)⊔· · ·⊔αDj (yl) = 1 for all 1 ≤ j ≤ s. Hence, and since αD(x0) ⊔ · · · ⊔ αD(xk) ⊔αD(y1) ⊔ · · · ⊔αD(yl) ̸= 1, s satisfies t ̸= 1. This shows that s satisfies C.
• All negative literals have been removed from C during the algorithm. The positive literal t0 = 1 of C is such that the inner clauses of t0 are Horn. They will be part of Ψ, and therefore t0 = 1 is satisfied by s.

We conclude that s is a solution to Φ.

Combining Proposition 17 with Theorem 19, we obtain:

Theorem 20. Let Γ be a finite set constraint language from EI. Then CSP(Γ) can be solved in quadratic time.

7 Maximality

The tractability result Theorem 20 may be complemented by a hardness result. Indeed, the class EI is a maximal tractable set constraint language in the sense of the following theorem.

Theorem 21. Let Γ be a set constraint language. Suppose that Γ contains all relations from EI, and also contains a relation that is not from EI. Then there is a finite sublanguage Γ′ of Γ such that CSP(Γ′ ) is NP-hard.

The proof of Theorem 21 uses the so-called universalalgebraic approach to the complexity of CSPs, as presented in [Bulatov et al., 2005] for finite domain constraint satisfaction. This requires that we re-formulate set CSPs as constraint satisfaction problems for ω-categorical structures (see e.g. [Bodirsky and K´ara, 2009]).

Because of the space limits, we cannot present the proof of Theorem 21 in this extended abstract. (We refer to the long version of this paper [Bodirsky et al., 2011] for the proof.)

8 Concluding Remarks

We have introduced the powerful set constraint language of EI set constraints, which in particular contains all Horn-Horn set constraints and all previously studied tractable set constraint languages. Constraint satisfaction problems over EI can be solved in polynomial - even quadratic - time. Our tractability result is complemented by a complexity result which shows that tractability of EI set constraints is bestpossible within a large class of set constraint languages.

Acknowledgement

Manuel Bodirsky has received funding from the ERC under the European Community's Seventh Framework Programme (FP7/2007-2013 Grant Agreement no. 257039).