Florin Manea

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.

MFCS Conference 2025 Conference Paper

Linear Time Subsequence and Supersequence Regex Matching

• Antoine Amarilli
• Florin Manea
• Tina Ringleb
• Markus L. Schmid

It is well-known that checking whether a given string w matches a given regular expression r can be done in quadratic time O(|w|⋅ |r|) and that this cannot be improved to a truly subquadratic running time of O((|w|⋅ |r|)^{1-ε}) assuming the strong exponential time hypothesis (SETH). We study a different matching paradigm where we ask instead whether w has a subsequence that matches r, and show that regex matching in this sense can be solved in linear time O(|w| + |r|). Further, the same holds if we ask for a supersequence. We show that the quantitative variants where we want to compute a longest or shortest subsequence or supersequence of w that matches r can be solved in O(|w|⋅ |r|), i. e. , asymptotically no worse than classical regex matching; and we show that O(|w| + |r|) is conditionally not possible for these problems. We also investigate these questions with respect to other natural string relations like the infix, prefix, left-extension or extension relation instead of the subsequence and supersequence relation. We further study the complexity of the universal problem where we ask if all subsequences (or supersequences, infixes, prefixes, left-extensions or extensions) of an input string satisfy a given regular expression.

IJCAI Conference 2024 Conference Paper

Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis

• Zhengyang Lu
• Stefan Siemer
• Piyush Jha
• Joel Day
• Florin Manea
• Vijay Ganesh

Modern SMT solvers, such as Z3, offer user-controllable strategies that allow solver users the ability to tailor solving strategies for their unique set of instances, thus dramatically enhancing the solver performance for their specific use cases. However, this approach of strategy customization presents a significant challenge: handcrafting an optimized strategy for a class of SMT instances remains a complex and demanding task for both solver developers and users alike. In this paper, we address this problem of automated SMT strategy synthesis via a novel Monte Carlo Tree Search (MCTS) based method. Our method treats strategy synthesis as a sequential decision-making process, whose search tree corresponds to the strategy space, and employs MCTS to navigate this vast search space. The key innovations that enable our method to identify effective strategies, while keeping costs low, are the ideas of layered and staged MCTS search. These novel heuristics allow for a deeper and more efficient exploration of the strategy space, enabling us to synthesize more effective strategies than the default ones in state-of-the-art (SOTA) SMT solvers. We implement our method, dubbed Z3alpha, as part of the Z3 SMT solver. Through extensive evaluations across six important SMT logics, Z3alpha demonstrates superior performance compared to the SOTA synthesis tool FastSMT, the default Z3 solver, and the CVC5 solver on most benchmarks. Remarkably, on a challenging QF_BV benchmark set, Z3alpha solves 42. 7% more instances than the default strategy in Z3.

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.

MFCS Conference 2021 Conference Paper

Matching Patterns with Variables Under Hamming Distance

• Pawel Gawrychowski
• Florin Manea
• Stefan Siemer

A pattern α is a string of variables and terminal letters. We say that α matches a word w, consisting only of terminal letters, if w can be obtained by replacing the variables of α by terminal words. The matching problem, i. e. , deciding whether a given pattern matches a given word, was heavily investigated: it is NP-complete in general, but can be solved efficiently for classes of patterns with restricted structure. In this paper, we approach this problem in a generalized setting, by considering approximate pattern matching under Hamming distance. More precisely, we are interested in what is the minimum Hamming distance between w and any word u obtained by replacing the variables of α by terminal words. Firstly, we address the class of regular patterns (in which no variable occurs twice) and propose efficient algorithms for this problem, as well as matching conditional lower bounds. We show that the problem can still be solved efficiently if we allow repeated variables, but restrict the way the different variables can be interleaved according to a locality parameter. However, as soon as we allow a variable to occur more than once and its occurrences can be interleaved arbitrarily with those of other variables, even if none of them occurs more than once, the problem becomes intractable.

Highlights Conference 2020 Conference Abstract

Efficiently Testing Simon’s Congruence

• Florin Manea

Simon’s congruence is defined as follows: two words are -equivalent if they have the same set of subsequences of length at most. We propose an algorithm which computes, given two words and, the largest for which. Our algorithm runs in linear time when the input words are over the integer alphabet (or other alphabets which can be sorted in linear time). This approach leads to an optimal algorithm in the case of general alphabets as well. Our results are based on a novel combinatorial approach and a series of efficient data structures.

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.

