Conditional Constraint Satisfaction: Logical Foundations and Complexity

1 Introduction

Constraint satisfaction is a static framework in its original formulation that cannot be used to model and solve decision problems in scenarios where uncertainty and dynamism come into play. Indeed, a Constraint Satisfaction Problem (CSP) instance (e.g., [Dechter, 2003]) is basically a triple (Var, U, C), where Var is a finite set of variables, U is a finite domain of values, and C = {C1,C2, . . . ,Cq} is a finite set of constraints, where each Ci is a pair (Si, ri), in which Si ⊆ Var is called the constraint scope, and ri ⊆ U |Si| is called the constraint relation. Then, by solving a CSP instance, we simply mean determining whether there is a substitution θ : Var ↦→U that satisfies all constraints.

To remove the assumption that all the variables, the domains of values, and the constraints are known beforehand and do not change over time, several generalized CSP frameworks have been already proposed in the literature (see, e.g., [Verfaillie and Jussien, 2005] and the references therein). In this paper, we focus on the core of these extensions, by considering the framework for Conditional Constraint Satisfaction Problems (CCSPs).

Indeed, CCSPs (proposed with the name of Dynamic CSPs in [Mittal and Falkenhainer, 2000]) are CSPs tailored to support conditional activation of variables and constraints, which have been used in model diagnosis, structural design, and configuration problems. As an example application, one may think of an automated personal computer (PC) configurator devoted to assemble several PC components. Conditional constraints may require other components to be added to the current configuration, depending on the choices made for the others. E.g., if the motherboard does not embed a video-card, then a compatible one should be added.

Despite the interest emerged for the CCSPs framework and the efforts spent in the design of specialized algorithms for their efficient solution (e.g., [Soininen et al., 1999; Bowen and Bahler, 1991; Sabin et al., 2003; Gelle and Faltings, 2003; Keppens and Shen, 2004]), many aspects have not yet been investigated and several research questions are, in fact, still open. For instance, both the expressiveness and the complexity issues arising in this setting have only partially been studied in the literature [Soininen et al., 1999; Bowen and Bahler, 1991; Mittal and Falkenhainer, 2000]. And, more importantly, differently from the case of classical CSPs where several classes of instances that are efficiently solvable have been singled out (e.g., [Pearson and Jeavons, 1997; Gottlob et al., 2000]), no island of tractability is known for CCSPs, whose identification is instead crucial for applications in real world scenarios.

The aim of this paper is precisely to shed lights on these aspects and to face the above research questions. To make our analysis formal, we shall exploit the logic-based characterization of a CSP instance (cf. [Kolaitis and Vardi, 1998]) as a pair (φ,D), where D is the constraint database, i.e., the set of all the constraint relations ri, for each constraint Ci = (Si, ri), and φ is a ∃FO∧,+ sentence, i.e., an existentially quantified first-order formula with no negations or disjunctions, over the relational vocabulary consisting of the atoms ri(Si). Within this framework, we investigate the class of those constraint satisfaction problems build over the ∃FO→,∧,+ fragment of the first-order logic, which consists of all the formulas obtained extending ∃FO∧,+ with the implication connective "→". The rationale of this approach is that enhancing ∃FO∧,+ with the implication connective is a mathematically well-founded approach to model conditional activation of variables, as for it is next exemplified.

Example 1. Consider again the PC configuration scenario. Then, the ∃FO→,∧,+ formula:

states, intuitively, that a motherboardM is needed to assemble a PC; moreover, if M has no embedded video, then a video-card V fitting the requirements of M has to be chosen (and, C is the additional cost). ◁

In fact, we show that ∃FO→,∧,+ formulas characterize (in a precise, logical sense) the class of CCSPs. Based on this result, we then embark on a systematic study of ∃FO→,∧,+. In summary:

