Dirk Nowotka

TCS Journal 2025 Journal Article

Generalised Nyldon words

• Pamela Fleischmann
• Annika Huch
• Dirk Nowotka

One of the most studied famous classes of words is the class of Lyndon words. Their studies are mainly motivated by the property that they factorise the free monoid as shown in the famous Chen-Fox-Lyndon Theorem. Several generalisations of Lyndon words as anti-Lyndon words, Nyldon words or inverse Lyndon words were made over time. In 2014, Grinberg introduced Nyldon words as a new perspective on the factorisation of the free monoid of words. In particular, for Nyldon words the famous Chen-Fox-Lyndon Theorem is considered w. r. t. a reversed lexicographical order, i. e. , a lexicographically non-decreasing factorisation where each factor is smaller or equal than its successor. Further, a generalised lexicographical order is defined by equipping each position i in a word in Σ ⁎ with a total order ◃ i on Σ. For combining the concept of a generalised order as for generalised Lyndon words and the class of Nyldon words, we investigate a non-decreasing factorisation of the free monoid w. r. t. this generalised ordering and introduce generalised Nyldon words. We show that those words even force a unique non-decreasing factorisation, form a right Hall set, and coincide with the anti-Lyndon words.

I&C Journal 2025 Journal Article

k-Universality of Regular Languages

• Duncan Adamson
• Pamela Fleischmann
• Annika Huch
• Tore Koß
• Florin Manea
• Dirk Nowotka

A subsequence of a word w is a word u such that u = w [ i 1 ] w [ i 2 ] … w [ i k ], for some set of indices 1 ≤ i 1 < i 2 < … < i k ≤ | w |. A word w is k-subsequence universal over an alphabet Σ if every word in Σ k appears in w as a subsequence. In this paper, we study the intersection between the set of k-subsequence universal words over some alphabet Σ and regular languages over Σ. We call a regular language L k-∃-subsequence universal if there exists a k-subsequence universal word in L, and k-∀-subsequence universal if every word of L is k-subsequence universal. We give algorithms solving the problems of deciding if a given regular language, represented by a finite automaton recognising it, is k-∃-subsequence universal and, respectively, if it is k-∀-subsequence universal, for a given k. The algorithms are FPT w. r. t. the size of the input alphabet, and their run-time does not depend on k; they run in polynomial time in the number n of states of the input automaton when the size of the input alphabet is O ( log ⁡ n ). Moreover, we show that the problem of deciding if a given regular language is k-∃-subsequence universal is NP-complete, when the language is over a large alphabet. Further, we provide algorithms for counting the number of k-subsequence universal words (paths) accepted by a given deterministic (respectively, non-deterministic) finite automaton, and ranking an input word (path) within the set of k-subsequence universal words accepted by a given finite automaton.

TCS Journal 2023 Journal Article

Nearly k-universal words – Investigating a part of Simon's congruence

• Pamela Fleischmann
• Lukas Haschke
• Jonas Höfer
• Annika Huch
• Annika Mayrock
• Dirk Nowotka

Determining the index of Simon's congruence is a long outstanding open problem. Two words u and v are called Simon congruent if they have the same set of scattered factors (also known as subwords or subsequences), which are parts of the word in the correct order but not necessarily consecutive, e. g. , oath is a scattered factor of logarithm but tail is not. Following the idea of scattered factor k-universality (also known as k-richness), we investigate m-nearly k-universality, i. e. , words where exactly m scattered factors of length k are absent. We present full characterisations as well as the indexes of the congruence for very small and very large m. Moreover, we give a full combinatorial characterisation of m-nearly k-universal words which are additionally ( k − 1 ) -universal.

TCS Journal 2023 Journal Article

Towards more efficient methods for solving regular-expression heavy string constraints

• Murphy Berzish
• Joel D. Day
• Vijay Ganesh
• Mitja Kulczynski
• Florin Manea
• Federico Mora
• Dirk Nowotka

