اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدNear-Optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps
110
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We prove near-optimal trade-offs for quantifier depth versus number of variables in first-order logic by exhibiting pairs of $n$-element structures that can be distinguished by a $k$-variable first-order sentence but where every such sentence requires quantifier depth at least $n^{Omega(k/log k)}$. Our trade-offs also apply to first-order counting logic, and by the known connection to the $k$-dimensional Weisfeiler--Leman algorithm imply near-optimal lower bounds on the number of refinement iterations. A key component in our proof is the hardness condensation technique recently introduced by [Razborov 16] in the context of proof complexity. We apply this method to reduce the domain size of relational structures while maintaining the minimal quantifier depth to distinguish them in finite variable logics.
قيم البحث
اقرأ أيضاً
The $k$-dimensional Weisfeiler-Leman algorithm ($k$-WL) is a fruitful approach to the Graph Isomorphism problem. 2-WL corresponds to the original algorithm suggested by Weisfeiler and Leman over 50 years ago. 1-WL is the classical color refinement ro
utine. Indistinguishability by $k$-WL is an equivalence relation on graphs that is of fundamental importance for isomorphism testing, descriptive complexity theory, and graph similarity testing which is also of some relevance in artificial intelligence. Focusing on dimensions $k=1,2$, we investigate subgraph patterns whose counts are $k$-WL invariant, and whose occurrence is $k$-WL invariant. We achieve a complete description of all such patterns for dimension $k=1$ and considerably extend the previous results known for $k=2$.
Given a connected graph $G$ and its vertex $x$, let $U_x(G)$ denote the universal cover of $G$ obtained by unfolding $G$ into a tree starting from $x$. Let $T=T(n)$ be the minimum number such that, for graphs $G$ and $H$ with at most $n$ vertices eac
h, the isomorphism of $U_x(G)$ and $U_y(H)$ surely follows from the isomorphism of these rooted trees truncated at depth $T$. Motivated by applications in theory of distributed computing, Norris [Discrete Appl. Math. 1995] asks if $T(n)le n$. We answer this question in the negative by establishing that $T(n)=(2-o(1))n$. Our solution uses basic tools of finite model theory such as a bisimulation version of the Immerman-Lander 2-pebble counting game. The graphs $G_n$ and $H_n$ we construct to prove the lower bound for $T(n)$ also show some other tight lower bounds. Both having $n$ vertices, $G_n$ and $H_n$ can be distinguished in 2-variable counting logic only with quantifier depth $(1-o(1))n$. It follows that color refinement, the classical procedure used in isomorphism testing and other areas for computing the coarsest equitable partition of a graph, needs $(1-o(1))n$ rounds to achieve color stabilization on each of $G_n$ and $H_n$. Somewhat surprisingly, this number of rounds is not enough for color stabilization on the disjoint union of $G_n$ and $H_n$, where $(2-o(1))n$ rounds are needed.
The $k$-dimensional Weisfeiler-Leman algorithm ($k$-WL) is a very useful combinatorial tool in graph isomorphism testing. We address the applicability of $k$-WL to recognition of graph properties. Let $G$ be an input graph with $n$ vertices. We show
that, if $n$ is prime, then vertex-transitivity of $G$ can be seen in a straightforward way from the output of 2-WL on $G$ and on the vertex-individualized copies of $G$. However, if $n$ is divisible by 16, then $k$-WL is unable to distinguish between vertex-transitive and non-vertex-transitive graphs with $n$ vertices as long as $k=o(sqrt n)$. Similar results are obtained for recognition of arc-transitivity.
Given two structures $G$ and $H$ distinguishable in $fo k$ (first-order logic with $k$ variables), let $A^k(G,H)$ denote the minimum alternation depth of a $fo k$ formula distinguishing $G$ from $H$. Let $A^k(n)$ be the maximum value of $A^k(G,H)$ ov
er $n$-element structures. We prove the strictness of the quantifier alternation hierarchy of $fo 2$ in a strong quantitative form, namely $A^2(n)ge n/8-2$, which is tight up to a constant factor. For each $kge2$, it holds that $A^k(n)>log_{k+1}n-2$ even over colored trees, which is also tight up to a constant factor if $kge3$. For $kge 3$ the last lower bound holds also over uncolored trees, while the alternation hierarchy of $fo 2$ collapses even over all uncolored graphs. We also show examples of colored graphs $G$ and $H$ on $n$ vertices that can be distinguished in $fo 2$ much more succinctly if the alternation number is increased just by one: while in $Sigma_{i}$ it is possible to distinguish $G$ from $H$ with bounded quantifier depth, in $Pi_{i}$ this requires quantifier depth $Omega(n^2)$. The quadratic lower bound is best possible here because, if $G$ and $H$ can be distinguished in $fo k$ with $i$ quantifier alternations, this can be done with quantifier depth $n^{2k-2}$.
Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze quantifier can be part of the language, as in some real-time logics, bu
t this variable-binding mechanism is quite general and ubiquitous in many logical languages (first-order temporal logics, hybrid logics, logics for sequence diagrams, navigation logics, logics with lambda-abstraction etc.). We show that Constraint LTL over the simple domain (N,=) augmented with the freeze quantifier is undecidable which is a surprising result in view of the poor language for constraints (only equality tests). Man
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
