Dependence Logic vs. Constraint Satisfaction

Dependence Logic vs. Constraint Satisfaction Lauri Hella∗1and Phokion G. Kolaitis†2 1 School of Information Sciences, University of Tampere, Finland [email protected] 2 University of California Santa Cruz and IBM Research – Almaden, USA [email protected] Abstract During the past decade, dependence logic has emerged as a formalism suitable for expressing and analyzing notions of dependence and independence that arise in different scientific areas. The sentences of dependence logic have the same expressive power as those of existential second-order logic, hence dependence logic captures NP on the class of all finite structures. In this paper, we identify a natural fragment of universal dependence logic and show that, in a precise sense, it captures constraint satisfaction. This tight connection between dependence logic and constraint satisfaction contributes to the descriptive complexity of constraint satisfaction and elucidates the expressive power of universal dependence logic. 1998 ACM Subject Classification F.4.1 Mathematical Logic, F.1.3 Complexity Measures and Classes Keywords and phrases Dependence logic, constraint satisfaction, computational complexity, expressive power Digital Object Identifier 10.4230/LIPIcs.CSL.2016.14 1 Introduction Dependence logic is a formalism for expressing and analyzing notions of dependence and independence that are encountered across different areas of computer science and mathematics, from functional dependencies in relational databases to independence in linear algebra and in probability theory. Even though its origins can be traced back to Henkin quantifiers [ 10 ] and to independence-friendly logic [ 11 ], dependence logic was fully developed by Väänänen in his monograph [ 17 ], which became the catalyst for numerous subsequent investigations (see, e.g., [ 6 , 7 , 8 , 13 , 14 ]). The syntax of dependence logic uses dependence atoms as the main building blocks; these atoms assert that a functional dependency between variables holds, i.e., that a certain variable is a function of some other variables. The semantics of dependence logic uses sets of assignments, called teams, instead of single assignments of values to variables. In terms of expressive power and as regards sentences, dependence logic has the same expressive power as existential second-order logic [ 13 ]. Combined with Fagin’s Theorem [ 4 ], this result implies that, on classes of finite structures, the sentences of dependence logic can express precisely all decision problems in NP. Constraint satisfaction comprises a set of algorithmic problems that are ubiquitous in several different areas of computer science. An influential paper by Feder and Vardi [ 5 ] provided the impetus for an in-depth and still ongoing investigation of the connections ∗ The research of Lauri Hella was partially supported by a Professor Pool’s Grant of the Finnish Cultural Foundation. †The research of Phokion Kolaitis was partially supported by NSF Grant IIS-1217869. ©Lauri Hella and Phokion G. Kolaitis; licensed under Creative Commons License CC-BY 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Editors: Jean-Marc Talbot and Laurent Regnier; Article No. 14; pp. 14:1–14:17 Leibniz International Proceedings in Informatics Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany 14:2 Dependence Logic vs. Constraint Satisfaction between constraint satisfaction, computational complexity, logic, and universal algebra (see, e.g., [ 1 , 9 ]). Feder and Vardi argued convincingly that, in its most general form, constraint satisfaction can be identified with the Homomorphism Problem: given two relational structures A and B , is there a homomorphism from A to B ? Clearly, the Homomorphism Problem is NP-complete, since it contains, for example, 3-Satisfiability as a special case. Moreover, each fixed relational structure B gives rise to the non-uniform constraint satisfaction problem CSP ( B ): given a relational structure A , is there a homomorphism from A to B ? The computational complexity of each such problem depends on the structure B . Feder and Vardi conjectured that the family of all constraint satisfaction problems CSP ( B ) exhibits the following dichotomy: for each B , either CSP ( B )is NP-complete or CSP ( B )is solvable in polynomial time. This conjecture remains open to date, in spite of concerted efforts by different groups of researchers that, so far, have established only special cases of it. Feder and Vardi [ 5 ] also investigated the descriptive complexity of constraint satisfaction. To this effect, they identified a fragment of existential second-order logic, called monadic monotone strict NP without inequality or, in short, MMSNP , and showed that it captures, in a precise sense, the family CSP ( B )of all non-uniform constraint satisfaction problems. MMSNP consists of all sentences of existential second order logic that have the following properties (where it is assumed that all negation symbols occurring in the sentences have been pushed inward, so that they apply to atomic formulas only): (a) all second-order quantifiers are monadic; (b) all first-order quantifiers are universal; (c) no inequalities occur in the formula; (d) all occurrences of relation symbols from the underlying vocabulary are preceded by the negation symbol. MMSNP captures constraint satisfaction in the following way. First, it is easy to see that if B is a relational structure, then CSP ( B )is expressible in MMSNP . Second, Feder and Vardi showed that every MMSNP -expressible problem is equivalent to a CSP ( B ), for some relational structure B , under polynomial-time reductions (originally, this equivalence was proved under randomized polynomial-time reductions, which, however, were subsequently derandomized [ 15 ]). Note that Feder and Vardi also showed that if one of the aforementioned properties (a), (b), (c), (d) defining MMSNP is dropped, then every problem in NP is equivalent under polynomial-time reductions to a problem in the resulting fragment of existential second-order logic. Combined with Ladner’s Theorem [ 16 ], this implies that if one of these four properties is dropped, then the resulting fragment can express decision problems that are neither NP-complete, nor solvable in polynomial time (unless P=NP). As seen from the preceding discussion, dependence logic captures existential second-order logic, while constraint satisfaction is captured by a proper fragment of existential second-order logic. This state of affairs gives rise to the following question: is there a natural fragment of dependence logic that captures constraint satisfaction? In this paper, we show that this is indeed the case. In fact, we identify a fragment of a variant of dependence logic consisting of universal sentences and show that it can capture, in a precise sense, constraint satisfaction. In what follows in this section, we present a high-level description of our main results. The building blocks of dependence logic, as developed by Väänänen, are dependence atoms dep ( x x x ; y ), where x x x is a tuple of variables and y is a single variable. A team (i.e., a set of assignments) satisfies such an atom if whenever two assignments in the team agree on the variables in x x x , they must also agree on the variable y . Here, we introduce a variant of dependence atoms, which we call uniform dependence atoms; they are expressions of the form udep ( x1, . . . , xn ; α1, . . . , αn )with the following semantics: a team T satisfies udep ( x1, . . . , xn ; α1, . . . , αn )if there is a unary function f such that for every assignment s in T , we have that s ( αi ) = f ( s ( xi )), for 1 ≤i≤n . Even though uniform dependence atoms have not been studied in their own right in earlier work on dependence logic, we believe that L. Hella and Ph. G. Kolaitis 14:3 they are very natural as they express scenarios in which n different observers use sensors or measuring instruments to collect data in different sites, and then each observer applies the same function to the data collected to obtain a value. As a concrete example, each xi may represent a list of temperature values collected at site i at regular intervals of time each day, while αimay stand for the maximum temperature at site i. We consider k -valued uniform dependence atoms in which the variables α1, . . . , αn take values in a domain with k elements, for some fixed k≥ 1. We define the universal monotone uniform dependence logic ∀-MUD [ k ]as the closure under universal quantification of all quantifier-free formulas that contain all k -valued uniform dependence atoms, all equalities between k -valued variables and constants, and all negated relational atoms, and are closed under disjunctions and conjunctions. The semantics of the logic ∀-MUD [ k ]are given using teams as in (standard) dependence logic. Our first main result asserts that every non-uniform constraint satisfaction problem CSP ( B )such that B has a single relation is expressible by a sentence of ∀-MUD [ k ], where k is the number of elements in the universe of B . Our second main result asserts that every sentence of ∀-MUD [ k ], k≥ 1, is equivalent to a sentence of MMSNP . Since, as described earlier, every MMSNP -expressible problem is polynomial-time equivalent to some non-uniform constraint satisfaction problem [ 5 ] and since, as shown in [ 5 ] and in [ 15 ], every non-uniform constraint satisfaction problem is polynomial-time equivalent to some non-uniform constraint satisfaction problem on a structure with a single relation, our two main results imply that universal monotone uniform dependence logic captures, in a precise sense, all non-uniform constraint satisfaction problems CSP(B). Our results establish a tight connection between constraint satisfaction and a natural fragment of dependence logic. From the standpoint of constraint satisfaction, they contribute to the investigation of the descriptive complexity of constraint satisfaction. From the standpoint of dependence logic, they reveal that a dichotomy theorem for the computational complexity of the universal fragment of uniform dependence logic is as difficult as a dichotomy theorem for constraint satisfaction, which, to date, remains an elusive goal. 2 Background and Basic Notions All structures considered in this paper are finite and relational. Thus, a vocabulary τ is a finite set of {R1, . . . , Rn} of relation symbols, and the domain dom ( A )of each τ -structure A = ( dom ( A ) , RA 1, . . . , RA n )is assumed to be finite. However, to interpret k -valued dependence atoms, we add k constant symbols to the vocabulary; see Subsection 2.3 below. We will usually denote dom ( A )by A , dom ( B )by B , etc. For any integer k≥ 1, we will use the notation [k] = {1, . . . , k}throughout. 2.1 Constraint Satisfaction and MMSNP Ahomomorphism between two τ -structures A and B is a function h from the universe A of A to the universe B of B such that for every relation symbol R of τ and every tuple ( a1, . . . , an )of elements of A , if ( a1, . . . , an ) ∈RA , then ( h ( a1 ) , . . . , h ( an )) ∈RB . Every τ-structure Bgives rise to the following constraint satisfaction problem CSP(B): Given a τ-structure A, is there a homomorphism from Ato B? According to the usual practise, we identify the problem CSP ( B )with the class of its positive instances. Thus, we write A∈CSP(B), if the answer to the question above is “yes”. CSL 2016 14:4 Dependence Logic vs. Constraint Satisfaction Clearly, each constraint satisfaction problem CSP ( B )is in NP . Moreover, numerous natural computational problems can be viewed as constraint satisfaction problems for a suitable choice of B . For example, if Kk is the complete graph on k nodes (i.e., Kk is the k -clique), k≥ 2, then CSP ( Kk )is the k -Colorability problem. Furthermore, several variants of Satisfiability can be viewed as constraint satisfaction problems. We now give two such examples. First, consider a vocabulary τ consisting of four ternary relation symbols R0, R1, R2, R3 and let B be the τ -structure with universe { 0 , 1 } and relations RB 0 = { 0 , 1 }3\ { (0 , 0 , 0) } , RB 1 = { 0 , 1 }3\ { (1 , 0 , 0) } , RB 2 = { 0 , 1 }3\ { (1 , 1 , 0) } , RB 3 = { 0 , 1 }3\ { (1 , 1 , 1) } . It is easy to see that CSP ( B )amounts to 3-Sat, where a 3CNF-formula ϕ is encoded as a τ -structure Aϕ with universe the set of its variables and where the relation RAϕ i interpreting Ri consists of the triples of variables occurring in a clause with inegative literals, i= 0,1,2,3. Next, consider a vocabulary τ consisting of a single ternary relation symbol R and let B be the τ -structure with universe { 0 , 1 } and relation RB = { (1 , 0 , 0) , (0 , 1 , 0) , (0 , 0 , 1) } . It is easy to see that CSP ( B )amounts to Positive 1-in-3 Sat: given a 3CNF-formula ϕ consisting entirely of positive clauses, is there a truth assignment t such that, for every clause c of ϕ , the assignment t makes true exactly one of the three variables of c ? Here, ϕ is encoded as a τ -structure Aϕ with universe the set of its variables and where the relation RAϕconsists of all triples (x, y, z)of variables such that (x∨y∨z)is a clause of ϕ. As mentioned in the Introduction, Feder and Vardi [ 5 ] conjectured that, for every fixed τ -structure B , either CSP ( B )is NP -complete or CSP ( B )is solvable in polynomial time. Moreover, they showed that, for every τ -structure B , there is a structure B0 over a vocabulary consisting of a single binary relation such that CSP ( B )and CSP ( B0 )are equivalent via polynomial-time reductions. Thus, to settle the Feder-Vardi conjecture, it is enough to settle it for structures with a single binary relation (i.e., for directed graphs). Every constraint satisfaction problem CSP ( B )is expressible by a sentence of existential second-order logic that also obeys certain syntactic restrictions. For example, as discussed earlier, CSP ( K3 ), which is the same as 3-Colorability, is expressible by the sentence ∃B∃R∃G∀x∀y θ, where θis the quantifier-free formula (B(x)∨R(x)∨G(x)) ∧ ¬(B(x)∧R(x)) ∧ ¬(B(x)∧G(x))∧¬(R(x)∧G(x)) ∧¬E(x, y)∨(¬(B(x)∧B(y)) ∧ ¬(R(x)∧R(y))∧¬(G(x)∧G(y))). Similarly, Positive 1-in-3 Sat is expressible by the sentence ∃S∀x∀y∀z η , where η is the formula ¬R(x, y, z)∨(S(x)∧ ¬S(y)∧ ¬S(z)) ∨(¬S(x)∧S(y)∧ ¬S(z)) ∨(¬S(x)∧ ¬S(y)∧S(z)). The preceding sentences of existential second-order logic obey the following syntactic restrictions: (a) all second-order quantifiers are monadic; (b) all first-order quantifiers are universal; (c) no inequalities occur; (d) all occurrences of relation symbols from the underlying vocabulary τ are preceded by the negation symbol. Taken together, these syntactic restrictions define the fragment of existential second-order logic known as MMSNP. MMSNP has strictly higher expressive power than constraint satisfaction, in the sense that there are problems that are definable by a MMSNP -sentence, but are not expressible as a CSP ( B )problem for any structure B over the same vocabulary. Indeed, as pointed out in [15], the problem “given a graph, is it triangle-free?” is expressible by the sentence ∀x∀y∀z(¬E(x, y)∨ ¬E(x, z)∨ ¬E(y, z)), L. Hella and Ph. G. Kolaitis 14:5 which is in the first-order part of MMSNP , but there is no graph H such that a graph G is triangle-free if and only if there is a homomorphism from G to H . Towards a contradiction, assume that such a graph H exists. Erdös [ 3 ] showed that there are graphs of arbitrarily large girth and chromatic number. It follows that there is a graph G that is triangle-free (i.e., G has girth at least 4) and chromatic number bigger than that of H . Thus, G is triangle-free, but there is no homomorphism from G to H , else we could color G with at most the number of colors needed to color H. As mentioned in the Introduction, however, Feder and Vardi [ 5 ] showed that every MMSNP -definable problem is equivalent under polynomial-time reductions to a constraint satisfaction problem CSP ( B ), for some structure B over the same vocabulary. Consequently, establishing a dichotomy theorem for the complexity of model checking MMSNP -sentences is precisely as hard as affirming the Feder-Vardi dichotomy conjecture for constraint satisfaction. 2.2 Dependence logic Dependence logic Dis the extension of first-order logic augmented with dependence atoms dep ( x1, . . . , xn ; y ). Since dependence atoms are allowed to occur only positively in formulas of D, it is natural assume that all formulas are in negation normal form. Thus, we define the syntax of Dby the following grammar: ϕ:: = x1=x2| ¬ x1=x2|R(x1, . . . , xn)| ¬R(x1, . . . , xn)| dep(x1, . . . , xn;y)|(ϕ1∧ϕ1)|(ϕ1∨ϕ2)| ∀xϕ | ∃xϕ. The semantics of Dis defined with respect to teams, i.e., sets of assignments, instead of single assignments. If A is a structure with domain A and V is a set of first-order variables, then an assignment on A is a function s : V→A . A team on A is a set T of assignments on some fixed set V = dom ( T )of variables. In particular, if V = ∅ , then there are two teams on A with domain V : the empty team ∅ , and the team T = {∅} consisting of the empty assignment ∅:∅ → A. To define the semantics of universal quantification, we use the following notation: T [ A/x ] = {s [ a/x ] |s∈T, a ∈A} , where s [ a/x ]is the assignment such that it agrees with son all y∈dom(s)\ {x}, and s[a/x](x) = a. To define the semantics for existential quantification, we need the notion of a choice function F : T→A . The idea is that F picks an element F ( s )from the domain A of a structure A for each assignment s in a team T . The element F ( s )is then used to interpret a variable x , thus obtaining the new assignment s [ F ( s ) /x ]. We write T [ F/x ]for the team {s[F(s)/x]|s∈T}obtained from Tby making this change to each s∈T. IDefinition 1. Let A be a model and T a team on A . The truth relation A, T | = ϕ for dependence logic is defined as follows. A, T |=x1=x2⇐⇒ s(x1) = s(x2)for all s∈T. A, T |=¬x1=x2⇐⇒ s(x1)6=s(x2)for all s∈T. A, T |=R(x1, . . . , xn)⇐⇒ (s(x1), . . . , s(xn)) ∈RAfor all s∈T. A, T |=¬R(x1, . . . , xn)⇐⇒ (s(x1), . . . , s(xn)) 6∈ RAfor all s∈T. A, T |= dep(x1, . . . , xn;y)⇐⇒ there is a function f:An→Asuch that s(y) = f(s(x1), . . . , s(xn)) for all s∈T. A, T |=ϕ∧ψ⇐⇒ A, T |=ϕand A, T |=ψ. A, T |=ϕ∨ψ⇐⇒ there are T0, T00 ⊆Tsuch that T∪T0=T00, A, T0|=ϕand A, T00 |=ψ. A, T |=∀xψ ⇐⇒ A, T[A/x]|=ψ. A, T |=∃xψ ⇐⇒ there is a function F:T→As.t. A, T[F/x]|=ψ. CSL 2016 14:6 Dependence Logic vs. Constraint Satisfaction The set Fr ( ϕ )of free variables of a formula ϕ∈ Dis defined in the standard way. The formula ϕ is a sentence if Fr ( ϕ ) = ∅ . A sentence ϕ∈ Dis true in a structure A , in symbols A|=ϕ, if A,{∅} |=ϕ. Note that in the literature (see, e.g., [ 17 ]), the semantics of the dependence atom is usually stated in the following equivalent form: A, T |= dep(x1, . . . , xn;y)⇐⇒ for all s, s0∈T, if s(xi) = s0(xi)for all i∈ {1, . . . , n}, then s(y) = s0(y). Note also that, in database terminology, A, T | = dep ( x1, . . . , xn ; y )means that the team T , viewed as an n-ary relation, satisfies the functional dependency x1, . . . , xn→y. We review here briefly the basic properties of dependence logic. The first property is that the team semantics for first-order formulas in D(i.e., formulas without dependence atoms) can be reduced to the standard Tarski semantics. We write A, s | = ϕ if the first-order formula ϕis satisfied by the assignment sin the structure A. IFact 1 (Flatness, [ 17 ]) . Let ϕ be a formula of Dwithout dependence atoms, and let A be a structure and Ta team on A. Then A, T |=ϕif and only if A, s |=ϕfor all s∈T. The second property is that the semantics of every D-formula is downwards closed in the following sense. IFact 2 (Downward closure, [ 17 ]) . Let ϕ be a formula of D. If T and T0 are teams on a structure Asuch that A, T |=ϕand T0⊆T, then A, T0|=ϕ. The formulas ϕ of Dalso have the desirable property that the truth of ϕ only depends on the interpretation of its free variables Fr ( ϕ ). We use here the notation TV = {sV|s∈T} for a team Tand a set Vof variables. IFact 3 (Locality, [ 17 ]) . Let ϕ be a formula of Dwith Fr ( ϕ ) = V . If T is a team on a structure Aand T0=TV, then A, T |=ϕif and only if A, T0|=ϕ. Finally, as mentioned in the Introduction, dependence logic Dhas the same expressive power as existential second-order logic Σ1 1. IFact 4 (Dcaptures Σ 1 1 , [ 17 ]) . For every sentence ϕ of D, there is an equivalent sentence ψ of Σ1 1; vice versa, for every sentence ψof Σ1 1, there is an equivalent sentence ϕof D. As a consequence of Fact 4 and Fagin’s Theorem [ 4 ], dependence logic Dcaptures the complexity class NP . In particular, this means that NP-complete problems, such as k - Colorability and k -Sat, k≥ 3, are expressible in D. Perhaps surprisingly, it turns out that the model-checking problem of D-formulas can be NP-complete already at the quantifierfree level. Specifically, Jarmo Kontinen [ 12 ] proved that the problem “does a team T on a structure A (with empty vocabulary) satisfy the formula dep ( x ; y ) ∨dep ( u ; v ) ∨dep ( u ; v )?” is NP-complete. On the other hand, he proved that the model-checking problem for the disjunction of any two dependence atoms is in NLOGSPACE. The complexity of model-checking for quantifier-free formulas of Dhas been further investigated by Durand et al. [ 2 ]. Extending the ideas of Kontinen [ 12 ], they give sufficient syntactic criteria for the tractability and the NP-completeness of such model-checking problems. In the present paper, we focus on the relationship between the universal fragment of dependence logic, constraint satisfaction problems and MMSNP , and unveil a tight connection. L. Hella and Ph. G. Kolaitis 14:7 2.3 Logics with k-valued variables In the next subsection, we will define uniform k -valued dependence atoms. To do this, in addition to the usual first-order variables, we need a separate supply of k -valued variables. Furthermore, to interpret the k -valued variables, we will extend structures by a standard part consisting of the numbers 1 , . . . , k . Thus, if A = ( A, RA 1, . . . , RA n )is a τ -structure, then we define A [ k ]to be the two-sorted structure ( A ; [ k ] ,1A, . . . , kA ). Here [ k ]is the domain of the second sort and 1, . . . , k are constant symbols over the second sort such that iA = i for each i∈[k]. We will use the Greek letters α, β, γ , with or without subscripts, as k -valued variables, while we will use x, y, u, v as ordinary first-order variables. The intuition is that k -valued variables always range over the second sort [ k ]of a structure A [ k ], while the first-order variables range over the domain A of A . We often use the boldface notation x x x ( α α α , or a a a ) for a tuple ( x1, . . . , xn )of variables (a tuple ( α1, . . . , αn )of k -valued variables, or a tuple ( a1, . . . , an )of elements, respectively). If not explicitly defined, the length n of the tuple will be clear from the context. For logics with k -valued variables and team semantics, the notion of a team needs to be adapted. If A is a structure, and V is a finite set of first-order and k -valued variables, then an assignment on A [ k ]with domain V is a function s : V→A∪ [ k ]such that s ( x ) ∈A for each first-order variable x∈V and s ( α ) ∈ [ k ]for each k -valued variable α∈V . A team on A[k]with domain Vis a set Tof assignments s:V→A∪[k]. We will next introduce some useful notation. IDefinition 2. Let Tbe a team on a structure A[k]with domain V. If x x x∈Vn and α α α∈Vm , then we use the notation RT,x x xα α α for the ( n + m )-ary relation {s(x x xα α α)|s∈T} ⊆ An×[k]m. In case m = 0, we write simply RT,x x x = {s ( x x x ) |s∈T} . Similarly, in case n = 0, we write RT,α α α={s(α α α)|s∈T}. Furthermore, if a a a∈An , then T [ x x x=a a a ]denotes the subteam {s∈T|s ( x x x ) = a a a} ⊆ T . Similarly, if ` ` `∈[k]m, then T[α α α=` ` `]denotes the subteam {s∈T|s(α α α) = ` ` `} ⊆ T. Note that, in database terminology, RT,x x xα α α is the projection πx x xα α α ( T )of the team T on the variables x x xα α α , where T is viewed as a relation. Moreover, T [ x x x=a a a ]is the selection σx x x=a a a ( T )of the team T, where Tis viewed as a relation; similarly, T[α α α=` ` `]is the selection σα α α=` ` `(T). To simplify the notation, henceforth we will denote the structures A [ k ]simply by A . This should not cause any confusion, since it is always clear from the context, whether the symbol Arefers to a usual structure, or the extension of such structure with the second sort [k]. 2.4 Uniform k-valued dependence atoms We are now ready to define the uniform k -valued dependence atoms, which we will use in the rest of the paper. These atoms differ from the standard dependence atoms in two ways: first, they are k -valued; second, the functional dependence is generated by a single unary function. IDefinition 3. If x x x = ( x1, . . . , xn )is an n -tuple of first-order variables and α α α = ( α1, . . . , αn ) is an n -tuple of k -valued variables, then udep [ k ]( x x x ; α α α )is an atomic formula with the semantics A, T |= udep[k](x x x;α α α)⇐⇒ there is a function f:A→[k]such that s(αi) = f(s(xi)),for all i∈[n]and s∈T. Note that in the case n = 1, the uniform k -valued dependence atom udep [ k ]( x ; α )is equivalent with the k -valued version dep [ k ]( x ; α )of the ordinary dependence atom dep ( x ; y ). CSL 2016 14:8 Dependence Logic vs. Constraint Satisfaction The semantics of universal and existential quantification of k -valued variables can be defined in the same way as for quantification of first-order variables by defining T [[ k ] /α ] = {s [ i/α ] |s∈T, i ∈ [ k ] } , and T [ G/α ] = {s [ G ( s ) /α ] |s∈T} for a choice function G : T→ [ k ]. However, we will not consider existential quantification in this paper, as our main focus is on a quantifier-free fragment of the full logic with uniform k -valued dependence atoms, and its closure with respect to universal quantifiers. IDefinition 4. The quantifier-free monotone dependence logic with uniform k -valued dependence atoms,QF-MUD[k], is defined by the following grammar: ϕ:: = α=i| ¬R(x x x)|udep[k](x x x;α α α)|(ϕ1∧ϕ2)|(ϕ1∨ϕ2),where i∈[k]. Universal monotone dependence logic with uniform k -valued dependence atoms, ∀-MUD [ k ], is the extension of QF-MUD[k]defined by the grammar ϕ:: = ψ| ∀xϕ | ∀αϕ, where ψ∈QF-MUD[k]. The union of ∀-MUD [ k ]over all k≥ 1is denoted by ∀-MUD [ ω ]. Similarly, QF-MUD [ ω ]is the union of QF-MUD[k]over all k≥1. Thus, analogously to MMSNP , the logics QF-MUD [ k ]and ∀-MUD [ k ]admit no inequalities and only negative occurrences of relation symbols in the vocabulary. Note that there is no need to include equalities of the form α = β , since they can be expressed as Wi∈[k] ( α = i∧β = i ). Furthermore, inequalities between k -valued variables are also expressible: α6 = β is equivalent to Wi∈[k]α=i∧Wj∈[k],j6=iβ=j. For the sake of completeness, we state here the definition of the semantics of ∀-MUD[k]. IDefinition 5. Let A be a structure and T a team on A . The truth relation A, T | = ϕ for universal monotone uniform k-valued dependence logic is defined as follows. A, T |=α=i⇐⇒ s(α) = ifor all s∈T. A, T |=¬R(x x x)⇐⇒ (s(x1), . . . , s(xn)) 6∈ RAfor all s∈T. A, T |= udep[k](x x x;α α α)⇐⇒ there is a function f:A→[k]such that s(αi) = f(s(xi)) for all i∈[n]and s∈T. A, T |=ϕ∧ψ⇐⇒ A, T |=ϕand A, T |=ψ. A, T |=ϕ∨ψ⇐⇒ there are T0, T00 ⊆Tsuch that T0∪T00 =T, A, T0|=ϕand A, T00 |=ψ. A, T |=∀xϕ ⇐⇒ A, T[A/x]|=ϕ. A, T |=∀αϕ ⇐⇒ A, T[[k]/α]|=ϕ. Since dependence logic has the same expressive power as existential second-order logic, it is clear that uniform k -valued dependence atoms are definable in D(in the setting with k -valued variables). Indeed, it is straightforward to check that udep [ k ]( x1, . . . , xn ; α1, . . . , αn ) is equivalent to the formula ∀y∃βdep[k](y;β)∧^ i∈[n] (y=xi→β=αi). Note however, that this formula violates the syntactic restrictions of ∀-MUD [ k ]in two different ways: it contains existential quantification of a k -valued variable and inequalities between first-order variables. As in the case of dependence logic D, a formula ϕ of ∀-MUD [ k ]is a sentence, if the set Fr ( ϕ )of its free variables is empty. Furthermore, a sentence ϕ is true in a structure A , in symbols A|=ϕ, if A,{∅} |=ϕ. L. Hella and Ph. G. Kolaitis 14:9 Clearly any ∀-MUD [ k ]-sentence ϕ is equivalent to a sentence of the form ∀x x x∀α α αψ , where ψ is a QF-MUD [ k ]-formula. As a matter of fact, we can assume without loss of generality that ϕ is the universal closure of ψ , i.e., the tuple x x xα α α is repetition-free and consists of the free variables of ψ . Using the truth conditions for universal quantification of first-order and k -valued variables repeatedly, we obtain the following simple connection between the semantics of ϕand ψ: A| = ϕ if and only if A, F | = ψ , where F is the team consisting of all assignments s:V→A∪[k]with V= Fr(ψ). We will call F the full team (on A with domain V ) in the sequel. If there is need to emphasize the domain Vof F, we denote the full team by FV. The full team has a special role in the semantics of QF-MUD [ k ]also in another way. It is straightforward to verify that Facts 2 and 3 (see Subsection 2.2) remain true for ∀-MUD [ k ]. Specifically, for every formula ψ∈QF-MUD[k], the following statements are true: 1. if A, T |=ψand T0⊆T, then A, T 0|=ψ. 2. if T0=TFr(ψ), then A, T |=ψif and only if A, T0|=ψ. Thus, to decide whether a formula is satisfied by every team in a given structure, it suffices to check whether it is satisfied by the full team. We summarize the two observations concerning the full team in the following lemma. ILemma 6. Let ψ be a QF-MUD [ k ]-formula with x x x and α α α as its free variables. Then the following statements are equivalent: 1. A|=∀x x x∀α α αψ. 2. A, F |=ψ. 3. A, T |=ψ, for every team Ton Awith Fr(ψ)⊆dom(T) 3 From Constraint Satisfaction to Dependence Logic Our aim in this section is to prove that every constraint satisfaction problem CSP ( B )is captured by a sentence of ∀-MUD [ ω ]. To do this, we will prove that CSP ( B )is definable in ∀-MUD [ ω ], assuming that B is of the form ( B, RB ), i.e., B has only one relation. This suffices, since as mentioned in Subsection 2.1, every constraint satisfaction problem CSP ( B ) is equivalent, via polynomial-time reductions, to a CSP ( B0 )in which B0 is a structure with a single binary relation. We start by observing that the truth of a [ k ]-valued uniform dependence atom on a given structure Aand a given team Timplies the existence of a homomorphism between the two structures (A, RT,x x x)and ([k], RT,α α α). ILemma 7. If A, T |= udep[k](x x x;α α α), then (A, RT,x x x)∈CSP([k], RT,α α α). Proof. Assume that A, T |= udep[k](x x x;α α α). Then there is a function f:A→[k]such that f(s(xi)) = s(αi)for all i∈[n]and s∈T. This condition implies that f is a homomorphism from ( A, RT,x x x )to ([ k ] , RT,α α α ). Indeed, if a a a = ( a1, . . . , an ) ∈RT,x x x , then there exists s∈T such that s ( xi ) = ai for all i∈ [ n ]. But then also s(αi) = f(ai)holds for all i∈[n], whence (f(a1), . . . , f(an)) ∈RT,α α α.J Note that the converse implication of Lemma 7 is not true. As an example, consider the team T = {s, s0} , where s ( x1 ) = s0 ( x1 ), s ( x2 ) = s0 ( x2 ), s ( α1 ) = s ( α2 ) = 1 and s0 ( α1 ) = s0 ( α2 )=2. Then the function h : A→ [ k ]such that h ( a ) = 1 for all a∈A , is a homomorphism ( A, RT,x1x2 ) → ([ k ] , RT,α1α2 ), but clearly A, T 6| = udep [ k ]( x1, x2 ; α1, α2 ). Thus, uniform dependence atoms are different from homomorphism atoms. CSL 2016 14:16 Dependence Logic vs. Constraint Satisfaction 5 Concluding Remarks In this paper, we established a tight connection between dependence logic and constraint satisfaction. Since dependence logic has the same expressive power as existential second-order logic, it is expected that constraint satisfaction problems can be expressed in dependence logic. We believe, however, that the connection established in this paper is a priori unexpected, since we showed that a simple fragment of universal dependence logic captures, in a precise sense, the family of constraint satisfaction problems CSP ( B ), where B is a relational structure. Our results contribute to the descriptive complexity of constraint satisfaction and also shed new light on quantifier-free and universal dependence logic. The connection between universal dependence logic and constraint satisfaction is established by using MMSNP as a bridge and also the result by Feder and Vardi [ 5 ] that MMSNP captures constraint satisfaction via polynomial-time reductions. Specifically, we showed that every constraint satisfaction problem CSP ( B ), in which B has only one relation, is definable by a ∀-MUD [ ω ]-sentence, and every ∀-MUD [ ω ]-sentence is equivalent to some MMSNP -sentence. A natural question that arises from these results is whether every MMSNP - sentence is equivalent to some ∀-MUD [ ω ]-sentence or, in other words, whether MMSNP and ∀-MUD [ ω ]have the same expressive power. A related question is to identify other natural fragments of dependence logic that capture important fragments of existential second-order logic, such as strict existential second-order logic (i.e., the fragment of existential second-order logic in which all first-order quantifiers are universal). Acknowledgements. A part of the research reported here was carried out while Lauri Hella was visiting the University of California Santa Cruz. References 1Nadia Creignou, Phokion G. Kolaitis, and Heribert Vollmer, editors. Complexity of Constraints – An Overview of Current Research Themes [Result of a Dagstuhl Seminar], volume 5250 of Lecture Notes in Computer Science. Springer, 2008. 2Arnaud Durand, Juha Kontinen, Nicolas de Rugy-Altherre, and Jouko Väänänen. Tractability frontier of data complexity in team semantics. In Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2015, Genoa, Italy, 21-22nd September 2015., pages 73–85, 2015. 3Paul Erdös. Graph theory and probability. Canadian J. of Mathematics, 11:34–38, 1959. 4Ronald Fagin. Generalized first-order spectra and polynomial-time recognizable sets. In Richard Karp, editor, Complexity of Computation, number 7 in SIAM-AMS Proceedings, pages 43–73. SIAM-AMS, 1974. 5Tomás Feder and Moshe Y. Vardi. The computational structure of monotone monadic SNP and constraint satisfaction: A study through datalog and group theory. SIAM J. Comput., 28(1):57–104, 1998. 6P. Galliani. Inclusion and exclusion dependencies in team semantics – on some logics of imperfect information. Ann. Pure Appl. Logic, 163(1):68–84, 2012. 7Pietro Galliani and Lauri Hella. Inclusion logic and fixed point logic. In Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, number 23 in LIPIcs, pages 281–295. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 2013. doi: 10.4230/LIPIcs.CSL.2013.281. 8Erich Grädel and Jouko A. Väänänen. Dependence and independence. Studia Logica, 101(2):399–410, 2013. doi:10.1007/s11225-013-9479-2. L. Hella and Ph. G. Kolaitis 14:17 9Johan Håstad, Andrei A. Krokhin, and Dániel Marx. The constraint satisfaction problem: Complexity and approximability (Dagstuhl Seminar 12451). Dagstuhl Reports, 2(11):1–19, 2012. 10 Leon Henkin. Some remarks on infinitely long formulas. In Infinitistic Methods. Pergamon Press, 1961. 11 Jaakko Hintikka and Gabriel Sandu. Informational independence as a semantical phenomenon. In J. E. Fenstad et al., editor, Logic, Methodology and the Philosophy of Science VIII, pages 571–89. North-Holland, 1989. 12 Jarmo Kontinen. Coherence and computational complexity of quantifier-free dependence logic formulas. Studia Logica, 101(2):267–291, 2013. doi:10.1007/s11225-013-9481-8. 13 Juha Kontinen and Jouko A. Väänänen. On definability in dependence logic. Journal of Logic, Language and Information, 18(3):317–332, 2009. doi:10.1007/s10849-009-9082-0. 14 Juha Kontinen and Jouko A. Väänänen. Axiomatizing first-order consequences in dependence logic. Ann. Pure Appl. Logic, 164(11):1101–1117, 2013. doi:10.1016/j.apal.2013. 05.006. 15 Gábor Kun and Jaroslav Nesetril. Forbidden lifts (NP and CSP for combinatorialists). Eur. J. Comb., 29(4):930–945, 2008. 16 Richard E. Ladner. On the structure of polynomial time reducibility. J. ACM, 22(1):155– 171, 1975. 17 Jouko A. Väänänen. Dependence Logic – A New Approach to Independence Friendly Logic, volume 70 of London Mathematical Society student texts. Cambridge University Press, 2007. URL: http://www.cambridge.org/de/knowledge/isbn/item1164246/. CSL 2016