• ✄ We investigate the expressive power of CCSPs by depicting, in Section 3, a clear picture of its relationships with other logic-based CSP formalisms. The results of this comparison are graphically summarized in Figure 1.
• ✄ In Section 4, we study the computational complexity of some basic reasoning tasks for CCSPs. We considered both the case where one is interested in finding a generic solution and the case where solutions are refined by means of some pro-orders. From our analysis, summarized in Figure 2, it emerges that reasoning with CCSPs is intractable, with hardness and membership results being established for various classes at the first and the second level of the polynomial hierarchy.
• ✄ Motivated by the above complexity results, in Section 5, we turn to identify tractable classes of ∃FO→,∧,+ formulas, by issuing restrictions on the constraints interactions. As a bad news, we show that decomposition methods for traditional CSPs do not guarantee the tractability of CCSPs. Indeed, the NP-hardness of the SATISFIABILITY problem also holds for the class of CCSPs whose constraints interactions can be modelled with an acyclic primal graph (see, e.g., [Dechter, 2003]).
• ✄ The major reason for the failure of traditional decomposition methods is that the primal graph obscures the real nature of the interactions occurring in CCSPs due to the variables activation. Hence, in Section 5.2, we introduce a special graphical representation for CCSPs, called implication graph, and show that SATISFIABILITY is feasible in LOGCFL and hence in polynomial time, over instances whose implications graphs are acyclic or have, more generally, bounded treewidth [Robertson and Seymour, 1986].

2 ∃FO→,∧,+ Formulas: Syntax and Semantics

In this section, we propose a framework for modelling conditional activation of variables and constraints in CSPs, which is based on an extension of the fragment ∃FO∧,+ with the logical implication, as formalized next.

An ∃FO→,∧,+ sentence (over a vocabulary R of constraint relations) is a formula ∃ ⃗X φ( ⃗X), where φ( ⃗X) belongs to the fragment FO→,∧,+ of first-order logic, defined as follows:

• "true" and "false" are in FO→,∧,+;
• Any atom of the form r( ⃗X) (r ∈ R) is in FO→,∧,+;
• If φ( ⃗X) and ψ(⃗Z) are in FO→,∧,+, then φ( ⃗X) ∧ ψ(⃗Z) is in FO→,∧,+;
• If φ( ⃗X) is in FO∧,+ and ψ( ⃗X, ⃗Y ) is in FO→,∧,+, then φ( ⃗X) → ∃⃗Y ψ( ⃗X, ⃗Y ) is in FO→,∧,+.

The set of all the variables in ψ is denoted by V(ψ).

Example 2. The following formula ψ0 ∈ ∃FO→,∧,+ adds some further requirements to the configuration constraints in Example 1 (names have been shortened, for simplicity):

Given a constraint database D and an ∃FO→,∧,+ formula ψ, we denote by (ψ,D) the constraint satisfaction problem instance of deciding an assignment for variables in ψ that satisfies all the constraints over D.

Note that because of the presence of the implication connective, differently from the standard CSPs, a formula ψ ∈ ∃FO→,∧,+ can be satisfied by partial assignments over V(ψ). Formally, a partial assignment θ for (ψ, D) is a mapping from a subset of V(ψ) to values in D. Then, the θ-reduct of ψ is the formula θ(ψ) resulting from ψ by (1) applying all the substitutions in θ to the variables in ψ, and (2) by replacing all the atoms in which a variable in V(ψ) \ V(θ) occurs with "false", where V(θ) denotes the variables in the domain of θ. A solution for (ψ, D) is a partial assignment θ such that θ(ψ) evaluates to true over D, denoted by D |= θ(ψ).

Example 3. Consider the database D0 containing the relations: m = {(m1), (m2)}, h = {(m2)}, f = {(m2, v2)}, c = {(v2, c4), (v1, c3)}, e = {(m1)}, b = {(m1)} and g = {(m1, h4)}. Then, the followings assignments are partial: θ1 = {M/m2, V/v2, C/c3}

Note that θ1 is not a solution for (ψ0,D0). On the other hand, the θ2-reduct of ψ0 evaluates true over D0. ◁

3 Expressiveness of ∃FO→,∧,+ Formulas