TCS Journal 2018 Journal Article

Revisiting Shinohara's algorithm for computing descriptive patterns

• Henning Fernau
• Florin Manea
• Robert Mercaş
• Markus L. Schmid

A pattern α is a word consisting of constants and variables and it describes the pattern language L ( α ) of all words that can be obtained by uniformly replacing the variables with constant words. In 1982, Shinohara presents an algorithm that computes a pattern that is descriptive for a finite set S of words, i. e. , its pattern language contains S in the closest possible way among all pattern languages. We generalise Shinohara's algorithm to subclasses of patterns and characterise those subclasses for which it is applicable. Furthermore, within this set of pattern classes, we characterise those for which Shinohara's algorithm has a polynomial running time (under the assumption P ≠ NP ). Moreover, we also investigate the complexity of the consistency problem of patterns, i. e. , finding a pattern that separates two given finite sets of words.

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 on Languages and Combinatorics in Theory and Nature

• Florin Manea
• Bianca Truthe
• György Vaszil

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.

I&C Journal 2014 Journal Article

The pseudopalindromic completion of regular languages

• Szilárd Zsolt Fazekas
• Florin Manea
• Robert Mercaş
• Kayoko Shikishima-Tsuji

Pseudopalindromes are words that are fixed points for some antimorphic involution. In this paper we discuss a newer word operation, that of pseudopalindromic completion, in which symbols are added to either side of the word such that the new obtained words are pseudopalindromes. This notion represents a particular type of hairpin completion, where the length of the hairpin is at most one. We give precise descriptions of regular languages that are closed under this operation and show that the regularity of the closure under the operation is decidable.

TCS Journal 2012 Journal Article

Complexity results for deciding Networks of Evolutionary Processors

• Florin Manea

The Accepting Networks of Evolutionary Processors (ANEPs for short) are bio-inspired computational models which were introduced and thoroughly studied in the last decade. In this paper we propose a method of using ANEPs as deciding devices. More precisely, we define a new halting condition for this model, which seems more coherent with the rest of the theory than the previous such definitions, and show that all the computability related results reported so far remain valid in the new framework. Further, we are able to show a direct and efficient simulation of an arbitrary ANEP by an ANEP having a complete underlying graph; as a consequence of this result, we conclude that the efficiency of deciding a language by ANEPs is not influenced by the network’s topology. Finally, focusing on the computational complexity of ANEP-based computations, we obtain a surprising characterisation of P NP [ log ] as the class of languages that can be decided in polynomial time by such networks.

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.

TCS Journal 2012 Journal Article

Language classes generated by tree controlled grammars with bounded nonterminal complexity

• Sherzod Turaev
• Jürgen Dassow
• Florin Manea
• Mohd Hasan Selamat

A tree controlled grammar is specified as a pair ( G, G ′ ) where G is a context-free grammar and G ′ is a regular grammar. Its language consists of all terminal words with a derivation in G such that all levels of the corresponding derivation tree–except the last level–belong to L ( G ′ ). We define the nonterminal complexity V ar ( H ) of H = ( G, G ′ ) as the sum of the numbers of nonterminals of G and G ′. In Turaev et al. (2011) [23] it is shown that tree controlled grammars H with V ar ( H ) ≤ 9 are sufficient to generate all recursively enumerable languages. In this paper, we improve the bound to seven. Moreover, we show that all linear and regular simple matrix languages can be generated by tree controlled grammars with a nonterminal complexity bounded by three, and we prove that this bound is optimal for the mentioned language families. Furthermore, we show that any context-free language can be generated by a tree controlled grammar ( G, G ′ ) where the number of nonterminals of G and G ′ is at most four.

TCS Journal 2012 Journal Article

On external contextual grammars with subregular selection languages

• Jürgen Dassow
• Florin Manea
• Bianca Truthe

In this paper, we study the power of external contextual grammars with selection languages from subfamilies of the family of regular languages. If we consider families F n which are obtained by restriction to n states or nonterminals or productions or symbols to accept or to generate regular languages, we obtain four infinite hierarchies of the corresponding families of languages generated by external contextual grammars with selection languages in F n. Moreover, we give some results on the power of external contextual grammars with regular commutative, regular circular, definite, suffix-free, ordered, combinational, nilpotent, and union-free selection languages.

