[go: up one dir, main page]
More Web Proxy on the site http://driver.im/

Twin-Width and Types

Authors Jakub Gajarský , Michał Pilipczuk , Wojciech Przybyszewski , Szymon Toruńczyk



PDF
Thumbnail PDF

File

LIPIcs.ICALP.2022.123.pdf
  • Filesize: 1.05 MB
  • 21 pages

Document Identifiers

Author Details

Jakub Gajarský
  • University of Warsaw, Poland
Michał Pilipczuk
  • University of Warsaw, Poland
Wojciech Przybyszewski
  • University of Warsaw, Poland
Szymon Toruńczyk
  • University of Warsaw, Poland

Acknowledgements

The authors thank Rose McCarty and Felix Reidl for many initial discussions on the type approach to first-order logic on graphs of bounded twin-width.

Cite As Get BibTex

Jakub Gajarský, Michał Pilipczuk, Wojciech Przybyszewski, and Szymon Toruńczyk. Twin-Width and Types. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 123:1-123:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.ICALP.2022.123

Abstract

We study problems connected to first-order logic in graphs of bounded twin-width. Inspired by the approach of Bonnet et al. [FOCS 2020], we introduce a robust methodology of local types and describe their behavior in contraction sequences - the decomposition notion underlying twin-width. We showcase the applicability of the methodology by proving the following two algorithmic results. In both statements, we fix a first-order formula φ(x_1,…,x_k) and a constant d, and we assume that on input we are given a graph G together with a contraction sequence of width at most d.  
- One can in time 𝒪(n) construct a data structure that can answer the following queries in time 𝒪(log log n): given w_1,…,w_k, decide whether φ(w_1,…,w_k) holds in G. 
- After 𝒪(n)-time preprocessing, one can enumerate all tuples w₁,…,w_k that satisfy φ(x_1,…,x_k) in G with 𝒪(1) delay.  In the first case, the query time can be reduced to 𝒪(1/ε) at the expense of increasing the construction time to 𝒪(n^{1+ε}), for any fixed ε > 0. Finally, we also apply our tools to prove the following statement, which shows optimal bounds on the VC density of set systems that are first-order definable in graphs of bounded twin-width.  
- Let G be a graph of twin-width d, A be a subset of vertices of G, and φ(x_1,…,x_k,y_1,…,y_l) be a first-order formula. Then the number of different subsets of A^k definable by φ using l-tuples of vertices from G as parameters, is bounded by O(|A|^l).

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
Keywords
  • twin-width
  • FO logic
  • model checking
  • query answering
  • enumeration

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Matthias Aschenbrenner, Alf Dolich, Deirdre Haskell, Dugald Macpherson, and Sergei Starchenko. Vapnik-chervonenkis density in some theories without the independence property, i. Transactions of the American Mathematical Society, 368, September 2011. Google Scholar
  2. Guillaume Bagan. MSO queries on tree decomposable structures are computable with linear delay. In Proceedings of the 15th Annual Conference on Computer Science Logic, CSL 2006, volume 4207 of Lecture Notes in Computer Science, pages 167-181. Springer, 2006. URL: https://doi.org/10.1007/11874683_11.
  3. J. T. Baldwin and S. Shelah. Second-order quantifiers and the complexity of theories. Notre Dame Journal of Formal Logic, 26(3):229-303, 1985. Google Scholar
  4. Édouard Bonnet, Ugo Giocanti, Patrice Ossona de Mendez, Pierre Simon, Stéphan Thomassé, and Szymon Toruńczyk. Twin-width IV: ordered graphs and matrices. CoRR, abs/2102.03117, 2021. Accepted to STOC 2022. URL: http://arxiv.org/abs/2102.03117.
  5. Édouard Bonnet, Eun Jung Kim, Amadeus Reinald, and Stéphan Thomassé. Twin-width VI: the lens of contraction sequences. CoRR, abs/2111.00282, 2021. To appear in the proceedings of SODA 2022. URL: http://arxiv.org/abs/2111.00282.
  6. Édouard Bonnet, Eun Jung Kim, Amadeus Reinald, Stéphan Thomassé, and Rémi Watrigant. Twin-width and polynomial kernels. In Procedings of the 16th International Symposium on Parameterized and Exact Computation, IPEC 2021, volume 214 of LIPIcs, pages 10:1-10:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.IPEC.2021.10.
  7. Édouard Bonnet, Eun Jung Kim, Stéphan Thomasse, and Rémi Watrigant. Twin-width I: tractable FO model checking. In Proceedings of the IEEE 61st Annual Symposium on Foundations of Computer Science, FOCS 2020, pages 601-612. IEEE Computer Society, 2020. Google Scholar
  8. Édouard Bonnet, Jaroslav Nešetřil, Patrice Ossona de Mendez, Sebastian Siebertz, and Stéphan Thomassé. Twin-width and permutations. CoRR, abs/2102.06880, 2021. URL: http://arxiv.org/abs/2102.06880.
  9. Timothy M. Chan. Persistent predecessor search and orthogonal point location on the word RAM. In Proceedings of the Twenty-Second Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2011, pages 1131-1145. SIAM, 2011. Google Scholar
  10. Thomas Colcombet. A combinatorial theorem for trees. In ICALP 2007, volume 4596 of Lecture Notes in Computer Science, pages 901-912. Springer, 2007. Google Scholar
  11. Zdenek Dvorák, Daniel Král, and Robin Thomas. Testing first-order properties for subclasses of sparse graphs. J. ACM, 60(5):36:1-36:24, 2013. Google Scholar
  12. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite model theory. Perspectives in Mathematical Logic. Springer, 1995. Google Scholar
  13. Jakub Gajarský, Michał Pilipczuk, and Szymon Toruńczyk. Stable graphs of bounded twin-width. CoRR, abs/2107.03711, 2021. URL: http://arxiv.org/abs/2107.03711.
  14. Wojciech Kazana and Luc Segoufin. Enumeration of monadic second-order queries on trees. ACM Trans. Comput. Log., 14(4):25:1-25:12, 2013. URL: https://doi.org/10.1145/2528928.
  15. Wojciech Kazana and Luc Segoufin. First-order queries on classes of structures with bounded expansion. Log. Methods Comput. Sci., 16(1), 2020. URL: https://doi.org/10.23638/LMCS-16(1:25)2020.
  16. Adam Paszke and Michał Pilipczuk. VC density of set systems definable in tree-like graphs. In Proceedings of the 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020, volume 170 of LIPIcs, pages 78:1-78:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.MFCS.2020.78.
  17. Michał Pilipczuk, Nicole Schirrmacher, Sebastian Siebertz, Szymon Toruńczyk, and Alexandre Vigny. Algorithms and data structures for first-order logic with connectivity under vertex failures. CoRR, abs/2111.03725, 2021. URL: http://arxiv.org/abs/2111.03725.
  18. Michał Pilipczuk, Sebastian Siebertz, and Szymon Toruńczyk. On the number of types in sparse graphs. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, pages 799-808. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209178.
  19. Michał Pilipczuk, Marek Sokołowski, and Anna Zych-Pawlewicz. Compact representation for matrices of bounded twin-width. CoRR, abs/2110.08106, 2021. URL: http://arxiv.org/abs/2110.08106.
  20. Wojciech Przybyszewski. VC-density and abstract cell decomposition for edge relation in graphs of bounded twin-width. CoRR, abs/2202.04006, 2022. URL: http://arxiv.org/abs/2202.04006.
  21. Norbert Sauer. On the density of families of sets. Journal of Combinatorial Theory, Series A, 13(1):145-147, 1972. Google Scholar
  22. Nicole Schweikardt, Luc Segoufin, and Alexandre Vigny. Enumeration for FO queries over nowhere dense graphs. In Proceedings of the 37th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS 2018, pages 151-163. ACM, 2018. URL: https://doi.org/10.1145/3196959.3196971.
  23. Saharon Shelah. A combinatorial problem; stability and order for models and theories in infinitary languages. Pacific Journal of Mathematics, 41(1):247-261, 1972. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail