A Generalized Quantifier Concept in Computational Complexity Theory
Heribert Vollmer
探讨了计算复杂性理论中广义量词的概念，并将其用于统一处理叶语言的可定义性、预言机分离、2型算子和带单值门的电路.关系Lindstroem量词指出。
A notion of generalized quantifier in computational complexity theory is explored and used to give a unified treatment of leaf language definability, oracle separations, type 2 operators, and circuits with monoidal gates. Relations to Lindstroem quantifiers are pointed out.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
On the Number of Quantifiers as a Complexity Measure
在1981年，尼尔·伊莫曼描述了一个两人博弈，他称之为“可分离性博弈”（separability game）\cite{Immerman81}，这个博弈捕获了描述一个一阶逻辑中的属性所需的量词的数量。Immerman的论文为研究一阶逻辑中表达属性所需的量词数量奠定了基础，但这个博弈似乎太复杂而无法研究，论文的论点几乎只使用量词秩作为量词总数的下限。然而，去年Fagin，Lenchner，Regan和Vyas重新发现了这些游戏，提供了一些分析它们的工具，并展示了如何利用它们来表征表达不同大小的线性顺序所需的量词数量。本文通过建立几个新的结果，推进了量词个数作为真实复杂性测度的研究。首先，我们仔细区分最小数量的量词从更常见的描述性复杂性措施，最小量词秩和最小数量的变量。然后，对于每一个正整数$k$，我们给出了一个明确的例子，有限结构的属性（特别是有限图），可以用一个句子的量词秩$k$表示，但相同的属性需要$2^{Ω(k^2)}$量词来表示。
Constraint Satisfaction with Counting Quantifiers
我们开始研究存在计数量词的约束满足问题（CSP），它可以被看作是量化CSP（QCSP）模型中CSP的变体。我们证明了严格在exists^1：=exists和exists^n：=forall之间的单个计数量词（域的大小为n）已经提供了QCSP（既有exists又有forall）的最大可能复杂度，对于适当选择的模板是P空间完全的。接下来，我们重点讨论团和循环模板上计数量词子集的复杂性。对于循环，我们给出了一个完整的可分性--所有这样的问题都是在L，NP-完全或P空间-完全的。对于集团，我们接近于一个类似的分裂，但有一个案例仍然悬而未决。然后，我们考虑CSP的推广，其中我们用量词exists^j（j not 1）扩充现存量词exists ^1：=exists。这样的CSP在非二分图模板上已经是NP困难的。我们探讨的情况下，这种广义CSP的二分模板，给各种条件的易处理性和硬度-最终在一般图形的分类定理。最后，我们使用计数量词来解决一个具体的QCSP的复杂性，其复杂性是以前开放的。
The descriptive complexity approach to LOGCFL
基于已知的广义量词为基础的一阶表征LOGCFL的基础上，我们奠定了基础，更深入的调查。具体来说，我们研究LOGCFL的子类所产生的不同arity和嵌套的groupoidal量词。我们的工作扩展到NC 1及其子类的monoidal量词的详细理论。在没有BIT谓词的情况下，我们解决了主要问题：我们特别表明，没有一个最外面的一元群形量词与FO可以捕获所有的上下文无关的语言，我们得到了令人惊讶的结果，一个变种格雷巴赫的“最硬的上下文无关的语言”是LOGCFL-完全下量词免费的BIT免费的投影。然后，我们证明了FO与一元群体量词是严格更有表现力的BIT谓词比没有。考虑一个特殊的群体量词，我们证明了一阶逻辑与大多数对严格更有表现力比一阶与大多数个人。作为一个独立的兴趣的技术工具，我们定义了一个非周期性非确定性有限自动机的概念，并证明了FO翻译正是由单值非周期性非确定性有限换能器计算的映射。
Complexity of the Guarded Two-Variable Fragment with Counting Quantifiers
该研究证明带计数量词的受护两变量片段的有限可满足性问题属于EXPTIME复杂度类，所用方法还为Kazakov近期提出的该片段可满足性问题属EXPTIME的结论给出了简单证明。
Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic
从计算复杂性的角度研究了分支时间逻辑CTL的可满足性问题。严格的上限和下限提供了每个时间操作符片段。在平行，最小模型的大小进行了研究，一个合适的概念极小。第三，研究了平坦的CTL，即，时态运算符嵌套深度非常低的公式。在复杂性和最小模型方面显示出尖锐的二分法：时间深度1具有低表达能力，而时间深度2相当于完整的CTL。
Data-Complexity of the Two-Variable Fragment with Counting Quantifiers
本文确定了带计数量词的两变量片段及其守护片段在数据复杂度上的精确界限，分别达到NP完全和co-NP完全。
An Improved Homomorphism Preservation Theorem From Lower Bounds in Circuit Complexity
作者[39]以前的工作表明，经典模型论的同态保持定理在其陈述仅限于有限结构时仍然有效。在本文中，我们给出了一个新的证明，通过减少电路复杂性的下界，特别是在AC $^0$公式大小的着色子图同构问题。在形式上，我们证明了：如果一个一阶句子$Φ$的量词秩$k$在有限结构上的同态下保持不变，那么它在有限结构上等价于一个存在肯定句子$Ψ$的量词秩$k^{O(1)}$ .量化，这改进了[39]的结果，其中$Ψ$的量化器秩的上限是$k$的非初等函数。
On the freeze quantifier in Constraint LTL: decidability and complexity
约束LTL是LTL在Presburger约束上的推广，通常被用作一种形式语言来描述具有约束的操作模型的行为。冻结量词可以是语言的一部分，如在一些实时逻辑中，但这种变量绑定机制在许多逻辑语言中（一阶时态逻辑，混合逻辑，序列图逻辑，导航逻辑，具有抽象的逻辑等）是相当普遍和普遍的。我们表明，约束LTL在简单的域（N，=）增加了冻结量词是不可判定的，这是一个令人惊讶的结果，鉴于穷人的语言约束（只有平等测试）。许多版本的无冻结约束LTL在具有定性谓词的域上是可判定的，我们的不可判定性结果实际上建立了Sigma_1^1-完备性。在积极的一面，我们提供的复杂性结果时，域是有限的（EXPSPACE-完备性）或当公式是平坦的，在某种意义上介绍的文件。我们的不可判定性的结果是尖锐的（即限制变量的数量），我们所有的复杂性特征确保完整性方面的一些复杂性类（主要是PSPACE和EXPSPACE）。
Existential Second-Order Logic Over Graphs: Parameterized Complexity
本文研究图上 ESO 公式按一阶量词序列分类的参数化复杂度，以二阶量化集合大小为参数，完整刻画各序列的复杂度高低及可处理性分界。
The Descriptive Complexity of Subgraph Isomorphism without Numerics
令$F$是一个具有$\ell$顶点的连通图。同构于$F$的子图的存在性可以在量词深度不比$\ell$好的一阶逻辑中定义，这仅仅是因为没有更小量词深度的一阶公式可以区分完全图$K_\ell$和$K_{\ell-1}$。证明了对某些$F$，\emph{sufficiently large}连通图中$F$子图的存在性是可用量词深度$\ell-3$定义的.另一方面，如果量词深度优于$\ell/2$，这是不可能的。然而，如果我们考虑具有足够大树宽的连通图上的定义，则对于某些$F$，量词深度可以与$\ell$相比任意小，但永远不会小于$F$的树宽。此外，高连通图上的定义要求量词深度严格大于$F$的密度。最后，我们确定了这些描述复杂性参数的确切值为所有连接模式图$F$的4个顶点。
On the Descriptive Complexity of Vertex Deletion Problems
本文基于一阶逻辑公式的单个量词模式将顶点删除问题的复杂性从二分法细化为三分法，揭示了新的可处理片段及不同图类型下的可处理边界差异。
Generalized Complexity of ALC Subsumption
描述逻辑ALC中关于术语的包含问题是EXPTIME完全的。我们调查的计算复杂性的片段，这个问题的允许布尔运算符。在这里，我们利用克隆的概念在波斯特格的上下文中。此外，我们认为所有四个可能的量词组合的克隆参数化的每个片段。我们将看到，根据可用的量词，分类将是三分的或四分的。
Quantifier Elimination Meets Treewidth
本文提出利用树宽参数的动态规划框架，通过量化消除过程中的结构稀疏性，将FME和CAD的复杂度从双指数降低到单指数。
Parametric Presburger Arithmetic: Complexity of Counting and Quantifier Elimination
我们考虑一个扩展的Presburger算法，它允许乘以$k$参数$t_1,\ldots,t_k$。该语言中的公式定义了参数集$S_\mathbf{t} \subseteq \mathbb{Z}^{d}$，因为$\mathbf{t}$在$\mathbb{Z}^k$中变化，并且我们将计数函数$|S_\mathbf{t}|$作为$\mathbf{t}$的函数进行检查。对于单个参数，已知$|S_t|$可以表示为最终的准多项式（存在周期$m$，使得对于足够大的$t$，函数在每个剩余类mod $m$上是多项式）。我们表明，这样一个很好的表达式是不可能有2个或更多的参数。实际上（假设\textbf{P} $\neq$ \textbf{NP}），我们构造参数集$S_{t_1,t_2}$，使得$|S_{t_1, t_2}|$甚至不能在输入$(t_1,t_2)$上多项式时间计算。与此相反，参数集$S_\mathbf{t} \subseteq \mathbb{Z}^d$任意多个参数，定义在一个类似的语言没有顺序关系，我们表明，$|S_\mathbf{t}|$总是多项式时间计算的大小$\mathbf{t}$，事实上可以表示使用的gcd和类似的功能。
The Complexity of Weighted Counting for Acyclic Conjunctive Queries
本文研究非循环合取查询解的加权计数问题（$\ACQ$）。这个问题的未加权量词自由版本已知是易于处理的（对于组合复杂性），但也知道即使引入单个量化变量也会使其成为$\sP$ -困难。我们首先表明，量化器免费$\ACQ$的加权计数仍然是易处理的，即使是最低限度的扩展问题导致硬的情况下。然后，我们引入了一个新的参数量化查询，允许隔离大岛屿的易处理性。我们表明，从参数化的复杂性的标准假设，这个参数充分表征计数加权解决方案的$\ACQ$查询听话的子类。因此，我们完全确定了$\ACQ$加权计数的易处理边界。
Logical complexity of graphs: a survey
本文讨论了一阶逻辑中有限图的可定义性，它具有两个表示顶点邻接和相等的关系符号。图$G$的逻辑深度$D(G)$等于定义$G$直到同构的句子的最小量词深度。逻辑宽度$W(G)$是在这样的句子中出现的变量的最小数目。逻辑长度$L(G)$是最短定义语句的长度。我们调查已知的估计，这些图的参数，并讨论他们的关系到其他主题（如效率的Weisfeiler-Lehman算法在同构测试，随机图的演变，定量特征的零一律，或贡献的弗兰克拉姆齐的研究希尔伯特的Entscheidungsproblem）。此外，我们跟踪一个图的描述性复杂性的行为，因为逻辑变得更加严格（例如，只允许定义有限数量的变量或量词交替）或更可表达（后与计数量词供电）。
Proof Complexity of Symbolic QBF Reasoning
我们介绍和调查量化布尔公式（QBF）的符号证明系统的有序二元决策图（OBDDs）。这些系统捕获执行符号量词消去的QBF求解器，并因此承认有界路径宽度和量词复杂性的公式的简短证明。因此，我们从标准子句证明系统中获得指数分离，特别是（长距离）QU-Resolution和IR-Calc。我们进一步开发了一个下界技术的符号QBF证明系统的基础上，从通信复杂性的战略提取，升降机已知的下界。这使我们能够推导出强大的下界对符号QBF证明系统是独立的变量排序的基础OBDDs，并举行，即使证明系统被允许访问一个NP-预言。
The computational complexity of integer programming with alternations
证明了具有三个量词交替的整数规划是$NP$ -完全的，即使变量个数固定。这补充了Lenstra和Kannan的早期结果，他们一起说，对于固定数量的变量，最多有两个量词交替的整数规划可以在多项式时间内完成。作为证明的副产品，我们表明，对于两个多面体$P,Q \subset \mathbb{R}^4$，计数的整数点在$Q \backslash P$的投影是$\#P$ -完全的。这与Barvinok和Woods在2003年的结果形成对比，后者允许在多项式时间内分别计算$P$和$Q$中整数点的投影。
Short Presburger arithmetic is hard
研究了Presburger算法（Short-PA）中短句的计算复杂性。这里的“短”是指具有有限数量的变量、量词、不等式和布尔运算的句子;输入仅由线性不等式中涉及的整数系数组成。证明了当第一个量词为$\exists$或$\forall$时，含有$m+2$交替量词的短PA句的可满足性分别是$Σ_{P}^m$ -完全或$Π_{P}^m$ -完全的.对计数版本和受限系统也进行了分析。进一步应用于随机优化中两个自然问题的困难性。
Unprovability of Strong Complexity Lower Bounds in Bounded Arithmetic
本文利用博弈论见证结果与Krajíček技术的扩展，证明了有界算术理论（如APC1和TPV^i）无法证明分离多项式层级更高层的强复杂度下界。
2-ASP(Q) programs with weak constraints: Complexity and efficient implementation
本文研究了带有两个量词和弱约束的ASP(Q)程序（2-ASP(Q)^w）的复杂性，并提出基于CEGAR技术的Casper系统实现策略，实验证明其有效性。
Effective dimension in some general metric spaces
我们引入了有效维数的概念，广泛的一类度量空间，不需要有一个可计算的措施。有效维数是由Lutz在（Lutz 2003）中定义的，用于Cantor空间，并且也被扩展到欧氏空间。Lutz有效化使用了gale和supergale的概念，我们将Hausdorff维数扩展到其他度量空间也是基于维数的supergale特征，这在实践中避免了基于Hausdorff测度的经典维数定义中存在的额外量词，因此允许小时间范围的有效化。本文提出了构造维数的概念及其在Kolmogorov复杂性方面的特征，并将Kolmogorov复杂性的概念推广到任何度量空间，定义了一个点在一定精度下的Kolmogorov复杂性。指出了进一步的研究方向。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。