Parameterized Modal Satisfiability

TL;DR

This paper explores the parameterized complexity of modal satisfiability, identifying structural parameters that influence computational difficulty and proposing new parameters that enable more efficient fixed-parameter tractable algorithms.

Contribution

It introduces alternative parameters like diamond dimension, box dimension, and modal width, which lead to more practical FPT algorithms for modal satisfiability.

Findings

Modal satisfiability is FPT when parameterized by propositional variables and modality depth, but with a tower exponential dependence.

New parameters such as diamond dimension, box dimension, and modal width yield FPT algorithms with milder exponential dependence.

The study advances understanding of structural parameters affecting modal logic satisfiability complexity.

Abstract

We investigate the parameterized computational complexity of the satisfiability problem for modal logic and attempt to pinpoint relevant structural parameters which cause the problem's combinatorial explosion, beyond the number of propositional variables v. To this end we study the modality depth, a natural measure which has appeared in the literature, and show that, even though modal satisfiability parameterized by v and the modality depth is FPT, the running time's dependence on the parameters is a tower of exponentials (unless P=NP). To overcome this limitation we propose several possible alternative parameters, namely diamond dimension, box dimension and modal width. We show fixed-parameter tractability results using these measures where the exponential dependence on the parameters is much milder than in the case of modality depth thus leading to FPT algorithms for modal satisfiability with much more reasonable running times.