The first crucial questions for CCSPs are how they relate with other approaches to deal with conditional activation of variables and constraints, and whether they are more expressive (in a precise logical sense) than classical CSPs. Both the questions are answered in this section.

Let F be a CSP formalism, i.e., a formalism for modelling constraint satisfaction problems (e.g., a subset of FO), and let D be a constraint database. For a formula φ ∈ F , let S(φ, D) denote the set of all the solutions, and for a set of variables V, let S(φ,D)[V] denote the set obtained from S(φ,D) by restricting each solution over the variables in V.

Let F1 and F2 be two CSP formalisms. We say that F1 weakly simulates F2 if for each φ2 ∈ F2 there exists φ1 ∈ F1 such that for each constraint database D, S(φ2, D) = S(φ1, D)[V(φ2)]. We say that F1 is more expressive than F2 iff F1 simulates F2 but F2 does not simulate F1. If F1 simulates F2 and viceversa, F1 and F2 are equivalent. If F1 does not simulate F2, and F2 does not simulate F1, we say that F1 and F2 are incomparable.

Armed with the notions above, we compared the expressiveness of ∃FO→,∧,+ with conditional CSPs (CCSP)s, with ∃FO∧,+ and with the positive existential disjunctive fragment ∃FO∨,∧,+ of FO. Results are summarized in Figure 1.

3.1 Comparison with Conditional CSPs

A CCSP specification π is a tuple 〈Var,VarI, CC, CA〉, where Var is a set of variables, VarI ⊆ Var is a set of initial variables (intuitively, of the variables that are initially "active"), and where the set of constraints is partitioned into compatibility (CC) and activity (CA) constraints.

Compatibility constraints are constraint atoms (as in traditional CSPs), while activity constraints are of the following kinds: require variable (RV): c(V1, . . . , Vk) RV→ V ; always require variable (ARV): {V1, . . . , Vk}ARV → V ; require not (RN): c(V1, . . . , Vk) RN→ V ; always require not (ARN): {V1, . . . , Vk}ARN → V , with {V1, . . . , Vk, V } ⊆ Var .

A CCSP instance is a pair (π,D), where π is a specification and D is a constraint database. A legal assignment for (π, D) is a partial mapping θ from variables in Var to domain values in D. A solution is a legal assignment such that: (1) VarI ⊆ V(θ); (2) θ satisfies every active compatibility constraints, i.e., those compatibility constraints whose variables are in V(θ); and (3) θ satisfies every activity constraint:

• WARV →V is satisfied if W ⊆ V(θ) implies V ∈ V(θ);
• c(V1, . . . , Vk) RV→V is satisfied if {V1, . . . , Vk} ⊆ V(θ) and (θ(V1), . . . θ(Vk)) ∈ c (in D) implies V ∈ V(θ);
• WARN →V is satisfied if W ⊆ V(θ) implies V ̸∈ V(θ);
• c(V1, . . . , Vk) RN→V is satisfied if {V1, . . . , Vk} ⊆ V(θ) and (θ(V1), . . . θ(Vk)) ∈ c (in D) implies V ̸∈ V(θ);

As usual, the set of all the solutions is denoted by S(π,D). We next show that ∃FO→,∧,+ formulas are, in fact, an elegant, mathematically-founded characterization of CCSPs.

Proof (Sketch). Let π be 〈Var,VarI, CC, CA〉. We build an ∃FO→,∧,+ formula ψπ = ∃Var, VarI Vc∈CC∪CA φc, where φc is obtained as follows:

• if c is the compatibility constraint c(V1, . . . , Vk), then φc = ∧V ∈{V1,...,Vk}\VarI dom(V ) → c(V1, . . . , Vk);
• if c is the activity constraint c(V1, . . . , Vk) RV→V , φc is given by c(V1, . . . , Vk) → dom(V ).

Note that other activity constraints can be, in fact, simulated by RV and compatibility constraints (cf. [Mittal and Falkenhainer, 2000]). Moreover, w.l.o.g., we have assumed the existence of a monadic relation dom listing all possible values for the variables - without this relation, the simulation is also possible, but would have required a much intricate construction for ψπ.

