Definability of some $k$-ary Relations Over Second Order kinds of Logics

Articles in Press

Document Type : Original paper

Authors

1 DICATAM - Sez. Matematica, Universit`a degli Studi di Brescia, Via Branze 43, I-25123 Brescia, Italy

2 DII, Università degli Studi di Brescia, Via Branze 38, I-25123 Brescia, Italy

Abstract

We consider the exprissibility in monadic second order logic of certain relations of importance in computer science. For integers $n\geq 1$ and $k\leq b$, a $k$-tuple of sequences in $\{0,1,\ldots, b-1\}^n$ are said to be $k$-hashed if there is a coordinate where they all differ. A set $\mathcal{C}$ of sequences is said to be a $k$-hash code if any $k$ distinct elements are $k$-hashed. Testing whether a code is $k$-hashing and determining the largest size of $k$-hash codes is an important problem in computer science. The use of general purpose solvers for this problem leads to question what minimal logic is needed to represent the problem.
In this paper, we prove that the $k$-hashing relation on $k$-tuples is not definable in Monadic Second Order Logic (MSO), highlighting its limitations for this problem. Instead, the property can be expressed in extensions of the MSO that add the equi-cardinality relation.
Finally, since to the best of our knowledge there are no available solvers for MSO with such global cardinality constraints,
we provide a practical SMT encoding in Z3 for fixed parameters. In addition, we computationally recover the non-existence of a trifferent code of size $11$ and length $5$.

Keywords

References

[1] S. Bhandari and A. Khetan, Improved upper bound for the size of a trifferent code, Combinatorica 45 (2025), Article number: 2 https://doi.org/10.1007/s00493-024-00130-2
[2] A. Bishnoi, J. D’haeseleer, D. Gijswijt, and A. Potukuchi, Blocking sets, minimal codes and trifferent codes, J. London Math. Soc. 109 (2024), no. 6, e12938. https://doi.org/10.1112/jlms.12938
[3] S. Costa and M. Dalai, A gap in the slice rank of k-tensors, J. Comb. Theory, Series A 177 (2021), 105335. https://doi.org/10.1016/j.jcta.2020.105335
[4] B. Courcelle, The monadic second-order logic of graphs, II: Infinite graphs of bounded width, Math. Systems Theory 21 (1988), no. 1, 187–221. https://doi.org/10.1007/BF02088013
[5] B. Courcelle, The monadic second-order logic of graphs. I. Recognizable sets of finite graphs, Info. Comput. 85 (1990), no. 1, 12–75. https://doi.org/10.1016/0890-5401(90)90043-H
[6] L. De Moura and N. Bjørner, Z3: An efficient SMT solver, International conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 4963.
[7] S. Della Fiore, A. Gnutti, and S. Polak, The maximum cardinality of trifferent codes with lengths 5 and 6, Examples and Counterexamples 2 (2022), 100051.  https://doi.org/10.1016/j.exco.2022.100051
[8] J.G. Henriksen, J. Jensen, M. Jørgensen, N. Klarlund, R. Paige, T. Rauhe, and A. Sandholm, Mona: Monadic second-order logic in practice, International workshop on tools and algorithms for the construction and analysis of systems, vol. 1019, Springer, 1995, pp. 89–110.
[9] L. Herrmann, V. Peth, and S. Rudolph, Decidable (ac) counting with Parikh and Muller: adding Presburger arithmetic to monadic second-order logic over treeinterpretable structures, 32nd EACSL Annual Conference on Computer Science
Logic (2024).
[10] F. Klaedtke and H. Rueß, Monadic second-order logics with cardinalities, International Colloquium on Automata, Languages, and Programming, vol. 2719, Springer, 2003, pp. 681–696.
[11] J. Körner and S. G´abor, Trifference, Studia Scientiarum Mathematicarum Hungarica 30 (1995), 95–103.
[12] J. Körner and K. Marton, New bounds for perfect hashing via information theory, Eur. J. Comb. 9 (1988), no. 6, 523–530. https://doi.org/10.1016/S0195-6698(88)80048-9
[13] V. Kuncak, H.H. Nguyen, and M. Rinard, An algorithm for deciding BAPA: Boolean algebra with Presburger arithmetic, International Conference on Automated Deduction, vol. 3632, Springer, 2005, pp. 260–277.
[14] V. Kuncak, H.H. Nguyen, and M. Rinard, Deciding Boolean algebra with Presburger arithmetic, J. Automat. Rea-
soning 36 (2006), no. 3, 213–239. https://doi.org/10.1007/s10817-006-9042-1
[15] S. Kurz, Trifferent codes with small lengths, Examples and Counterexamples 5 (2024), 100139. https://doi.org/10.1016/j.exco.2024.100139
[16] H. Läuchli and C. Savioz, Monadic second order definable relations on the binary tree, The Journal of Symbolic Logic 52 (1987), no. 1, 219–226. https://doi.org/10.2307/2273878
[17] L. Libkin, Elements of Finite Model Theory, vol. 41, Springer, 2004.
Communications in Combinatorics and Optimization

Articles in Press, Accepted Manuscript
Available Online from 23 February 2026

Files

Share

How to cite

Statistics