Abstract
In this work we introduce the notion of decisional width of a finite relational structure and the notion of regular-decisional width of a regular class of finite structures. Our main result states that the first-order theory of any regular-decisional class of finite structures is decidable. Building on the proof of this decidability result, we show that the problem of counting satisfying assignments for a first-order logic formula in a structure of constant width is fixed parameter tractable when parameterized by the width parameter and can be solved in quadratic time with respect to the length of the input representation of the structure.
Keywords
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
MSO\(_1\) denotes the MSO logic of graphs where edge-set quantifications are not allowed, while MSO\(_2\) is the extension of MSO\(_1\) where we can also quantify over sets of edges.
- 2.
Note that Theorem 5.2 implies that the first-order theory of unlabeled grids is decidable, since unlabeled grids have constant decisional-width. Nevertheless, it is known that the first-order theory of labeled grids is undecidable. In this latter case, we may have labeled grids that require ODDs of arbitrarily high width to be represented.
References
Blumensath, A.: Automatic structures. Diploma thesis. Rheinisch-Westfälische Technische Hochschule Aachen (1999)
Blumensath, A., Gradel, E.: Automatic structures. In: Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, pp. 51–62. IEEE (2000)
Bollig, B.: On symbolic OBDD-based algorithms for the minimum spanning tree problem. Theoret. Comput. Sci. 447, 2–12 (2012)
Bollig, B.: On the width of ordered binary decision diagrams. In: Zhang, Z., Wu, L., Xu, W., Du, D.-Z. (eds.) COCOA 2014. LNCS, vol. 8881, pp. 444–458. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12691-3_33
Bonomo, F., Grippo, L.N., Milanič, M., Safe, M.D.: Graph classes with and without powers of bounded clique-width. Discrete Appl. Math. 199, 3–15 (2016)
Büchi, J.R.: Weak second order arithmetic and finite automata. Z. Math. Logik Grundl. Math. 6, 66–92 (1960)
Bulatov, A.A.: Graphs of relational structures: restricted types. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 642–651. ACM (2016)
Chandran, L.S., Kavitha, T.: The treewidth and pathwidth of hypercubes. Discrete Math. 306(3), 359–365 (2006)
Courcelle, B.: The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Inf. Comput. 85(1), 12–75 (1990)
Courcelle, B., Makowsky, J.A., Rotics, U.: Linear time solvable optimization problems on graphs of bounded clique-width. Theory Comput. Syst. 33(2), 125–150 (2000)
Ebbinghaus, H.D., Flum, J., Thomas, W.: Mathematical Logic. Springer, New York (2013)
Ebbinghaus, H.D., Flum, J.: Finite Model Theory. Springer, Heidelberg (2005)
Elgot, C.C.: Decision problems of finite automata and related arithmetics. Trans. Am. Math. Soc. 98, 21–52 (1961)
Farb, B.: Automatic groups: a guided tour. Enseign. Math. (2) 38(3–4), 291–313 (1992)
Getoor, L., Friedman, N., Koller, D., Taskar, B.: Learning probabilistic models of relational structure. In: ICML, vol. 1, pp. 170–177 (2001)
Grohe, M.: Algorithmic meta theorems. In: Broersma, H., Erlebach, T., Friedetzky, T., Paulusma, D. (eds.) WG 2008. LNCS, vol. 5344, p. 30. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-92248-3_3
Grohe, M.: Algorithmic meta theorems for sparse graph classes. In: Hirsch, E.A., Kuznetsov, S.O., Pin, J.É., Vereshchagin, N.K. (eds.) CSR 2014. LNCS, vol. 8476, pp. 16–22. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06686-8_2
Hachtel, G.D., Somenzi, F.: A symbolic algorithm for maximum flow in 0-1 networks. In: Proceedings of the 1993 IEEE/ACM International Conference on Computer-Aided Design, pp. 403–406. IEEE Computer Society Press (1993)
Hliněnỳ, P., Seese, D.: Trees, grids, and MSO decidability: from graphs to matroids. Theoret. Comput. Sci. 351(3), 372–393 (2006)
Khoussainov, B., Minnes, M.: Three lectures on automatic structures. In: Proceedings of Logic Colloquium, pp. 132–176 (2007)
Khoussainov, B., Nerode, A.: Automatic presentations of structures. In: Leivant, D. (ed.) LCC 1994. LNCS, vol. 960, pp. 367–392. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60178-3_93
Kolaitis, P.G., Vardi, M.Y.: A game-theoretic approach to constraint satisfaction. In: AAAI/IAAI, pp. 175–181 (2000)
Kreutzer, S.: Algorithmic meta-theorems. In: Grohe, M., Niedermeier, R. (eds.) IWPEC 2008. LNCS, vol. 5018, pp. 10–12. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-79723-4_3
Kruckman, A., Rubin, S., Sheridan, J., Zax, B.: A Myhill-Nerode theorem for automata with advice. In: Proceedings of GANDALF 2012. Electronic Proceedings in Theoretical Computer Science, vol. 96, pp. 238–246 (2012)
Poon, H., Domingos, P.M., Sumner, M.: A general method for reducing the complexity of relational inference and its application to MCMC. In: AAAI, vol. 8, pp. 1075–1080 (2008)
Sawitzki, D.: Implicit flow maximization by iterative squaring. In: Van Emde Boas, P., Pokorný, J., Bieliková, M., Štuller, J. (eds.) SOFSEM 2004. LNCS, vol. 2932, pp. 301–313. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24618-3_26
Seese, D.: The structure of the models of decidable monadic theories of graphs. Ann. Pure Appl. Log. 53(2), 169–195 (1991)
Sutskever, I., Tenenbaum, J.B., Salakhutdinov, R.R.: Modelling relational data using Bayesian clustered tensor factorization. In: Advances in Neural Information Processing Systems, pp. 1821–1828 (2009)
Woelfel, P.: Symbolic topological sorting with OBDDs. J. Discrete Algorithms 4(1), 51–71 (2006)
Zaid, F.A., Grädel, E., Reinhardt, F.: Advice automatic structures and uniformly automatic classes. In: 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). LIPIcs, vol. 82, pp. 35:1–35:20 (2017)
Acknowledgments
Alexsander Andrade de Melo acknowledges support from the Brazilian agencies CNPq/GD 140399/2017-8 and CAPES/PDSE 88881.187636/2018-01; and Mateus de Oliveira Oliveira acknowledges support from the Bergen Research Foundation and from the Research Council of Norway.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Andrade de Melo, A., de Oliveira Oliveira, M. (2019). On the Width of Regular Classes of Finite Structures. In: Fontaine, P. (eds) Automated Deduction – CADE 27. CADE 2019. Lecture Notes in Computer Science(), vol 11716. Springer, Cham. https://doi.org/10.1007/978-3-030-29436-6_2
Download citation
DOI: https://doi.org/10.1007/978-3-030-29436-6_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-29435-9
Online ISBN: 978-3-030-29436-6
eBook Packages: Computer ScienceComputer Science (R0)