It is possible to show (details omitted for lack of space) that, for every constraint c of π, a legal assignment θ satisfies c iff the corresponding partial assignment θ of ψπ satisfies the subformula φc. Hence, ∀D, it is: S(π,D) = S(ψπ,D).

Not surprisingly, CCSPs have been previously simulated by means of different logic-based frameworks. For instance, [Bowen and Bahler, 1991] expressed CCSPs by means of the FOF logic; and, [Bacchus and Walsh, 2005] discussed a rich formalism where implications can be simulated by negations and disjunctions, by introducing a specific propagation method and characterizing when this method enforces generalized arc-consistency. Yet, the precise logical characterization of CCSPs was unknown, which is made clear below.

Proof (Sketch). Let ψ be an ∃FO→,∧,+ formula. We build a CCSP πψ as follows. First, all the atoms are converted into compatibility constraints. Then, for each subformula φ′ ( ⃗X) → ∃⃗Y φ′′ ( ⃗X, ⃗Y ) where φ′ = c1( ⃗X)∧· · ·∧ck( ⃗X), and where ⃗Y = {Y1, . . . Ym}, we create m×k fresh variables Y j i (1 ≤ i ≤ m, 1 ≤ j ≤ k), m × k activation constraints of the form cj ( ⃗X) RV→Y j 1 , . . . cj( ⃗X) RV→Y jm (1 ≤ j ≤ k), and m ARV constraints of the form {Y 1 i , . . . , Y k i }ARV →Yi. It can be shown that for each database D, S(ψ, D) = S(πψ, D)[V(ψ)].

Interestingly, if ψ is such that the left-hand side of any implicative formula is a constraint atom only, the encoding can be adjusted not to use fresh variables. Hence, we can show a stronger kind of simulation: ∀D, S(ψ, D) = S(πψ, D).

Before leaving the section, note that in [Mittal and Falkenhainer, 2000] solutions to CCSPs are also required to be subset-minimal. In fact, the simulation techniques of Theorem 1 and 2 (in the case left sides of implications are constraint atoms) established a one-to-one correspondence between solutions of CCSPs and assignments for ∃FO→,∧,+ formulas. Hence, further properties on the solutions are preserved as well, but formal results are omitted.

3.2 Comparison with Other Logics for CSPs

A comparison between CSPs and CCSPs has been proposed in [Soininen et al., 1999], by focusing on a knowledge representation perspective. Indeed, it is shown that CCSPs are not modular representable by standard CSPs, i.e., intuitively, that small changes in a CCSP may result in significant changes in any corresponding CSP, which is an encoding for it.

Based on the logical equivalence between CCSPs and ∃FO→,∧,+, we can now formally compare CCSPs with CSPs, and in fact prove that there are CCSPs (formulas in ∃FO→,∧,+) that cannot be "simulated" in ∃FO∧,+. The argument is that there is no way to encode the "→" connective by means of conjunctions. In turn, "→" cannot encode disjunction of atoms. Thus, the following relationships hold 1 .

Theorem3. ∃FO→,∧,+ is such that: (1) it is more expressive than ∃FO∧,+; and, (2) it is incomparable with ∃FO∨,∧,+.

1 Proofs are reported in an extended version of the paper available at www.unical.it/∼ggreco.

4 The Complexity of Reasoning with CCSPs

Let (ψ,D) be a CCSP instance. The intrinsic complexity of some basic reasoning tasks for (ψ,D) has been studied in [Soininen et al., 1999; Mittal and Falkenhainer, 2000]. In particular, it is known that the SATISFIABILITY problem (does there exists a partial assignment θ such that θ is a solution for (ψ,D)?) is NP-complete.

However, there are other important reasoning tasks that often come into play with CSPs, and whose complexity has not been investigated for CCSPs. In this section, we explore these issues, by focusing on the following problems:

