Parametrised Complexity of Model Checking and Satisfiability in Propositional Dependence Logic

TL;DR

This paper systematically studies the parametrised complexity of model checking and satisfiability in propositional dependence logic, identifying parameters that lead to fixed-parameter tractability and those that result in paraNP-completeness.

Contribution

It provides a comprehensive analysis of various parametrisations affecting the complexity of model checking and satisfiability in propositional dependence logic, including new complexity classifications.

Findings

Model checking is NP-complete but fixed-parameter tractable under certain parameters.

Satisfiability is paraNP-complete under team-size and dep-arity, but FPT under others.

Introduces a variant of satisfiability with teams of fixed size, with a nearly complete complexity classification.

Abstract

In this paper, we initiate a systematic study of the parametrised complexity in the field of Dependence Logics which finds its origin in the Dependence Logic of V\"a\"an\"anen from 2007. We study a propositional variant of this logic (PDL) and investigate a variety of parametrisations with respect to the central decision problems. The model checking problem (MC) of PDL is NP-complete. The subject of this research is to identify a list of parametrisations (formula-size, treewidth, treedepth, 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) showing a different picture: under team-size, or dep-arity SAT is paraNP-complete whereas under all other mentioned parameters the problem is in FPT. Finally, we introduce a variant of the satisfiability problem, asking for teams of a given size, and show for this problem an almost complete picture.