I&C Journal 2011 Journal Article

Bounded hairpin completion

• Masami Ito
• Peter Leupold
• Florin Manea
• Victor Mitrana

Hairpin completion is a formal operation inspired from biochemistry. Here we consider a restricted variant of hairpin completion called bounded hairpin completion. Applied to a word encoding a single stranded molecule x such that either a suffix or a prefix of x is complementary to a subword of x, hairpin completion produces a new word z, which is a prolongation of x to the right or to the left by annealing. Although this operation is a purely mathematical one and the biological reality is just a source of inspiration, it seems rather unrealistic to impose no restriction on the length of the prefix or suffix added by the hairpin completion. The restriction considered here concerns the length of all prefixes and suffixes that are added to the current word by hairpin completion. They cannot be longer than a given constant. Closure properties of some classes of formal languages under the non-iterated and iterated bounded hairpin completion are investigated. We consider the bounded hairpin completion distance between two words and generalize this distance to languages and discuss algorithms for computing them. Finally also the inverse operation, namely bounded hairpin reduction, as well as the set of all primitive bounded hairpin roots of a regular language are considered.

MFCS Conference 2011 Conference Paper

Periodicity Algorithms for Partial Words

• Florin Manea
• Robert Mercas
• Catalin Tiseanu

Abstract In this paper we investigate several periodicity-related algorithms for partial words. First, we show that all periods of a partial word of length n are determined in \({\mathcal O}(n\log n)\) time, and provide algorithms and data structures that help us answer in constant time queries regarding the periodicity of their factors. For this we need a \({\mathcal O}(n^2)\) preprocessing time and a \({\mathcal O}(n)\) updating time, whenever the words are extended by adding a letter. In the second part we show that substituting letters of a word w with holes, with the property that no two holes are too close to each other, to make it periodic can be done in optimal time \({\mathcal O}(|w|)\). Moreover, we show that inserting the minimum number of holes such that the word keeps the property can be done as fast.

TCS Journal 2010 Journal Article

A series of algorithmic results related to the iterated hairpin completion

• Florin Manea

In this paper we propose efficient algorithmic solutions for the computation of the hairpin completion distance between two given words, for the computation of a minimum-distance common hairpin completion ancestor of two given words (i. e. , a word from which we can obtain the two given words by iterated hairpin completion, such that the sum of the hairpin completion distances from this word to the two given words is minimum), and, respectively, for the computation of an arbitrary hairpin completion ancestor of two given words. In all the cases we improve the upper bounds known for time complexity of solving these problems. Then we show how the algorithms designed for these three initial problems can be modified to solve a series of related problems.

ICAART Conference 2009 Conference Paper

Accepting Networks of Evolutionary Processors: Complexity Aspects - Recent Results and New Challenges

• Florin Manea
• Victor Mitrana

In this paper we survey some results reported so far, for the new computational model of Accepting Networks of Evolutionary Processors (ANEPs), in the area of computational and descriptional complexity. First we give the definitions of the computational model, and its variants, then we define several ANEP complexity classes, and, further, we show how some classical complexity classes, defined for Turing Machines, can be characterized in this framework. After this, we briefly show how ANEPs can be used to solve efficiently NP-complete problems. Finally, we discuss a list of open problems and further directions of research which appear interesting to us.

TCS Journal 2009 Journal Article

On small, reduced, and fast universal accepting networks of splicing processors

• Remco Loos
• Florin Manea
• Victor Mitrana

In this paper, we show that accepting networks of splicing processors (ANSPs) of size 2 are computationally complete. Since, by definition, an ANSP needs at least two nodes to perform non-trivial computations, this completely settles the question of designing complete ANSPs of minimal size. Also, we derive from this result the fact that all the languages in PSPACE can be accepted by ANSPs of size 2, having polynomial length complexity (the ANSP complexity measure for the space used in a computation). However, the construction that we propose, although efficient from the descriptional complexity and space complexity points of view, does not seem to have good properties from the time complexity point of view. In this respect, we prove that ANSPs of size three can decide all languages in NP in polynomial time. The previous lower bound on size for both completeness and efficient acceptance of NP-languages was seven. We also consider ANSPs with restricted features, proving the following normal forms: for any ANSP there exists an equivalent ANSP without input filters, and one without output filters. Finally, we show how to construct a small universal ANSP and make several considerations on the computational efficiency of universal ANSPs.

