Dependence Logic vs. Constraint Satisfaction

Dependence Logic s. Cons ain Sa is ac ion Lau i Hella∗1and Phokion G. Kolai is†2 1 School o In o ma ion Sciences, Uni e si y o Tampe e, Finland [email p o ec ed] 2 Uni e si y o Cali o nia San a C uz and IBM Resea ch – Almaden, USA [email p o ec ed] Abs ac Du ing he pas decade, dependence logic has eme ged as a o malism sui able o exp essing and analyzing no ions o dependence and independence ha a ise in di e en scien i ic a eas. The sen ences o dependence logic ha e he same exp essi e powe as hose o exis en ial second-o de logic, hence dependence logic cap u es NP on he class o all ini e s uc u es. In his pape , we iden i y a na u al agmen o uni e sal dependence logic and show ha , in a p ecise sense, i cap u es cons ain sa is ac ion. This igh connec ion be ween dependence logic and cons ain sa is ac ion con ibu es o he desc ip i e complexi y o cons ain sa is ac ion and elucida es he exp essi e powe o uni e sal dependence logic. 1998 ACM Subjec Classi ica ion F.4.1 Ma hema ical Logic, F.1.3 Complexi y Measu es and Classes Keywo ds and ph ases Dependence logic, cons ain sa is ac ion, compu a ional complexi y, ex- p essi e powe Digi al Objec Iden i ie 10.4230/LIPIcs.CSL.2016.14 1 In oduc ion Dependence logic is a o malism o exp essing and analyzing no ions o dependence and independence ha a e encoun e ed ac oss di e en a eas o compu e science and ma hema ics, om unc ional dependencies in ela ional da abases o independence in linea algeb a and in p obabili y heo y. E en hough i s o igins can be aced back o Henkin quan i ie s [ 10 ] and o independence- iendly logic [ 11 ], dependence logic was ully de eloped by Väänänen in his monog aph [ 17 ], which became he ca alys o nume ous subsequen in es iga ions (see, e.g., [ 6 , 7 , 8 , 13 , 14 ]). The syn ax o dependence logic uses dependence a oms as he main building blocks; hese a oms asse ha a unc ional dependency be ween a iables holds, i.e., ha a ce ain a iable is a unc ion o some o he a iables. The seman ics o dependence logic uses se s o assignmen s, called eams, ins ead o single assignmen s o alues o a iables. In e ms o exp essi e powe and as ega ds sen ences, dependence logic has he same exp essi e powe as exis en ial second-o de logic [ 13 ]. Combined wi h Fagin’s Theo em [ 4 ], his esul implies ha , on classes o ini e s uc u es, he sen ences o dependence logic can exp ess p ecisely all decision p oblems in NP. Cons ain sa is ac ion comp ises a se o algo i hmic p oblems ha a e ubiqui ous in se e al di e en a eas o compu e science. An in luen ial pape by Fede and Va di [ 5 ] p o ided he impe us o an in-dep h and s ill ongoing in es iga ion o he connec ions ∗ The esea ch o Lau i Hella was pa ially suppo ed by a P o esso Pool’s G an o he Finnish Cul u al Founda ion. †The esea ch o Phokion Kolai is was pa ially suppo ed by NSF G an IIS-1217869. ©Lau i Hella and Phokion G. Kolai is; licensed unde C ea i e Commons License CC-BY 25 h EACSL Annual Con e ence on Compu e Science Logic (CSL 2016). Edi o s: Jean-Ma c Talbo and Lau en Regnie ; A icle No. 14; pp. 14:1–14:17 Leibniz In e na ional P oceedings in In o ma ics Schloss Dags uhl – Leibniz-Zen um ü In o ma ik, Dags uhl Publishing, Ge many 14:2 Dependence Logic s. Cons ain Sa is ac ion be ween cons ain sa is ac ion, compu a ional complexi y, logic, and uni e sal algeb a (see, e.g., [ 1 , 9 ]). Fede and Va di a gued con incingly ha , in i s mos gene al o m, cons ain sa is ac ion can be iden i ied wi h he Homomo phism P oblem: gi en wo ela ional s uc u es A and B , is he e a homomo phism om A o B ? Clea ly, he Homomo phism P oblem is NP-comple e, since i con ains, o example, 3-Sa is iabili y as a special case. Mo eo e , each ixed ela ional s uc u e B gi es ise o he non-uni o m cons ain sa is ac ion p oblem CSP ( B ): gi en a ela ional s uc u e A , is he e a homomo phism om A o B ? The compu a ional complexi y o each such p oblem depends on he s uc u e B . Fede and Va di conjec u ed ha he amily o all cons ain sa is ac ion p oblems CSP ( B ) exhibi s he ollowing dicho omy: o each B , ei he CSP ( B )is NP-comple e o CSP ( B )is sol able in polynomial ime. This conjec u e emains open o da e, in spi e o conce ed e o s by di e en g oups o esea che s ha , so a , ha e es ablished only special cases o i . Fede and Va di [ 5 ] also in es iga ed he desc ip i e complexi y o cons ain sa is ac ion. To his e ec , hey iden i ied a agmen o exis en ial second-o de logic, called monadic mono one s ic NP wi hou inequali y o , in sho , MMSNP , and showed ha i cap u es, in a p ecise sense, he amily CSP ( B )o all non-uni o m cons ain sa is ac ion p oblems. MMSNP consis s o all sen ences o exis en ial second o de logic ha ha e he ollowing p ope ies (whe e i is assumed ha all nega ion symbols occu ing in he sen ences ha e been pushed inwa d, so ha hey apply o a omic o mulas only): (a) all second-o de quan i ie s a e monadic; (b) all i s -o de quan i ie s a e uni e sal; (c) no inequali ies occu in he o mula; (d) all occu ences o ela ion symbols om he unde lying ocabula y a e p eceded by he nega ion symbol. MMSNP cap u es cons ain sa is ac ion in he ollowing way. Fi s , i is easy o see ha i B is a ela ional s uc u e, hen CSP ( B )is exp essible in MMSNP . Second, Fede and Va di showed ha e e y MMSNP -exp essible p oblem is equi alen o a CSP ( B ), o some ela ional s uc u e B , unde polynomial- ime educ ions (o iginally, his equi alence was p o ed unde andomized polynomial- ime educ ions, which, howe e , we e subsequen ly de andomized [ 15 ]). No e ha Fede and Va di also showed ha i one o he a o emen ioned p ope ies (a), (b), (c), (d) de ining MMSNP is d opped, hen e e y p oblem in NP is equi alen unde polynomial- ime educ ions o a p oblem in he esul ing agmen o exis en ial second-o de logic. Combined wi h Ladne ’s Theo em [ 16 ], his implies ha i one o hese ou p ope ies is d opped, hen he esul ing agmen can exp ess decision p oblems ha a e nei he NP-comple e, no sol able in polynomial ime (unless P=NP). As seen om he p eceding discussion, dependence logic cap u es exis en ial second-o de logic, while cons ain sa is ac ion is cap u ed by a p ope agmen o exis en ial second-o de logic. This s a e o a ai s gi es ise o he ollowing ques ion: is he e a na u al agmen o dependence logic ha cap u es cons ain sa is ac ion? In his pape , we show ha his is indeed he case. In ac , we iden i y a agmen o a a ian o dependence logic consis ing o uni e sal sen ences and show ha i can cap u e, in a p ecise sense, cons ain sa is ac ion. In wha ollows in his sec ion, we p esen a high-le el desc ip ion o ou main esul s. The building blocks o dependence logic, as de eloped by Väänänen, a e dependence a oms dep ( x x x ; y ), whe e x x x is a uple o a iables and y is a single a iable. A eam (i.e., a se o assignmen s) sa is ies such an a om i whene e wo assignmen s in he eam ag ee on he a iables in x x x , hey mus also ag ee on he a iable y . He e, we in oduce a a ian o dependence a oms, which we call uni o m dependence a oms; hey a e exp essions o he o m udep ( x1, . . . , xn ; α1, . . . , αn )wi h he ollowing seman ics: a eam T sa is ies udep ( x1, . . . , xn ; α1, . . . , αn )i he e is a una y unc ion such ha o e e y assignmen s in T , we ha e ha s ( αi ) = ( s ( xi )), o 1 ≤i≤n . E en hough uni o m dependence a oms ha e no been s udied in hei own igh in ea lie wo k on dependence logic, we belie e ha L. Hella and Ph. G. Kolai is 14:3 hey a e e y na u al as hey exp ess scena ios in which n di e en obse e s use senso s o measu ing ins umen s o collec da a in di e en si es, and hen each obse e applies he same unc ion o he da a collec ed o ob ain a alue. As a conc e e example, each xi may ep esen a lis o empe a u e alues collec ed a si e i a egula in e als o ime each day, while αimay s and o he maximum empe a u e a si e i. We conside k - alued uni o m dependence a oms in which he a iables α1, . . . , αn ake alues in a domain wi h k elemen s, o some ixed k≥ 1. We de ine he uni e sal mono one uni o m dependence logic ∀-MUD [ k ]as he closu e unde uni e sal quan i ica ion o all quan i ie - ee o mulas ha con ain all k - alued uni o m dependence a oms, all equali ies be ween k - alued a iables and cons an s, and all nega ed ela ional a oms, and a e closed unde disjunc ions and conjunc ions. The seman ics o he logic ∀-MUD [ k ]a e gi en using eams as in (s anda d) dependence logic. Ou i s main esul asse s ha e e y non-uni o m cons ain sa is ac ion p oblem CSP ( B )such ha B has a single ela ion is exp essible by a sen ence o ∀-MUD [ k ], whe e k is he numbe o elemen s in he uni e se o B . Ou second main esul asse s ha e e y sen ence o ∀-MUD [ k ], k≥ 1, is equi alen o a sen ence o MMSNP . Since, as desc ibed ea lie , e e y MMSNP -exp essible p oblem is polynomial- ime equi alen o some non-uni o m cons ain sa is ac ion p oblem [ 5 ] and since, as shown in [ 5 ] and in [ 15 ], e e y non-uni o m cons ain sa is ac ion p oblem is polynomial- ime equi alen o some non-uni o m cons ain sa is ac ion p oblem on a s uc u e wi h a single ela ion, ou wo main esul s imply ha uni e sal mono one uni o m dependence logic cap u es, in a p ecise sense, all non-uni o m cons ain sa is ac ion p oblems CSP(B). Ou esul s es ablish a igh connec ion be ween cons ain sa is ac ion and a na u al agmen o dependence logic. F om he s andpoin o cons ain sa is ac ion, hey con ibu e o he in es iga ion o he desc ip i e complexi y o cons ain sa is ac ion. F om he s andpoin o dependence logic, hey e eal ha a dicho omy heo em o he compu a ional complexi y o he uni e sal agmen o uni o m dependence logic is as di icul as a dicho omy heo em o cons ain sa is ac ion, which, o da e, emains an elusi e goal. 2 Backg ound and Basic No ions All s uc u es conside ed in his pape a e ini e and ela ional. Thus, a ocabula y τ is a ini e se o {R1, . . . , Rn} o ela ion symbols, and he domain dom ( A )o each τ -s uc u e A = ( dom ( A ) , RA 1, . . . , RA n )is assumed o be ini e. Howe e , o in e p e k - alued dependence a oms, we add k cons an symbols o he ocabula y; see Subsec ion 2.3 below. We will usually deno e dom ( A )by A , dom ( B )by B , e c. Fo any in ege k≥ 1, we will use he no a ion [k] = {1, . . . , k} h oughou . 2.1 Cons ain Sa is ac ion and MMSNP Ahomomo phism be ween wo τ -s uc u es A and B is a unc ion h om he uni e se A o A o he uni e se B o B such ha o e e y ela ion symbol R o τ and e e y uple ( a1, . . . , an )o elemen s o A , i ( a1, . . . , an ) ∈RA , hen ( h ( a1 ) , . . . , h ( an )) ∈RB . E e y τ-s uc u e Bgi es ise o he ollowing cons ain sa is ac ion p oblem CSP(B): Gi en a τ-s uc u e A, is he e a homomo phism om A o B? Acco ding o he usual p ac ise, we iden i y he p oblem CSP ( B )wi h he class o i s posi i e ins ances. Thus, we w i e A∈CSP(B), i he answe o he ques ion abo e is “yes”. CSL 2016 14:4 Dependence Logic s. Cons ain Sa is ac ion Clea ly, each cons ain sa is ac ion p oblem CSP ( B )is in NP . Mo eo e , nume ous na u al compu a ional p oblems can be iewed as cons ain sa is ac ion p oblems o a sui able choice o B . Fo example, i Kk is he comple e g aph on k nodes (i.e., Kk is he k -clique), k≥ 2, hen CSP ( Kk )is he k -Colo abili y p oblem. Fu he mo e, se e al a ian s o Sa is iabili y can be iewed as cons ain sa is ac ion p oblems. We now gi e wo such examples. Fi s , conside a ocabula y τ consis ing o ou e na y ela ion symbols R0, R1, R2, R3 and le B be he τ -s uc u e wi h uni e se { 0 , 1 } and ela ions 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) } . I is easy o see ha CSP ( B )amoun s o 3-Sa , whe e a 3CNF- o mula ϕ is encoded as a τ -s uc u e Aϕ wi h uni e se he se o i s a iables and whe e he ela ion RAϕ i in e p e ing Ri consis s o he iples o a iables occu ing in a clause wi h inega i e li e als, i= 0,1,2,3. Nex , conside a ocabula y τ consis ing o a single e na y ela ion symbol R and le B be he τ -s uc u e wi h uni e se { 0 , 1 } and ela ion RB = { (1 , 0 , 0) , (0 , 1 , 0) , (0 , 0 , 1) } . I is easy o see ha CSP ( B )amoun s o Posi i e 1-in-3 Sa : gi en a 3CNF- o mula ϕ consis ing en i ely o posi i e clauses, is he e a u h assignmen such ha , o e e y clause c o ϕ , he assignmen makes ue exac ly one o he h ee a iables o c ? He e, ϕ is encoded as a τ -s uc u e Aϕ wi h uni e se he se o i s a iables and whe e he ela ion RAϕconsis s o all iples (x, y, z)o a iables such ha (x∨y∨z)is a clause o ϕ. As men ioned in he In oduc ion, Fede and Va di [ 5 ] conjec u ed ha , o e e y ixed τ -s uc u e B , ei he CSP ( B )is NP -comple e o CSP ( B )is sol able in polynomial ime. Mo eo e , hey showed ha , o e e y τ -s uc u e B , he e is a s uc u e B0 o e a ocabula y consis ing o a single bina y ela ion such ha CSP ( B )and CSP ( B0 )a e equi alen ia polynomial- ime educ ions. Thus, o se le he Fede -Va di conjec u e, i is enough o se le i o s uc u es wi h a single bina y ela ion (i.e., o di ec ed g aphs). E e y cons ain sa is ac ion p oblem CSP ( B )is exp essible by a sen ence o exis en ial second-o de logic ha also obeys ce ain syn ac ic es ic ions. Fo example, as discussed ea lie , CSP ( K3 ), which is he same as 3-Colo abili y, is exp essible by he sen ence ∃B∃R∃G∀x∀y θ, whe e θis he quan i ie - ee o mula (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))). Simila ly, Posi i e 1-in-3 Sa is exp essible by he sen ence ∃S∀x∀y∀z η , whe e η is he o mula ¬R(x, y, z)∨(S(x)∧ ¬S(y)∧ ¬S(z)) ∨(¬S(x)∧S(y)∧ ¬S(z)) ∨(¬S(x)∧ ¬S(y)∧S(z)). The p eceding sen ences o exis en ial second-o de logic obey he ollowing syn ac ic es ic ions: (a) all second-o de quan i ie s a e monadic; (b) all i s -o de quan i ie s a e uni e sal; (c) no inequali ies occu ; (d) all occu ences o ela ion symbols om he unde lying ocabula y τ a e p eceded by he nega ion symbol. Taken oge he , hese syn ac ic es ic ions de ine he agmen o exis en ial second-o de logic known as MMSNP. MMSNP has s ic ly highe exp essi e powe han cons ain sa is ac ion, in he sense ha he e a e p oblems ha a e de inable by a MMSNP -sen ence, bu a e no exp essible as a CSP ( B )p oblem o any s uc u e B o e he same ocabula y. Indeed, as poin ed ou in [15], he p oblem “gi en a g aph, is i iangle- ee?” is exp essible by he sen ence ∀x∀y∀z(¬E(x, y)∨ ¬E(x, z)∨ ¬E(y, z)), L. Hella and Ph. G. Kolai is 14:5 which is in he i s -o de pa o MMSNP , bu he e is no g aph H such ha a g aph G is iangle- ee i and only i he e is a homomo phism om G o H . Towa ds a con adic ion, assume ha such a g aph H exis s. E dös [ 3 ] showed ha he e a e g aphs o a bi a ily la ge gi h and ch oma ic numbe . I ollows ha he e is a g aph G ha is iangle- ee (i.e., G has gi h a leas 4) and ch oma ic numbe bigge han ha o H . Thus, G is iangle- ee, bu he e is no homomo phism om G o H , else we could colo G wi h a mos he numbe o colo s needed o colo H. As men ioned in he In oduc ion, howe e , Fede and Va di [ 5 ] showed ha e e y MMSNP -de inable p oblem is equi alen unde polynomial- ime educ ions o a cons ain sa is ac ion p oblem CSP ( B ), o some s uc u e B o e he same ocabula y. Consequen ly, es ablishing a dicho omy heo em o he complexi y o model checking MMSNP -sen ences is p ecisely as ha d as a i ming he Fede -Va di dicho omy conjec u e o cons ain sa is ac ion. 2.2 Dependence logic Dependence logic Dis he ex ension o i s -o de logic augmen ed wi h dependence a oms dep ( x1, . . . , xn ; y ). Since dependence a oms a e allowed o occu only posi i ely in o mulas o D, i is na u al assume ha all o mulas a e in nega ion no mal o m. Thus, we de ine he syn ax o Dby he ollowing g amma : ϕ:: = x1=x2| ¬ x1=x2|R(x1, . . . , xn)| ¬R(x1, . . . , xn)| dep(x1, . . . , xn;y)|(ϕ1∧ϕ1)|(ϕ1∨ϕ2)| ∀xϕ | ∃xϕ. The seman ics o Dis de ined wi h espec o eams, i.e., se s o assignmen s, ins ead o single assignmen s. I A is a s uc u e wi h domain A and V is a se o i s -o de a iables, hen an assignmen on A is a unc ion s : V→A . A eam on A is a se T o assignmen s on some ixed se V = dom ( T )o a iables. In pa icula , i V = ∅ , hen he e a e wo eams on A wi h domain V : he emp y eam ∅ , and he eam T = {∅} consis ing o he emp y assignmen ∅:∅ → A. To de ine he seman ics o uni e sal quan i ica ion, we use he ollowing no a ion: T [ A/x ] = {s [ a/x ] |s∈T, a ∈A} , whe e s [ a/x ]is he assignmen such ha i ag ees wi h son all y∈dom(s) {x}, and s[a/x](x) = a. To de ine he seman ics o exis en ial quan i ica ion, we need he no ion o a choice unc ion F : T→A . The idea is ha F picks an elemen F ( s ) om he domain A o a s uc u e A o each assignmen s in a eam T . The elemen F ( s )is hen used o in e p e a a iable x , hus ob aining he new assignmen s [ F ( s ) /x ]. We w i e T [ F/x ] o he eam {s[F(s)/x]|s∈T}ob ained om Tby making his change o each s∈T. IDe ini ion 1. Le A be a model and T a eam on A . The u h ela ion A, T | = ϕ o dependence logic is de ined as ollows. A, T |=x1=x2⇐⇒ s(x1) = s(x2) o all s∈T. A, T |=¬x1=x2⇐⇒ s(x1)6=s(x2) o all s∈T. A, T |=R(x1, . . . , xn)⇐⇒ (s(x1), . . . , s(xn)) ∈RA o all s∈T. A, T |=¬R(x1, . . . , xn)⇐⇒ (s(x1), . . . , s(xn)) 6∈ RA o all s∈T. A, T |= dep(x1, . . . , xn;y)⇐⇒ he e is a unc ion :An→Asuch ha s(y) = (s(x1), . . . , s(xn)) o all s∈T. A, T |=ϕ∧ψ⇐⇒ A, T |=ϕand A, T |=ψ. A, T |=ϕ∨ψ⇐⇒ he e a e T0, T00 ⊆Tsuch ha T∪T0=T00, A, T0|=ϕand A, T00 |=ψ. A, T |=∀xψ ⇐⇒ A, T[A/x]|=ψ. A, T |=∃xψ ⇐⇒ he e is a unc ion F:T→As. . A, T[F/x]|=ψ. CSL 2016 14:6 Dependence Logic s. Cons ain Sa is ac ion The se F ( ϕ )o ee a iables o a o mula ϕ∈ Dis de ined in he s anda d way. The o mula ϕ is a sen ence i F ( ϕ ) = ∅ . A sen ence ϕ∈ Dis ue in a s uc u e A , in symbols A|=ϕ, i A,{∅} |=ϕ. No e ha in he li e a u e (see, e.g., [ 17 ]), he seman ics o he dependence a om is usually s a ed in he ollowing equi alen o m: A, T |= dep(x1, . . . , xn;y)⇐⇒ o all s, s0∈T, i s(xi) = s0(xi) o all i∈ {1, . . . , n}, hen s(y) = s0(y). No e also ha , in da abase e minology, A, T | = dep ( x1, . . . , xn ; y )means ha he eam T , iewed as an n-a y ela ion, sa is ies he unc ional dependency x1, . . . , xn→y. We e iew he e b ie ly he basic p ope ies o dependence logic. The i s p ope y is ha he eam seman ics o i s -o de o mulas in D(i.e., o mulas wi hou dependence a oms) can be educed o he s anda d Ta ski seman ics. We w i e A, s | = ϕ i he i s -o de o mula ϕis sa is ied by he assignmen sin he s uc u e A. IFac 1 (Fla ness, [ 17 ]) . Le ϕ be a o mula o Dwi hou dependence a oms, and le A be a s uc u e and Ta eam on A. Then A, T |=ϕi and only i A, s |=ϕ o all s∈T. The second p ope y is ha he seman ics o e e y D- o mula is downwa ds closed in he ollowing sense. IFac 2 (Downwa d closu e, [ 17 ]) . Le ϕ be a o mula o D. I T and T0 a e eams on a s uc u e Asuch ha A, T |=ϕand T0⊆T, hen A, T0|=ϕ. The o mulas ϕ o Dalso ha e he desi able p ope y ha he u h o ϕ only depends on he in e p e a ion o i s ee a iables F ( ϕ ). We use he e he no a ion TV = {sV|s∈T} o a eam Tand a se Vo a iables. IFac 3 (Locali y, [ 17 ]) . Le ϕ be a o mula o Dwi h F ( ϕ ) = V . I T is a eam on a s uc u e Aand T0=TV, hen A, T |=ϕi and only i A, T0|=ϕ. Finally, as men ioned in he In oduc ion, dependence logic Dhas he same exp essi e powe as exis en ial second-o de logic Σ1 1. IFac 4 (Dcap u es Σ 1 1 , [ 17 ]) . Fo e e y sen ence ϕ o D, he e is an equi alen sen ence ψ o Σ1 1; ice e sa, o e e y sen ence ψo Σ1 1, he e is an equi alen sen ence ϕo D. As a consequence o Fac 4 and Fagin’s Theo em [ 4 ], dependence logic Dcap u es he complexi y class NP . In pa icula , his means ha NP-comple e p oblems, such as k - Colo abili y and k -Sa , k≥ 3, a e exp essible in D. Pe haps su p isingly, i u ns ou ha he model-checking p oblem o D- o mulas can be NP-comple e al eady a he quan i ie - ee le el. Speci ically, Ja mo Kon inen [ 12 ] p o ed ha he p oblem “does a eam T on a s uc u e A (wi h emp y ocabula y) sa is y he o mula dep ( x ; y ) ∨dep ( u ; ) ∨dep ( u ; )?” is NP-comple e. On he o he hand, he p o ed ha he model-checking p oblem o he disjunc ion o any wo dependence a oms is in NLOGSPACE. The complexi y o model-checking o quan i ie - ee o mulas o Dhas been u he in es iga ed by Du and e al. [ 2 ]. Ex ending he ideas o Kon inen [ 12 ], hey gi e su icien syn ac ic c i e ia o he ac abili y and he NP-comple eness o such model-checking p oblems. In he p esen pape , we ocus on he ela ionship be ween he uni e sal agmen o dependence logic, cons ain sa is ac ion p oblems and MMSNP , and un eil a igh connec ion. L. Hella and Ph. G. Kolai is 14:7 2.3 Logics wi h k- alued a iables In he nex subsec ion, we will de ine uni o m k - alued dependence a oms. To do his, in addi ion o he usual i s -o de a iables, we need a sepa a e supply o k - alued a iables. Fu he mo e, o in e p e he k - alued a iables, we will ex end s uc u es by a s anda d pa consis ing o he numbe s 1 , . . . , k . Thus, i A = ( A, RA 1, . . . , RA n )is a τ -s uc u e, hen we de ine A [ k ] o be he wo-so ed s uc u e ( A ; [ k ] ,1A, . . . , kA ). He e [ k ]is he domain o he second so and 1, . . . , k a e cons an symbols o e he second so such ha iA = i o each i∈[k]. We will use he G eek le e s α, β, γ , wi h o wi hou subsc ip s, as k - alued a iables, while we will use x, y, u, as o dina y i s -o de a iables. The in ui ion is ha k - alued a iables always ange o e he second so [ k ]o a s uc u e A [ k ], while he i s -o de a iables ange o e he domain A o A . We o en use he bold ace no a ion x x x ( α α α , o a a a ) o a uple ( x1, . . . , xn )o a iables (a uple ( α1, . . . , αn )o k - alued a iables, o a uple ( a1, . . . , an )o elemen s, espec i ely). I no explici ly de ined, he leng h n o he uple will be clea om he con ex . Fo logics wi h k - alued a iables and eam seman ics, he no ion o a eam needs o be adap ed. I A is a s uc u e, and V is a ini e se o i s -o de and k - alued a iables, hen an assignmen on A [ k ]wi h domain V is a unc ion s : V→A∪ [ k ]such ha s ( x ) ∈A o each i s -o de a iable x∈V and s ( α ) ∈ [ k ] o each k - alued a iable α∈V . A eam on A[k]wi h domain Vis a se To assignmen s s:V→A∪[k]. We will nex in oduce some use ul no a ion. IDe ini ion 2. Le Tbe a eam on a s uc u e A[k]wi h domain V. I x x x∈Vn and α α α∈Vm , hen we use he no a ion RT,x x xα α α o he ( n + m )-a y ela ion {s(x x xα α α)|s∈T} ⊆ An×[k]m. In case m = 0, we w i e simply RT,x x x = {s ( x x x ) |s∈T} . Simila ly, in case n = 0, we w i e RT,α α α={s(α α α)|s∈T}. Fu he mo e, i a a a∈An , hen T [ x x x=a a a ]deno es he sub eam {s∈T|s ( x x x ) = a a a} ⊆ T . Simila ly, i ` ` `∈[k]m, hen T[α α α=` ` `]deno es he sub eam {s∈T|s(α α α) = ` ` `} ⊆ T. No e ha , in da abase e minology, RT,x x xα α α is he p ojec ion πx x xα α α ( T )o he eam T on he a iables x x xα α α , whe e T is iewed as a ela ion. Mo eo e , T [ x x x=a a a ]is he selec ion σx x x=a a a ( T )o he eam T, whe e Tis iewed as a ela ion; simila ly, T[α α α=` ` `]is he selec ion σα α α=` ` `(T). To simpli y he no a ion, hence o h we will deno e he s uc u es A [ k ]simply by A . This should no cause any con usion, since i is always clea om he con ex , whe he he symbol A e e s o a usual s uc u e, o he ex ension o such s uc u e wi h he second so [k]. 2.4 Uni o m k- alued dependence a oms We a e now eady o de ine he uni o m k - alued dependence a oms, which we will use in he es o he pape . These a oms di e om he s anda d dependence a oms in wo ways: i s , hey a e k - alued; second, he unc ional dependence is gene a ed by a single una y unc ion. IDe ini ion 3. I x x x = ( x1, . . . , xn )is an n - uple o i s -o de a iables and α α α = ( α1, . . . , αn ) is an n - uple o k - alued a iables, hen udep [ k ]( x x x ; α α α )is an a omic o mula wi h he seman ics A, T |= udep[k](x x x;α α α)⇐⇒ he e is a unc ion :A→[k]such ha s(αi) = (s(xi)), o all i∈[n]and s∈T. No e ha in he case n = 1, he uni o m k - alued dependence a om udep [ k ]( x ; α )is equi alen wi h he k - alued e sion dep [ k ]( x ; α )o he o dina y dependence a om dep ( x ; y ). CSL 2016 14:8 Dependence Logic s. Cons ain Sa is ac ion The seman ics o uni e sal and exis en ial quan i ica ion o k - alued a iables can be de ined in he same way as o quan i ica ion o i s -o de a iables by de ining T [[ k ] /α ] = {s [ i/α ] |s∈T, i ∈ [ k ] } , and T [ G/α ] = {s [ G ( s ) /α ] |s∈T} o a choice unc ion G : T→ [ k ]. Howe e , we will no conside exis en ial quan i ica ion in his pape , as ou main ocus is on a quan i ie - ee agmen o he ull logic wi h uni o m k - alued dependence a oms, and i s closu e wi h espec o uni e sal quan i ie s. IDe ini ion 4. The quan i ie - ee mono one dependence logic wi h uni o m k - alued de- pendence a oms,QF-MUD[k], is de ined by he ollowing g amma : ϕ:: = α=i| ¬R(x x x)|udep[k](x x x;α α α)|(ϕ1∧ϕ2)|(ϕ1∨ϕ2),whe e i∈[k]. Uni e sal mono one dependence logic wi h uni o m k - alued dependence a oms, ∀-MUD [ k ], is he ex ension o QF-MUD[k]de ined by he g amma ϕ:: = ψ| ∀xϕ | ∀αϕ, whe e ψ∈QF-MUD[k]. The union o ∀-MUD [ k ]o e all k≥ 1is deno ed by ∀-MUD [ ω ]. Simila ly, QF-MUD [ ω ]is he union o QF-MUD[k]o e all k≥1. Thus, analogously o MMSNP , he logics QF-MUD [ k ]and ∀-MUD [ k ]admi no inequali ies and only nega i e occu ences o ela ion symbols in he ocabula y. No e ha he e is no need o include equali ies o he o m α = β , since hey can be exp essed as Wi∈[k] ( α = i∧β = i ). Fu he mo e, inequali ies be ween k - alued a iables a e also exp essible: α6 = β is equi alen o Wi∈[k]α=i∧Wj∈[k],j6=iβ=j. Fo he sake o comple eness, we s a e he e he de ini ion o he seman ics o ∀-MUD[k]. IDe ini ion 5. Le A be a s uc u e and T a eam on A . The u h ela ion A, T | = ϕ o uni e sal mono one uni o m k- alued dependence logic is de ined as ollows. A, T |=α=i⇐⇒ s(α) = i o all s∈T. A, T |=¬R(x x x)⇐⇒ (s(x1), . . . , s(xn)) 6∈ RA o all s∈T. A, T |= udep[k](x x x;α α α)⇐⇒ he e is a unc ion :A→[k]such ha s(αi) = (s(xi)) o all i∈[n]and s∈T. A, T |=ϕ∧ψ⇐⇒ A, T |=ϕand A, T |=ψ. A, T |=ϕ∨ψ⇐⇒ he e a e T0, T00 ⊆Tsuch ha T0∪T00 =T, A, T0|=ϕand A, T00 |=ψ. A, T |=∀xϕ ⇐⇒ A, T[A/x]|=ϕ. A, T |=∀αϕ ⇐⇒ A, T[[k]/α]|=ϕ. Since dependence logic has he same exp essi e powe as exis en ial second-o de logic, i is clea ha uni o m k - alued dependence a oms a e de inable in D(in he se ing wi h k - alued a iables). Indeed, i is s aigh o wa d o check ha udep [ k ]( x1, . . . , xn ; α1, . . . , αn ) is equi alen o he o mula ∀y∃βdep[k](y;β)∧^ i∈[n] (y=xi→β=αi). No e howe e , ha his o mula iola es he syn ac ic es ic ions o ∀-MUD [ k ]in wo di e en ways: i con ains exis en ial quan i ica ion o a k - alued a iable and inequali ies be ween i s -o de a iables. As in he case o dependence logic D, a o mula ϕ o ∀-MUD [ k ]is a sen ence, i he se F ( ϕ )o i s ee a iables is emp y. Fu he mo e, a sen ence ϕ is ue in a s uc u e A , in symbols A|=ϕ, i A,{∅} |=ϕ. L. Hella and Ph. G. Kolai is 14:9 Clea ly any ∀-MUD [ k ]-sen ence ϕ is equi alen o a sen ence o he o m ∀x x x∀α α αψ , whe e ψ is a QF-MUD [ k ]- o mula. As a ma e o ac , we can assume wi hou loss o gene ali y ha ϕ is he uni e sal closu e o ψ , i.e., he uple x x xα α α is epe i ion- ee and consis s o he ee a iables o ψ . Using he u h condi ions o uni e sal quan i ica ion o i s -o de and k - alued a iables epea edly, we ob ain he ollowing simple connec ion be ween he seman ics o ϕand ψ: A| = ϕ i and only i A, F | = ψ , whe e F is he eam consis ing o all assignmen s s:V→A∪[k]wi h V= F (ψ). We will call F he ull eam (on A wi h domain V ) in he sequel. I he e is need o emphasize he domain Vo F, we deno e he ull eam by FV. The ull eam has a special ole in he seman ics o QF-MUD [ k ]also in ano he way. I is s aigh o wa d o e i y ha Fac s 2 and 3 (see Subsec ion 2.2) emain ue o ∀-MUD [ k ]. Speci ically, o e e y o mula ψ∈QF-MUD[k], he ollowing s a emen s a e ue: 1. i A, T |=ψand T0⊆T, hen A, T 0|=ψ. 2. i T0=TF (ψ), hen A, T |=ψi and only i A, T0|=ψ. Thus, o decide whe he a o mula is sa is ied by e e y eam in a gi en s uc u e, i su ices o check whe he i is sa is ied by he ull eam. We summa ize he wo obse a ions conce ning he ull eam in he ollowing lemma. ILemma 6. Le ψ be a QF-MUD [ k ]- o mula wi h x x x and α α α as i s ee a iables. Then he ollowing s a emen s a e equi alen : 1. A|=∀x x x∀α α αψ. 2. A, F |=ψ. 3. A, T |=ψ, o e e y eam Ton Awi h F (ψ)⊆dom(T) 3 F om Cons ain Sa is ac ion o Dependence Logic Ou aim in his sec ion is o p o e ha e e y cons ain sa is ac ion p oblem CSP ( B )is cap u ed by a sen ence o ∀-MUD [ ω ]. To do his, we will p o e ha CSP ( B )is de inable in ∀-MUD [ ω ], assuming ha B is o he o m ( B, RB ), i.e., B has only one ela ion. This su ices, since as men ioned in Subsec ion 2.1, e e y cons ain sa is ac ion p oblem CSP ( B ) is equi alen , ia polynomial- ime educ ions, o a CSP ( B0 )in which B0 is a s uc u e wi h a single bina y ela ion. We s a by obse ing ha he u h o a [ k ]- alued uni o m dependence a om on a gi en s uc u e Aand a gi en eam Timplies he exis ence o a homomo phism be ween he wo s uc u es (A, RT,x x x)and ([k], RT,α α α). ILemma 7. I A, T |= udep[k](x x x;α α α), hen (A, RT,x x x)∈CSP([k], RT,α α α). P oo . Assume ha A, T |= udep[k](x x x;α α α). Then he e is a unc ion :A→[k]such ha (s(xi)) = s(αi) o all i∈[n]and s∈T. This condi ion implies ha is a homomo phism om ( A, RT,x x x ) o ([ k ] , RT,α α α ). Indeed, i a a a = ( a1, . . . , an ) ∈RT,x x x , hen he e exis s s∈T such ha s ( xi ) = ai o all i∈ [ n ]. Bu hen also s(αi) = (ai)holds o all i∈[n], whence ( (a1), . . . , (an)) ∈RT,α α α.J No e ha he con e se implica ion o Lemma 7 is no ue. As an example, conside he eam T = {s, s0} , whe e s ( x1 ) = s0 ( x1 ), s ( x2 ) = s0 ( x2 ), s ( α1 ) = s ( α2 ) = 1 and s0 ( α1 ) = s0 ( α2 )=2. Then he unc ion h : A→ [ k ]such ha h ( a ) = 1 o all a∈A , is a homomo phism ( A, RT,x1x2 ) → ([ k ] , RT,α1α2 ), bu clea ly A, T 6| = udep [ k ]( x1, x2 ; α1, α2 ). Thus, uni o m dependence a oms a e di e en om homomo phism a oms. CSL 2016 14:16 Dependence Logic s. Cons ain Sa is ac ion 5 Concluding Rema ks In his pape , we es ablished a igh connec ion be ween dependence logic and cons ain sa is ac ion. Since dependence logic has he same exp essi e powe as exis en ial second-o de logic, i is expec ed ha cons ain sa is ac ion p oblems can be exp essed in dependence logic. We belie e, howe e , ha he connec ion es ablished in his pape is a p io i unexpec ed, since we showed ha a simple agmen o uni e sal dependence logic cap u es, in a p ecise sense, he amily o cons ain sa is ac ion p oblems CSP ( B ), whe e B is a ela ional s uc u e. Ou esul s con ibu e o he desc ip i e complexi y o cons ain sa is ac ion and also shed new ligh on quan i ie - ee and uni e sal dependence logic. The connec ion be ween uni e sal dependence logic and cons ain sa is ac ion is es- ablished by using MMSNP as a b idge and also he esul by Fede and Va di [ 5 ] ha MMSNP cap u es cons ain sa is ac ion ia polynomial- ime educ ions. Speci ically, we showed ha e e y cons ain sa is ac ion p oblem CSP ( B ), in which B has only one ela ion, is de inable by a ∀-MUD [ ω ]-sen ence, and e e y ∀-MUD [ ω ]-sen ence is equi alen o some MMSNP -sen ence. A na u al ques ion ha a ises om hese esul s is whe he e e y MMSNP - sen ence is equi alen o some ∀-MUD [ ω ]-sen ence o , in o he wo ds, whe he MMSNP and ∀-MUD [ ω ]ha e he same exp essi e powe . A ela ed ques ion is o iden i y o he na u al agmen s o dependence logic ha cap u e impo an agmen s o exis en ial second-o de logic, such as s ic exis en ial second-o de logic (i.e., he agmen o exis en ial second-o de logic in which all i s -o de quan i ie s a e uni e sal). Acknowledgemen s. A pa o he esea ch epo ed he e was ca ied ou while Lau i Hella was isi ing he Uni e si y o Cali o nia San a C uz. Re e ences 1Nadia C eignou, Phokion G. Kolai is, and He ibe Vollme , edi o s. Complexi y o Con- s ain s – An O e iew o Cu en Resea ch Themes [Resul o a Dags uhl Semina ], olume 5250 o Lec u e No es in Compu e Science. Sp inge , 2008. 2A naud Du and, Juha Kon inen, Nicolas de Rugy-Al he e, and Jouko Väänänen. T ac - abili y on ie o da a complexi y in eam seman ics. In P oceedings Six h In e na ional Symposium on Games, Au oma a, Logics and Fo mal Ve i ica ion, GandALF 2015, Genoa, I aly, 21-22nd Sep embe 2015., pages 73–85, 2015. 3Paul E dös. G aph heo y and p obabili y. Canadian J. o Ma hema ics, 11:34–38, 1959. 4Ronald Fagin. Gene alized i s -o de spec a and polynomial- ime ecognizable se s. In Richa d Ka p, edi o , Complexi y o Compu a ion, numbe 7 in SIAM-AMS P oceedings, pages 43–73. SIAM-AMS, 1974. 5Tomás Fede and Moshe Y. Va di. The compu a ional s uc u e o mono one monadic SNP and cons ain sa is ac ion: A s udy h ough da alog and g oup heo y. SIAM J. Compu ., 28(1):57–104, 1998. 6P. Galliani. Inclusion and exclusion dependencies in eam seman ics – on some logics o impe ec in o ma ion. Ann. Pu e Appl. Logic, 163(1):68–84, 2012. 7Pie o Galliani and Lau i Hella. Inclusion logic and ixed poin logic. In Compu e Science Logic 2013 (CSL 2013), CSL 2013, Sep embe 2-5, 2013, To ino, I aly, numbe 23 in LIPIcs, pages 281–295. Schloss Dags uhl – Leibniz-Zen um ue In o ma ik, 2013. doi: 10.4230/LIPIcs.CSL.2013.281. 8E ich G ädel and Jouko A. Väänänen. Dependence and independence. S udia Logica, 101(2):399–410, 2013. doi:10.1007/s11225-013-9479-2. L. Hella and Ph. G. Kolai is 14:17 9Johan Hås ad, And ei A. K okhin, and Dániel Ma x. The cons ain sa is ac ion p oblem: Complexi y and app oximabili y (Dags uhl Semina 12451). Dags uhl Repo s, 2(11):1–19, 2012. 10 Leon Henkin. Some ema ks on in ini ely long o mulas. In In ini is ic Me hods. Pe gamon P ess, 1961. 11 Jaakko Hin ikka and Gab iel Sandu. In o ma ional independence as a seman ical phe- nomenon. In J. E. Fens ad e al., edi o , Logic, Me hodology and he Philosophy o Science VIII, pages 571–89. No h-Holland, 1989. 12 Ja mo Kon inen. Cohe ence and compu a ional complexi y o quan i ie - ee dependence logic o mulas. S udia Logica, 101(2):267–291, 2013. doi:10.1007/s11225-013-9481-8. 13 Juha Kon inen and Jouko A. Väänänen. On de inabili y in dependence logic. Jou nal o Lo- gic, Language and In o ma ion, 18(3):317–332, 2009. doi:10.1007/s10849-009-9082-0. 14 Juha Kon inen and Jouko A. Väänänen. Axioma izing i s -o de consequences in depend- ence logic. Ann. Pu e Appl. Logic, 164(11):1101–1117, 2013. doi:10.1016/j.apal.2013. 05.006. 15 Gábo Kun and Ja osla Nese il. Fo bidden li s (NP and CSP o combina o ialis s). Eu . J. Comb., 29(4):930–945, 2008. 16 Richa d E. Ladne . On he s uc u e o polynomial ime educibili y. J. ACM, 22(1):155– 171, 1975. 17 Jouko A. Väänänen. Dependence Logic – A New App oach o Independence F iendly Logic, olume 70 o London Ma hema ical Socie y s uden ex s. Camb idge Uni e si y P ess, 2007. URL: h p://www.camb idge.o g/de/knowledge/isbn/i em1164246/. CSL 2016