Upper Bounds on the Quantifier Depth for Graph Differentiation in First Order Logic

DOI10.1145/2933575.2933595zbMATH Open1394.68162arXiv1605.03480OpenAlexW2964195552WikidataQ130849078 ScholiaQ130849078MaRDI QIDQ4635884FDOQ4635884

Authors: Sandra Kiefer, P. Schweitzer 

Publication date: 23 April 2018

Published in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Abstract: We show that on graphs with n vertices, the 2-dimensional Weisfeiler-Leman algorithm requires at most O(n^2/log(n)) iterations to reach stabilization. This in particular shows that the previously best, trivial upper bound of O(n^2) is asymptotically not tight. In the logic setting, this translates to the statement that if two graphs of size n can be distinguished by a formula in first-order logic with counting with 3 variables (i.e., in C3), then they can also be distinguished by a C3-formula that has quantifier depth at most O(n^2/log(n)). To prove the result we define a game between two players that enables us to decouple the causal dependencies between the processes happening simultaneously over several iterations of the algorithm. This allows us to treat large color classes and small color classes separately. As part of our proof we show that for graphs with bounded color class size, the number of iterations until stabilization is at most linear in the number of vertices. This also yields a corresponding statement in first-order logic with counting. Similar results can be obtained for the respective logic without counting quantifiers, i.e., for the logic L3.

Full work available at URL: https://arxiv.org/abs/1605.03480

Recommendations

• Upper Bounds on the Quantifier Depth for Graph Differentiation in First Order Logic
• The first order definability of graphs: Upper bounds for quantifier depth
• Bounds for the quantifier depth in finite-variable logics: alternation hierarchy
• Bounds for the quantifier depth in finite-variable logics: alternation hierarchy
• The limits of decidability for first order logic on CPDA graphs
• On the parameterized complexity of graph modification to first-order logic properties
• Expressiveness and complexity of graph logic
• Expressivity and succinctness of order-invariant logics on depth-bounded structures
• The quantifier complexity of polynomial-size iterated definitions in first-order logic
• On the Expressive Power of Graph Logic

zbMATH Keywords

first-order logiccounting quantifiersquantifier depthWeisfeiler-Leman algorithmcolor refinement

Mathematics Subject Classification ID

Graph algorithms (graph-theoretic aspects) (05C85) Model theory of finite structures (03C13) Logic with extra quantifiers and operators (03C80) Descriptive complexity and finite models (68Q19)

Cites Work

• Practical graph isomorphism. II.
• Weisfeiler-Lehman graph kernels
• Fixed-point definability and polynomial time on graphs with excluded minors
• Random Graph Isomorphism
• An optimal lower bound on the number of variables for graph identification
• Title not available (Why is that?)
• Title not available (Why is that?)
• Tight Lower and Upper Bounds for the Complexity of Canonical Colour Refinement
• Dimension reduction via colour refinement
• Graph isomorphism in quasipolynomial time (extended abstract)
• Title not available (Why is that?)
• From Invariants to Canonization in Parallel
• Logical complexity of graphs: a survey
• Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler--Leman Refinement Steps
• Conflict propagation and component recursion for canonical labeling
• Graphs identified by logics with counting
• Universal covers, color refinement, and two-variable counting logic: lower bounds for the depth

Cited In (9)

• Title not available (Why is that?)
• Number of variables for graph differentiation and the resolution of GI formulas
• The limits of decidability for first order logic on CPDA graphs
• Title not available (Why is that?)
• Upper Bounds on the Quantifier Depth for Graph Differentiation in First Order Logic
• Universal covers, color refinement, and two-variable counting logic: lower bounds for the depth
• Walk refinement, walk logic, and the iteration number of the Weisfeiler-Leman algorithm
• Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler--Leman Refinement Steps
• Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism Formulas

Uses Software

• nauty
• Traces
• bliss

This page was built for publication: Upper Bounds on the Quantifier Depth for Graph Differentiation in First Order Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635884)