• CHECKING: Given a partial assignment θ, is θ a solution for (ψ,D)?
• RELEVANCE: Given a variable X, is X contained in V(θ) for some solution θ for (ψ,D)?
• NECESSITY: Given a variable X, is X contained in V(θ) for every solution θ for (ψ,D)?

When moving to CCSPs, these problems can be specialized to take care of those solutions that are partial assignments. Indeed, knowing whether there are solutions in which some variable is not "active" may be quite relevant. For instance, in product configuration, one may be interested in finding the configuration with the minimum number of (additional) components that, yet, meets the users' requirements.

In order to model scenarios as above, it is convenient to refine the notion of solutions by means of some pre-order ⪯ on the set of all the possible partial assignments. Accordingly, a solution θ for (ψ, D) is said ⪯-minimal if for each solution θ′ , it holds: θ ⪯ θ′ . In particular, we next consider ⪯-minimal solutions, where ⪯ is one of the following pre-orders 2 :

subset minimality "⊆": θ1 ⊆v θ2 iff V(θ1) ⊆ V(θ2). minimum cardinality "≤": θ1 ≤ θ2 iff |V(θ1)| ≤ |V(θ2)|. weighted cardinality "⊑": A weight w is attached to each

variable, and

Next, we depict a complete picture of the complexity figures arising in the CCSP setting.

Theorem 4. The complexity of CHECKING, RELEVANCE, and NECESSITY and of their variants for ⪯-minimal solutions (⪯∈ {"⊆", "≤", "⊑"}) is as shown in Figure 2.

Proof (Sketch). When no pre-order is considered, results easily derive from standard results on CSPs. Due to space limitations, we next only report the proof sketches for the variants of CHECKING.

CHECKING⊆ is co-NP-complete: (Membership) Let (ψ,D) be a CCSP instance, and let θ be a partial assignment such that θ |= ψ. Consider the complementary problem of deciding whether there is an assignment θ′ such that (i) θ′ is a solution for (ψ,D) and (ii) V(θ′ ) ⊆ V(θ) does not hold. Clearly, θ′ can be guessed in NP, while (i) and (ii) can be checked in P.

(Hardness) Deciding whether a Boolean formula in conjunctive normal form Φ = c1 ∧ . . . ∧ cm over the variables X1, . . . ,Xn is not satisfiable, i.e., deciding whether there exist no truth assignments to the variables making each clause cj true, is a well-known co-NP-complete problem.

2 In fact, these pre-orders have been widely used for refining solution concepts in other AI frameworks.

We build a CCSP instance (ψ(Φ),D(Φ)) as follows. For each clause cj, which is w.l.o.g. of the form tj1 ∨ tj2 ∨ tj3 , where tj1 is a variable Xi or its negation ¬Xi, D(Φ) contains the relation rcj = {(T1, T2, T3) | Ti ∈ {"true", "false"} s.t. cj is not satisfied when tji = Ti, ∀i}. Then, for each variable Xi in Φ, D(Φ) contains the relation rvi = {("true"), ("false")}. Finally, unsat = {(1)} is in D(Φ), and no other relation is in D(Φ). The formula ψ(Φ) is of the form ∃X ′1 , ..., X ′n, Z ∧1≤i≤n rvi(X ′ i ) ∧ ∧1≤j≤m(rcj(X ′j1 ,X ′j2 ,X ′j3 ) → unsat(Z)), where X ′ji ∈ {X ′1, ...,X ′n} is a variable such that Xji occurs in cj.

Let x be a truth value assignment for the variables in Φ. Let θx denote the assignment for (ψ(Φ),D(Φ)) such that: X ′ i is mapped to "true" (resp., "false") in θ(x) iff Xi is true (resp., false) x, and such that Z/1 is in θx iff x is not satisfying. Then, any solution θ′ for (ψ(Φ),D(Φ)) is such that V(θ′ ) ⊇ {X ′1, ...,X ′n}; moreover, Z may not occur in V(θ′ ) if and only if there is a satisfying assignment x for Φ such that θ′ = θx . To conclude the proof, we can hence take an assignment xu that does not satisfy Φ and notice that θxu is ⊆-minimal ⇔ there is no satisfying assignment for Φ.

