Parameterised complexity of model checking and satisfiability in propositional dependence logic

<jats:title>Abstract</jats:title><jats:p>Dependence Logic was introduced by Jouko Väänänen in 2007. We study a propositional variant of this logic<jats:italic>(PDL)</jats:italic>and investigate a variety of parameterisations with respect to central decision problems. The model checking problem (MC) of<jats:italic>PDL</jats:italic>is<jats:bold>NP</jats:bold>-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<jats:bold>NP</jats:bold>-complete as well (Lohmann and Vollmer, Studia Logica 2013). There we are presenting a different picture: under team-size, or dep-arity SAT is<jats:bold>paraNP</jats:bold>-complete whereas under all other mentioned parameters the problem is<jats:bold>FPT</jats:bold>. 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.</jats:p>