Widespread use of string solvers in the formal analysis of string-heavy programs has led to a growing demand for more efficient and reliable techniques which can be applied in this context. Designing practical algorithms for the (generally undecidable) satisfiability problem for systems of string constraints requires a deep understanding of the structure of constraints present in the targeted cases. In this paper, we first investigate relevant benchmarks containing regular expression membership predicates, extract a series of first order logic theories, and prove the decidability, respectively undecidability, of their satisfiability problem. Further, building on the theoretical results, we present a novel length-aware solving algorithm for the quantifier-free first-order theory over regular expression membership predicates and linear arithmetic over string length. We implement and evaluate this algorithm and related heuristics in the Z3 theorem prover. Besides the theoretical aspects leading to this algorithm, a crucial insight that underpins it is that real-world regex and string formulas contain a wealth of information about upper and lower bounds on lengths of strings, and such information can be used very effectively to simplify operations on automata representing regular expressions. Additionally, we present several novel general heuristics, such as the prefix/suffix method, that can be used to make a variety of regex solving algorithms more efficient in practice. We showcase the power of our algorithm and heuristics via an extensive empirical evaluation over a large and diverse benchmark of 57256 regex-heavy instances, almost 75% of which are derived from industrial applications or contributed by other solver developers. Our solver outperforms five other state-of-the-art string solvers over this benchmark.

FormaliSE Conference 2020 Conference Paper

Rule-based Word Equation Solving

• Joel D. Day
• Mitja Kulczynski
• Florin Manea
• Dirk Nowotka
• Danny Bøgsted Poulsen

We present a transformation-system-based technique in the framework of string solving, by reformulating a classical combinatorics on words result, the Lemma of Levi. We further enrich the induced rules by simplification steps based on results from the combinatorial theory of word equations, as well as by the addition of linear length constraints. This transformation-system approach cannot solve all equations efficiently by itself. To improve the efficiency of our transformation-system approach we integrate existing successful string solvers, which are called based on several heuristics. The experimental evaluation we performed shows that integrating our technique as an inprocessing step improves in general the performance of existing solvers.

MFCS Conference 2019 Conference Paper

Upper Bounds on the Length of Minimal Solutions to Certain Quadratic Word Equations

• Joel D. Day
• Florin Manea
• Dirk Nowotka

It is a long standing conjecture that the problem of deciding whether a quadratic word equation has a solution is in NP. It has also been conjectured that the length of a minimal solution to a quadratic equation is at most exponential in the length of the equation, with the latter conjecture implying the former. We show that both conjectures hold for some natural subclasses of quadratic equations, namely the classes of regular-reversed, k-ordered, and variable-sparse quadratic equations. We also discuss a connection of our techniques to the topic of unavoidable patterns, and the possibility of exploiting this connection to produce further similar results.

MFCS Conference 2018 Conference Paper

Lagrange's Theorem for Binary Squares

• P. Madhusudan
• Dirk Nowotka
• Aayush Rajasekaran
• Jeffrey O. Shallit

We show how to prove theorems in additive number theory using a decision procedure based on finite automata. Among other things, we obtain the following analogue of Lagrange's theorem: every natural number > 686 is the sum of at most 4 natural numbers whose canonical base-2 representation is a binary square, that is, a string of the form xx for some block of bits x. Here the number 4 is optimal. While we cannot embed this theorem itself in a decidable theory, we show that stronger lemmas that imply the theorem can be embedded in decidable theories, and show how automated methods can be used to search for these stronger lemmas.

TCS Journal 2018 Journal Article

Unary patterns under permutations

• James Currie
• Florin Manea
• Dirk Nowotka
• Kamellia Reshadi

Thue characterized completely the avoidability of unary patterns. Adding function variables gives a general setting capturing avoidance of powers, avoidance of patterns with palindromes, avoidance of powers under coding, and other questions of recent interest. Unary patterns with permutations have been previously analysed only for lengths up to 3. Consider a pattern p = π i 1 ( x ) … π i r ( x ), with r ≥ 4, x a word variable over an alphabet Σ and π i j function variables, to be replaced by morphic or antimorphic permutations of Σ. If | Σ | ≥ 3, we show the existence of an infinite word avoiding all pattern instances having | x | ≥ 2. If | Σ | = 3 and all π i j are powers of a single morphic or antimorphic π, the length restriction is removed. For the case when π is morphic, the length dependency can be removed also for | Σ | = 4, but not for | Σ | = 5, as the pattern x π 2 ( x ) π 56 ( x ) π 33 ( x ) becomes unavoidable. Thus, in general, the restriction on x cannot be removed, even for powers of morphic permutations. Moreover, we show that for every positive integer n there exists N and a pattern π i 1 ( x ) … π i n ( x ) which is unavoidable over all alphabets Σ with at least N letters and π morphic or antimorphic permutation.

TCS Journal 2017 Journal Article

TCS Special Issue: Combinatorics on Words – WORDS 2015

• Florin Manea
• Dirk Nowotka

MFCS Conference 2017 Conference Paper

The Hardness of Solving Simple Word Equations

• Joel D. Day
• Florin Manea
• Dirk Nowotka