CHECKING≤ and CHECKING⊑ are co-NP-complete: Memberships can be shown with similar arguments as above. The hardness of CHECKING≤ can be shown by observing that, in the above reduction, θxu is in fact ≤-minimal ⇔ θxu ⊆- minimal ⇔ there is no satisfying assignment for Φ. Finally, the hardness of CHECKING⊆ follows by assigning unitary weights to all the variables of ψ(Φ).

5 Restricted Classes of CCSPs

In the light of the intractability results of the previous section, it is relevant to single out classes of CCSPs that can be efficiently solved. To this aim, we next investigate how to adapt the approaches used in traditional CSPs, where tractable classes are identified by structural decomposition methods (e.g., [Pearson and Jeavons, 1997; Gottlob et al., 2000]).

5.1 The Hardness of Acyclic Structures

Let ψ be a FO formula. The structure of constraints interactions in ψ can be represented by the primal graph G(ψ) = (V(ψ),E), where two variables occur in some edge of E if they appear together in a constraint atom in ψ. We next focus on classes of primal graphs having bounded treewidth.

A tree decomposition of a graph G = (V,E) is a pair 〈T, χ〉, where T = (N, F) is a tree, and χ is a function assigning to each vertex p ∈ N a set of vertices χ(p) ⊆ V , such that the following conditions are satisfied: (1) ∀b ∈ V , ∃p ∈ N such that b ∈ χ(p); (2) ∀{b, d} ∈ E, ∃p ∈ N such that {b, d} ⊆ χ(p); (3) ∀b ∈ N, the set {p ∈ N | b ∈ χ(p)} induces a connected subtree of T . The width of 〈T, χ〉 is maxp∈N |χ(p)-1|, and the treewidth of G (short: tw(G)) is the minimum width over all its tree decompositions.

Let L be a subset of FO. We denote by CSPbtw(L) the class of all the CSP instances (φ,D), where φ is in L and where tw(G(φ)) is bounded by a fixed constant. It is wellknown (see, e.g., [Gottlob et al., 2000]) that SATISFIABILITY can be solved in polynomial time on CSPbtw(∃FO∧,+). We next show that this is not the case for CSPbtw(∃FO→,∧,+), even when further restricted on the class CSPac(∃FO→,∧,+) of acyclic instances (i.e., those having treewidth 1).

Theorem 5. SATISFIABILITY is NP-hard, even when restricted on the class CSPac(∃FO→,∧,+).

Proof. Let I = {I1, ..., In} be a set of elements, and let S = {S1, ..., Sm} be a number of sets each one containing exactly three elements in I. Recall that the EXACT-COVER-BY-3SETS problem of deciding whether there exists a set C ⊆ {S1, ..., Sm} such that ⋃Si∈C Si = {I1, ..., In} and Si∩Sj = ∅, for each Si, Sj ∈ C with i ̸= j, is NP-complete.

As an example instance, Figure 3 shows (on the left) the sets S1 = {I1, I2, I3}, S2 = {I4, I5, I6}, and S3 = {I3, I4, I5}. A solution consists of the set {S1, S3}.

We build a CCSP instance (ψ(I, S),D(I, S)) as follows. For each item Ii, D(I, S) contains the relation rIi = {(sj) | Sj ∈ S and Ii ∈ Sj}. For each set Sj and item Ii ∈ Sj, D(I, S) contains the relation rSji = {(sj)}. And, no other relation is in D(I, S). Moreover, the formula ψ(I, S) is of the form: ∃X1, ...,Xn, ∧i rIi(Xi) ∧ ∧i,i′ ,j|{Ii,Ii′}⊆Sj (rSji(Xi) → rSji′ (Xi′)). Importantly, given that constraint relations in ψ(I, S) are unary, G((ψ(I, S),D(I, S))) does not contain any edge and, hence, it is trivially acyclic.

We now claim that: there exists an exact cover of I with sets from S ⇔ (ψ(I, S), D(I, S)) admits a solution.

