Arrow Research search

Author name cluster

Florin Manea

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

25 papers
2 author rows

Possible papers

25

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.

Details

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.

PDF Details DOI

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.

Details

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.

PDF Details

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.

Details

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.

Details

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.

Details

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.

Details

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.

Details

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.

Details