Meier Arne, Ordyniak Sebastian, Ramanujan M S, Schindler Irena
1Institut für Theoretische Informatik, Leibniz Universität Hannover, Appelstrasse 4, 30167 Hannover, Germany.
2Algorithms Group, University of Sheffield, Regent Court, 211 Portobello, Sheffield, S1 4DP UK.
Algorithmica. 2019;81(2):476-496. doi: 10.1007/s00453-018-0515-5. Epub 2018 Sep 18.
In the present paper, we introduce the backdoor set approach into the field of temporal logic for the global fragment of linear temporal logic. We study the parameterized complexity of the satisfiability problem parameterized by the size of the backdoor. We distinguish between backdoor detection and evaluation of backdoors into the fragments of Horn and Krom formulas. Here we classify the operator fragments of globally-operators for past/future/always, and the combination of them. Detection is shown to be fixed-parameter tractable whereas the complexity of evaluation behaves differently. We show that for Krom formulas the problem is paraNP-complete. For Horn formulas, the complexity is shown to be either fixed parameter tractable or paraNP-complete depending on the considered operator fragment.
在本文中，我们将后门集方法引入到线性时态逻辑全局片段的时态逻辑领域。我们研究以后门大小为参数的可满足性问题的参数化复杂度。我们区分了进入霍恩公式和克朗公式片段的后门检测与评估。这里我们对过去/未来/总是的全局运算符的运算符片段及其组合进行分类。结果表明检测是固定参数可处理的，而评估的复杂度表现不同。我们表明对于克朗公式，该问题是参数化NP完全的。对于霍恩公式，根据所考虑的运算符片段，复杂度要么是固定参数可处理的，要么是参数化NP完全的。