TCS Journal 2009 Journal Article

Two complementary operations inspired by the DNA hairpin formation: Completion and reduction

• Florin Manea
• Victor Mitrana
• Takashi Yokomori

We consider two complementary operations: Hairpin completion introduced in [D. Cheptea, C. Martin-Vide, V. Mitrana, A new operation on words suggested by DNA biochemistry: Hairpin completion, in: Proc. Transgressive Computing, 2006, pp. 216–228] with motivations coming from DNA biochemistry and hairpin reduction as the inverse operation of the hairpin completion. Both operations are viewed here as formal operations on words and languages. We settle the closure properties of the classes of regular and linear context-free languages under hairpin completion in comparison with hairpin reduction. While the class of linear context-free languages is exactly the weak-code image of the class of the hairpin completion of regular languages, rather surprisingly, the weak-code image of the class of the hairpin completion of linear context-free languages is a class of mildly context-sensitive languages. The closure properties with respect to the hairpin reduction of some time and space complexity classes are also studied. We show that the factors found in the general cases are not necessary for regular and context-free languages. This part of the paper completes the results given in the earlier paper, where a similar investigation was made for hairpin completion. Finally, we briefly discuss the iterated variants of these operations.

TCS Journal 2007 Journal Article

Accepting networks of splicing processors: Complexity results

• Florin Manea
• Carlos Martín-Vide
• Victor Mitrana

In this paper we consider a new, bio-inspired computing model: the accepting network of splicing processors. We define two computational complexity classes based on this model and show how they are related to the classical ones defined for Turing machines, namely NP and PSPACE. Furthermore, we approach the topic of problem solving using these newly defined devices. In this context, a linear time solution for one of the most interesting NP-complete problems, the SAT problem, is presented. The results presented here suggest once more that nondeterminism might be approached in a deterministic way by means of multiplicities.

TCS Journal 2007 Journal Article

Erratum to: “Accepting networks of splicing processors: Complexity results” [Theoret. Comput. Sci. 371 (2007) 72–82]

• Florin Manea
• Carlos Martín-Vide
• Victor Mitrana

TCS Journal 2007 Journal Article

Freeness of partial words

• Florin Manea
• Robert Mercaş

The paper approaches the classical combinatorial problem of freeness of words, in the more general case of partial words. First, we propose an algorithm that tests efficiently whether a partial word is k -free or not, for a given k. Then, we show that there exist arbitrarily many k -free infinite partial words, over a binary alphabet, containing an infinite number of holes, for k ≥ 3. Moreover, we present an efficient algorithm for the construction of a cube-free partial word with a given number of holes, over a binary alphabet. In the final section of the paper, we show that there exists an infinite word, over a four-symbol alphabet, in which we can substitute randomly one symbol with a hole, and still obtain a cube-free word; we show that such a word does not exist for alphabets with fewer symbols. Further, we prove that in this word we can replace arbitrarily many symbols with holes, such that each two consecutive holes are separated by at least two symbols, and obtain a cube-free partial word. This result seems interesting because any partial word containing two holes with less than two symbols between them is not cube-free. Finally, we modify the previously presented algorithm to construct, over a four-symbol alphabet, a cube-free partial word with exactly n holes, having minimal length, among all the possible cube-free partial words with at least n holes.

TCS Journal 2006 Journal Article

An efficient approach for the rank aggregation problem

• Liviu P. Dinu
• Florin Manea

This paper presents some computational properties of the rank-distance, a measure of similarity between partial rankings. We show how this distance generalizes the Spearman footrule distance, preserving its good computational complexity: the rank-distance between two partial rankings can be computed in linear time, and the rank aggregation problem can be solved in polynomial time. Further, we present a generalization of the rank-distance to strings, which permits to solve the median string problem in polynomial time. This appears rather surprising to us given the fact that for other non-trivial string distances, such as edit-distance, this problem is NP-hard.