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