(⇒) Let C be an exact cover. Consider the assignment θC build as follows: (1) V(ψ(I, S)) = V(θC ); and (2) Xi is mapped to sj if and only if Ii ∈ Sj and Sj ∈ C. Note that the conjunction ∧i rIi(Xi) is satisfied by θC , by construction of the relation rIi in D(I, S). Hence, it remains to show that each implication of the form (rSji(Xi) → rSji′ (Xi′ )) is satisfied as well. We distinguish two cases. If Xi is not mapped to sj, then rSji(Xi) evaluates false over the database, and the implication is trivially satisfied. Otherwise, i.e., if Xi is mapped to sj , we must have that Xi′ with Ii′ ∈ Sj is mapped to sj as well, which in fact holds by construction of θC .

(⇐) Assume there is a solution θ for (φ(I, S),D(I, S)). We first notice that the following properties hold on θ: (P1) V(θ) = {X1, ...,Xn}; and (P2) if Xi is mapped to sj in θ, then Xi′ is mapped to sj, for each Ii′ ∈ Sj. Then, we can build the set C θ = {Sj | ∃Xi that is mapped to sj in θ}, and notice that it is an exact cover.

5.2 Tractable Classes

Since classical approaches fail in isolating classes of tractable CCSPs, we next propose and study a decomposition strategy specific for ∃FO→,∧,+ formulas. We shall focus on plain formulas, where nesting of the implication connective is not allowed. Formally, a plain ∃FO→,∧,+ formula is of the form:

where n ≥ 0, and φ, bi, hi are in FO∧,+.

In fact, arbitrary formulas can be made plain by iteratively substituting each subformula (φ → ((φ′ → φ′′ ) ∧ φ′′′ )) with (φ ∧ φ′ → φ′′ ) ∧ (φ → φ′′′ ); this transformation preserves the set of all the solutions, and is feasible in quadratic time.

Let ψ be a plain ∃FO→,∧,+. Constraint interactions in ψ can be represented with the implication graph IG(ψ) = (V, E), where V = V(ψ) ∪ {b1, ..., bn} ∪ {h1, ..., hn} and edges have the form: (X, Y ) between pairs of variables occurring in the same atom; (X, bi) if X occurs in some atom of bi; (X, hi) if X occurs in some atom of hi; and (bi, hi), for each subformula (bi( ⃗X) → ∃⃗ Yihi( ⃗X, ⃗ Yi)). E.g., a portion of the implication graph for the EXACT-COVER-BY-3-SETS instance in the proof of Theorem 5, which reveals the "hidden" intricacy of the problem, is reported in Figure 3 (bj,i,i′ and hj,i,i′ refer to the implication rSji(Xi) → rSji′ (Xi′ )).

Then, the class CSP[i]btw(∃FO→,∧,+) is defined as the set of all the CCSPs instances (ψ,D), where ψ is a plain formula in ∃FO→,∧,+ such that tw(IG(ψ)) is bounded by a fixed constant. An algorithm, called DecideSolutionk, deciding whether an instance in CSP[i]btw(∃FO∧,+) has a solution is reported in Figure 4.

The algorithm works on an tree decomposition of IG(φ) of width k, whose shape is T = (N, F). Roughly, it is based on a recursive procedure findSolution that receives in input a vertex v ∈ N. Each vertex is equipped with some nodes associated with variables of φ, denoted by V(v), as well as with nodes from {b1, ..., bn} and {h1, ..., hn}. The sets of these nodes are denoted by B(v) and H(v), respectively.

Basically, findSolution guesses for each child c of v (in F), a partial assignment θc for V(c) (conforming with the assignment for θv), and two "states" bc and hc. The state bc (resp., hc) is a mapping from B(c) (resp., Hc) to the values {T, F, willF, wasF}. The mapping bc(bi) = T states that the conjunct bi of φ must be true. In fact, when bc(bi) = T, it must be the case that the atoms in bi restricted over the assignment for v are satisfied in D (short: D |= πbi (v) in B1). Note that the information that bc(bi) = T is propagated to all

