A fine-grained hierarchy of hard problems in the separated fragment
A fine-grained hierarchy of hard problems in the separated fragment
复制标题
分离片段中困难问题的细粒度层次结构
DOI：
10.1109/lics.2017.8005094
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Marco Voigt
中科院分区：
文献类型：
--
作者：
Marco Voigt
近年来，分离片段（SF）被引入并被证明是可判定的。它的定义原理是普遍的和存在的量化变量可能不会同时出现在原子中。决定SF的可满足性问题所需时间的已知上界是用量词变换来表述的：给定一个SF句子∃z /∀x /∀<inf>1</inf>∃y /∃<inf>1</inf>…∀x /∃<inf>n</inf>∃y /∃<inf>n</inf>。其中ψ与量词无关，可满足性可以在非确定性的n倍指数时间内确定。在本文中，我们对sf可满足性的复杂性进行了更细粒度的分析。我们根据存在变量的相互作用的∂度（简称：度）推导出一个上界和下界——一个衡量句子中有多少个独立的存在量词块通过原子中变量的联合出现而连接起来的新度量。我们的主要结果是所有具有k或更小度的SF句子的集合SF<inf>∂≤k</inf>的可满足问题的k- nexptime -完备性。因此，我们证明了SF可满足性一般是非初等的，因为SF的定义不受程度的限制。除了平凡的下界之外，到目前为止，我们对sf可满足性的硬度一无所知。
Recently, the separated fragment (SF) has been introduced and proved to be decidable. Its defining principle is that universally and existentially quantified variables may not occur together in atoms. The known upper bound on the time required to decide SF's satisfiability problem is formulated in terms of quantifier alternations: Given an SF sentence ∃z⃗∀x⃗<inf>1</inf>∃y⃗<inf>1</inf>…∀x⃗<inf>n</inf>∃y⃗<inf>n</inf>.ψ in which ψ is quantifier free, satisfiability can be decided in non-deterministic n-fold exponential time. In the present paper, we conduct a more fine-grained analysis of the complexity of SF-satisfiability. We derive an upper and a lower bound in terms of the degree ∂ of interaction of existential variables (short: degree)—a novel measure of how many separate existential quantifier blocks in a sentence are connected via joint occurrences of variables in atoms. Our main result is the k-NEXPTIME-completeness of the satisfiability problem for the set SF<inf>∂≤k</inf> of all SF sentences that have degree k or smaller. Consequently, we show that SF-satisfiability is non-elementary in general, since SF is defined without restrictions on the degree. Beyond trivial lower bounds, nothing has been known about the hardness of SF-satisfiability so far.
蒯因的凹槽片段是非初级的
DOI：
--
发表时间：
2016
期刊：
--
影响因子：
--
作者：
Pratt-Hartmann I
通讯作者：
Pratt-Hartmann I