We investigate the class of regular-ordered word equations. In such equations, each variable occurs at most once in each side and the order of the variables occurring in both left and right hand sides is preserved (the variables can be, however, separated by potentially distinct constant factors). Surprisingly, we obtain that solving such simple equations, even when the sides contain exactly the same variables, is NP-hard. By considerations regarding the combinatorial structure of the minimal solutions of the more general quadratic equations we obtain that the satisfiability problem for regular-ordered equations is in NP. The complexity of solving such word equations under regular constraints is also settled. Finally, we show that a related class of simple word equations, that generalises one-variable equations, is in P.

MFCS Conference 2012 Conference Paper

Fine and Wilf's Theorem and Pseudo-repetitions

• Florin Manea
• Robert Mercas
• Dirk Nowotka

Abstract The notion of repetition of factors in words is central to considerations on sequences. One of the recent generalizations regarding this concept was introduced by Czeizler et al. (2010) and investigates a restricted version of that notion in the context of DNA computing and bioinformatics. It considers a word to be a pseudo-repetition if it is the iterated concatenation of one of its prefixes and the image of this prefix through an involution. We present here a series of results in the fashion of the Fine and Wilf Theorem in a more general setting where we consider the periods of some word given by a prefix of it and images of that prefix through some arbitrary morphism or antimorphism.

MFCS Conference 2007 Conference Paper

Height-Deterministic Pushdown Automata

• Dirk Nowotka
• Jirí Srba

Abstract We define the notion of height-deterministic pushdown automata, a model where for any given input string the stack heights during any (nondeterministic) computation on the input are a priori fixed. Different subclasses of height-deterministic pushdown automata, strictly containing the class of regular languages and still closed under boolean language operations, are considered. Several such language classes have been described in the literature. Here, we suggest a natural and intuitive model that subsumes all the formalisms proposed so far by employing height-deterministic pushdown automata. Decidability and complexity questions are also considered.

TCS Journal 2006 Journal Article

On unique factorizations of primitive words

• Tero Harju
• Dirk Nowotka

We give a short proof of a result by Weinbaum [Unique sunwords in nonperiodic words, Proc. Amer. Math. Soc. 109(3) (1990) 615–619] stating that each primitive word of length at least 2 has a conjugate w ′ = uv such that both u and v have a unique position in the cyclic word of w. We emphasize the connection of Weinbaum's result to the Critical Factorization Theorem.

TCS Journal 2005 Journal Article

A characterization of periodicity of bi-infinite words

• Tero Harju
• Arto Lepistö
• Dirk Nowotka

A finite word is called bordered if it has a proper prefix which is also a suffix of that word. Costa proves in [Theoret. Comput. Sci. 290(3) (2003) 2053–2061] that a bi-infinite word w is of the form fgf ω ω, for some finite words f and g, if, and only if, there is a factorization w = suv, with u ∈ A * such that every factor s ′ uv ′, with s ′ ≼ s and v ′ ⩽ v, is bordered. We present a shorter proof of that result in this paper.

TCS Journal 2005 Journal Article

Counting bordered and primitive words with a fixed weight

• Tero Harju
• Dirk Nowotka

A word w is primitive if it is not a proper power of another word, and w is unbordered if it has no prefix that is also a suffix of w. We study the number of primitive and unbordered words w with a fixed weight, that is, words for which the Parikh vector of w is a fixed vector. Moreover, we estimate the number of words that have a unique border.

TCS Journal 2005 Journal Article

On the equation x k = z 1 k 1 z 2 k 2 ⋯ z n k n in a free semigroup

• Tero Harju
• Dirk Nowotka

Word equations of the form x k = z 1 k 1 z 2 k 2 ⋯ z n k n are considered in this paper. In particular, we investigate the case where x is of different length than z i, for any i, and k and k i are at least 3, for all 1 ⩽ i ⩽ n, and n ⩽ k. We prove that for those equations all solutions are of rank 1, that is, x and z i are powers of the same word for all 1 ⩽ i ⩽ n. It is also shown that this result implies a well-known result by Appel and Djorup about the more special case where k i = k j for all 1 ⩽ i < j ⩽ n.

TCS Journal 2003 Journal Article

On the independence of equations in three variables

• Tero Harju
• Dirk Nowotka

We prove that an independent system of equations in three variables with a nonperiodic solution and at least two equations consists of balanced equations only. For that, we show that the intersection of two different entire systems contains only balanced equations, where an entire system is the set of all equations solved by a given morphism. Furthermore, we establish that two equations which have a common nonperiodic solution have the same set of periodic solutions or are not independent.