分离片段中难解问题的细粒度层次

近来，分离片段(SF)被提出并被证明是可判定的。其定义原则是全称量化变量和存在量化变量不能在原子中同时出现。已知的判定SF可满足性问题所需时间的上界是用量词交替来表述的：给定一个SF句子 $\exists \vec{z} \forall \vec{x}_1 \exists \vec{y}_1 \ldots \forall \vec{x}_n \exists \vec{y}_n . \psi$，其中 $\psi$ 是无量词的，其可满足性可在非确定性 $n$ 重指数时间内判定。本文中，我们对SF可满足性的复杂度进行了更细粒度的分析。我们根据存在变量的交互度(简称度)导出了上界和下界——这是一种新的度量，衡量一个句子中通过变量在原子中的共同出现而连接的独立存在量词块的数量。我们的主要结果是：对于所有度不大于 $k$ 的SF句子集合 $SF_{\leq k}$，其可满足性问题是 $k$-NEXPTIME-完全的。由此，我们表明SF可满足性一般而言是非初等的，因为SF的定义未对度施加限制。除了平凡下界外，迄今为止关于SF可满足性的困难性一无所知。