Input: (φ, D), and a k-width tree decomposition 〈T, V, H, B〉 of IG((φ, D)) with T = (N, F ); Output: true iff there is a solution θ for (ψ,D); Boolean Function findSolution(v : vertex in N; θv : partial assignment; bv : state for B(v); hv : state for H(v)); begin for each c s.t. (v, c) ∈ F guess: a partial assignment θc for V(c); a "state" bc for B(c), and a "state" hc for H(c); check that the following conditions hold: V 1 : D |= πφ(v); V 2 : for each c ∈ N s.t. (v, c) ∈ F θv conforms with θc; B1 : for each bi ∈ B(v) bv(bi) = T ⇒ D |= πbi (v); bv(bi) = F ⇔ D ̸|= πbi (v); B2 : for each bi ∈ B(p) s.t. bp(bi) = T ∀(v, c) ∈ F , bi ∈ B(c) ⇒ bp(bi) = T; B3 : for each bi ∈ B(p) s.t. bp(bi) = F ∨ wasF ∀(v, c) ∈ F , bi ∈ B(c) ⇒ bp(bi) = wasF; B4 : for each bi ∈ B(p) s.t. bp(bi) = willF ∀(v, c) ∈ F , bi ∈ B(c) ⇒ bc(bi) ̸= T; ∃(v, c) ∈ F s.t. bi ∈ B(c) ∧ (bc(bi) = willF ∨ F); H1 : for each hi ∈ H(v) hv(hi) = T ⇒D |= πhi (v); hv(hi) = F ⇔D ̸|= πhi (v); H2 : for each hi ∈ H(p) s.t. hp(hi) = T ∀(v, c) ∈ F , hi ∈ H(c) ⇒ hp(hi) = T; H3 : for each hi ∈ B(p) s.t. hp(bi) = F ∨ wasF; ∀(v, c) ∈ F , hi ∈ H(c) ⇒ hp(hi) = wasF; H4 : for each hi ∈ H(p) s.t. hp(hi) = willF ∀(v, c) ∈ F , hi ∈ H(c) ⇒ hc(hi) ̸= T; ∃(v, c) ∈ F s.t. hi ∈ H(c) ∧ (hc(bi) = willF ∨ F); I1 : for each (bi, hi) ∈ B(v) ×H(v) bv(bi) = T ⇒ hv(hi) = T; R1 : for each c ∈ N s.t. (v, c) ∈ F , findSolution(c, θc, bc, hc); if this check fails then return false; else return true; end; begin (* MAIN *) let v be the root of T; guess the sets θv, bv, and hv; check conditions (V 1), (B1), (H1), and (I1); if this check fails then return false; else return findSolution(r, θv , bb, hv); end.

the children (B2), so that all the atoms in bi are eventually satisfied. On the other hand, when bc(bi) = F the algorithm must find an atom which is not true in the database (B1). Moreover, all the children are advertised that bi is false, by putting them into the state wasF in (B3), which is basically a do not care state - this is also done when bp(bi) = wasF, to propagate this knowledge in the tree. Note that, it may happen that bi will be made false during the computation but not in the current node v. For these cases, we use the state willF, which forces (B4) that none of its children are in state T and that there is at least a children with state willF or F. Similar considerations apply to the mapping hv. Eventually, (I1) checks whether the implications are satisfied, while (V 1) checks whether the pure conjunctive part is satisfied.

The proof of correctness of DecideSolutionk is omitted. For the running time, we can adapt the techniques in [Gottlob et al., 2002] to show the following.

Theorem6. On CSP[i]btw(∃FO→,∧,+), SATISFIABILITY is in LOGCFL, hence, tractable and highly-parallelizable.

Acknowledgments

This work was supported by a Royal Society Wolfson Research Merit Award, allowing G. Gottlob to invite G. Greco and T. Mancini to Oxford.

In addition, G. Greco's work was supported by M.I.U.R. under project "tocai.it: Tecnologie Orientate alla Conoscenza per Aggregazioni di Imprese in Internet".