TY - JOUR

T1 - Parameterised complexity of model checking and satisfiability in propositional dependence logic

AU - Mahmood, Yasir

AU - Meier, Arne

N1 - Funding Information: The authors thank the anonymous referees for their comments in improving the paper. We thank Phokion Kolaitis, Juha Kontinen, and Sebastian Link for discussions on m-SAT. We are grateful to Jonni Virtema for his thoughts on the splits parameter in the database setting. This work was supported by the German Research Foundation (DFG), project ME 4279/1-2. The authors would like to thank the participants and organisers of the Dagstuhl Seminar 19031 “Logics for Dependence and Independence” [] for valuable comments and suggestions after the presentation of partial results of this article.

PY - 2022/3

Y1 - 2022/3

N2 - Dependence Logic was introduced by Jouko Väänänen in 2007. We study a propositional variant of this logic (PDL) and investigate a variety of parameterisations with respect to central decision problems. The model checking problem (MC) of PDL is NP-complete (Ebbing and Lohmann, SOFSEM 2012). The subject of this research is to identify a list of parameterisations (formula-size, formula-depth, treewidth, team-size, number of variables) under which MC becomes fixed-parameter tractable. Furthermore, we show that the number of disjunctions or the arity of dependence atoms (dep-arity) as a parameter both yield a paraNP-completeness result. Then, we consider the satisfiability problem (SAT) which classically is known to be NP-complete as well (Lohmann and Vollmer, Studia Logica 2013). There we are presenting a different picture: under team-size, or dep-arity SAT is paraNP-complete whereas under all other mentioned parameters the problem is FPT. Finally, we introduce a variant of the satisfiability problem, asking for a team of a given size, and show for this problem an almost complete picture.

AB - Dependence Logic was introduced by Jouko Väänänen in 2007. We study a propositional variant of this logic (PDL) and investigate a variety of parameterisations with respect to central decision problems. The model checking problem (MC) of PDL is NP-complete (Ebbing and Lohmann, SOFSEM 2012). The subject of this research is to identify a list of parameterisations (formula-size, formula-depth, treewidth, team-size, number of variables) under which MC becomes fixed-parameter tractable. Furthermore, we show that the number of disjunctions or the arity of dependence atoms (dep-arity) as a parameter both yield a paraNP-completeness result. Then, we consider the satisfiability problem (SAT) which classically is known to be NP-complete as well (Lohmann and Vollmer, Studia Logica 2013). There we are presenting a different picture: under team-size, or dep-arity SAT is paraNP-complete whereas under all other mentioned parameters the problem is FPT. Finally, we introduce a variant of the satisfiability problem, asking for a team of a given size, and show for this problem an almost complete picture.

KW - Model checking

KW - Parameterised complexity

KW - Propositional dependence logic

KW - Satisfiability

UR - http://www.scopus.com/inward/record.url?scp=85101856182&partnerID=8YFLogxK

U2 - 10.48550/arXiv.1904.06107

DO - 10.48550/arXiv.1904.06107

M3 - Article

AN - SCOPUS:85101856182

VL - 90

SP - 271

EP - 296

JO - Annals of Mathematics and Artificial Intelligence

JF - Annals of Mathematics and Artificial Intelligence

SN - 1012-2443

IS - 2-3

ER -