Details
| Original language | English |
|---|---|
| Pages (from-to) | 271-296 |
| Number of pages | 26 |
| Journal | Annals of Mathematics and Artificial Intelligence |
| Volume | 90 |
| Issue number | 2-3 |
| Early online date | 27 Feb 2021 |
| Publication status | Published - Mar 2022 |
Abstract
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.
Keywords
- Model checking, Parameterised complexity, Propositional dependence logic, Satisfiability
ASJC Scopus subject areas
- Computer Science(all)
- Artificial Intelligence
- Mathematics(all)
- Applied Mathematics
Cite this
- Standard
- Harvard
- Apa
- Vancouver
- BibTeX
- RIS
In: Annals of Mathematics and Artificial Intelligence, Vol. 90, No. 2-3, 03.2022, p. 271-296.
Research output: Contribution to journal › Article › Research › peer review
}
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 -