Abstract We investigate the locality number, a recently introduced structural parameter for strings (with applications in pattern matching with variables), and its connection to two important graph-parameters, cutwidth and pathwidth. These connections allow us to show that computing the locality number is $$\textsf {NP}$$ NP -hard, but fixed-parameter tractable, if parameterised by the locality number or by the alphabet size, which has been formulated as open problems in the literature. Moreover, the locality number can be approximated with ratio $${{\,\textrm{O}\,}}(\sqrt{\log ({{\,\mathrm{\textsf {opt}}\,}})} \log (n))$$ O ( log ( opt ) log ( n ) ) . An important aspect of our work – that is relevant in its own right and of independent interest – is that we identify connections between the string parameter of the locality number on the one hand, and the famous graph parameters of cutwidth and pathwidth, on the other hand. These two parameters have been jointly investigated in the literature and are arguably among the most central graph parameters that are based on “linearisations” of graphs. In this way, we also identify a direct approximation preserving reduction from cutwidth to pathwidth, which shows that any polynomial $$f({{\,\mathrm{\textsf {opt}}\,}},|V|)$$ f ( opt , | V | ) -approximation algorithm for pathwidth yields a polynomial $$2f(2{{\,\mathrm{\textsf {opt}}\,}},h)$$ 2 f ( 2 opt , h ) -approximation algorithm for cutwidth on multigraphs (where h is the number of edges). In particular, this translates known approximation ratios for pathwidth into new approximation ratios for cutwidth, namely $${{\,\textrm{O}\,}}(\sqrt{\log ({{\,\mathrm{\textsf {opt}}\,}})} \log (h))$$ O ( log ( opt ) log ( h ) ) and $${{\,\textrm{O}\,}}(\sqrt{\log ({{\,\mathrm{\textsf {opt}}\,}})} {{\,\mathrm{\textsf {opt}}\,}})$$ O ( log ( opt ) opt ) for (multi) graphs with h edges.

Core spanners are a class of document spanners that capture the core functionality of IBM’s AQL. FC is a logic on strings built around word equations that when extended with constraints for regular languages can be seen as a logic for core spanners. The recently introduced FC-Datalog extends FC with recursion, which allows us to define recursive relations for core spanners. Additionally, as FC-Datalog captures 𝖯, it is also a tractable version of Datalog on strings. This presents an opportunity for optimization. We propose a series of FC-Datalog fragments with desirable properties in terms of complexity of model checking, expressive power, and efficiency of checking membership in the fragment. This leads to a range of fragments that all capture LOGSPACE, which we further restrict to obtain linear combined complexity. This gives us a framework to tailor fragments for particular applications. To showcase this, we simulate deterministic regex in a tailored fragment of FC-Datalog.

Abstract Modern SMT solvers, such as Z3, allow solver users to customize strategies to improve performance on their specific use cases. However, handcrafting an optimized strategy for a specific class of SMT instances remains a complex and demanding task for both solver developers and users alike. In this paper, we address the problem of automated SMT strategy synthesis via a novel method based on Monte-Carlo Tree Search (MCTS). We formulate strategy synthesis as a sequential decision-making process, where the search tree corresponds to the strategy space. Subsequently, we employ MCTS to navigate this vast search space. Compared to the conventional MCTS, we introduce two heuristics—layered and staged search—that enable our method to identify effective strategies with lower costs. We implement our method, dubbed Z3alpha, upon the Z3 SMT solver. Our experiments demonstrate that Z3alpha outperforms the default Z3 solver and the state-of-the-art synthesis tool Fastsmt on the majority of the evaluated benchmark sets, while producing more interpretable strategies than FastSMT. At SMT-COMP’24, among the 16 participating logics, Z3alpha improved upon the default Z3 in 12 cases and helped solve hundreds more instances in QF_NIA and QF_NRA, winning their respective divisions.

http://dx.doi.org/10.13039/501100001659 German Research Foundation

Abstract Word equations are equations $$\alpha \doteq \beta $$ α ≐ β where $$\alpha $$ α and $$\beta $$ β are words consisting of letters from some alphabet $$\Sigma $$ Σ and variables from a set X. Recently, there has been substantial interest in the context of string solving in logics combining word equations with other kinds of constraints on words such as (regular) language membership (regular constraints) and arithmetic over string lengths (length constraints). We consider the expressive power of such logics by looking at the set of all values a single variable might take as part of a satisfying assignment for a given formula. Hence, each formula-variable pair defines a formal language, and each logic defines a class of formal languages. We consider logics arising from combining word equations with either length constraints, regular constraints, or both. We also consider word equations with visibly pushdown language membership constraints as a generalisation of the combination of regular and length constraints. We show that word equations with visibly pushdown membership constraints are sufficient to express all recursively enumerable languages and hence satisfiability is undecidable in this case. We then establish a strict hierarchy involving the other combinations. We also provide a complete characterisation of when a thin regular language is expressible by word equations (alone) and some further partial results for regular languages in the general case.

Abstract For quadratic word equations, there exists an algorithm based on rewriting rules which generates a directed graph describing all solutions to the equation. For regular word equations – those for which each variable occurs at most once on each side of the equation – we investigate the properties of this graph, such as bounds on its diameter, size, and DAG-width, as well as providing some insights into symmetries in its structure. As a consequence, we obtain a combinatorial proof that the problem of deciding whether a regular word equation has a solution is in NP.

We investigate properties of strings which are expressible by canonical types of string constraints. Specifically, we consider a landscape of 20 logical theories, whose syntax is built around combinations of four common elements of string constraints: language membership (e.g. for regular languages), concatenation, equality between string terms, and equality between string-lengths. For a variable x and formula f from a given theory, we consider the set of values for which x may be substituted as part of a satisfying assignment, or in other words, the property f expresses through x. Since we consider string-based logics, this set is a formal language. We firstly consider the relative expressive power of different combinations of string constraints by comparing the classes of languages expressible in the corresponding theories, and are able to establish a mostly complete picture in this regard. Secondly, we consider the question of deciding whether the language or property expressed by a variable/formula in one theory can be expressed in another theory. We establish several negative results which are relevant to preprocessing and normalisation of string constraints in practice. Some of our results have strong connections to important open problems regarding word equations and the theory of string solving.

We consider subsequences with gap constraints, i.e., length-k subsequences p that can be embedded into a string w such that the induced gaps (i.e., the factors of w between the positions to which p is mapped to) satisfy given gap constraints $gc = (C_1, C_2, ..., C_{k-1})$; we call p a gc-subsequence of w. In the case where the gap constraints gc are defined by lower and upper length bounds $C_i = (L^-_i, L^+_i) \in \mathbb{N}^2$ and/or regular languages $C_i \in REG$, we prove tight (conditional on the orthogonal vectors (OV) hypothesis) complexity bounds for checking whether a given p is a gc-subsequence of a string w. We also consider the whole set of all gc-subsequences of a string, and investigate the complexity of the universality, equivalence and containment problems for these sets of gc-subsequences.

A morphism g is ambiguous with respect to a word u if there exists a second morphism h≠g such that g(u)=h(u). Otherwise g is unambiguous with respect to u. Thus unambiguous morphisms are those for which the structure of the morphism is preserved in the image. Ambiguity has so far been studied for morphisms of free monoids, where several characterisations exist for the set of words u permitting an (injective) unambiguous morphism. In the present paper, we consider ambiguity of morphisms of free groups, and consider possible analogies to the existing characterisations in the free monoid. While a direct generalisation results in a trivial situation where all morphisms are ambiguous, we discuss some natural and well-motivated reformulations, and provide a characterisation of words in a free group that permit a morphism which is “as unambiguous as possible”.

Abstract We present a novel length-aware solving algorithm for the quantifier-free first-order theory over regex membership predicate and linear arithmetic over string length. We implement and evaluate this algorithm and related heuristics in the Z3 theorem prover. A crucial insight that underpins our algorithm 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 a number of 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, namely, CVC4, OSTRICH, Z3seq, Z3str3, and Z3-Trau, over this benchmark, in particular achieving a speedup of 2.4 $$\times $$ × over CVC4, 4.4 $$\times $$ × over Z3seq, 6.4 $$\times $$ × over Z3-Trau, 9.1 $$\times $$ × over Z3str3, and 13 $$\times $$ × over OSTRICH.

A word u is a subsequence of another word w if u can be obtained from w by deleting some of its letters. In the early 1970s, Imre Simon defined the relation ∼_k (called now Simon-Congruence) as follows: two words having exactly the same set of subsequences of length at most k are ∼_k-congruent. This relation was central in defining and analysing piecewise testable languages, but has found many applications in areas such as algorithmic learning theory, databases theory, or computational linguistics. Recently, it was shown that testing whether two words are ∼_k-congruent can be done in optimal linear time. Thus, it is a natural next step to ask, for two words w and u which are not ∼_k-equivalent, what is the minimal number of edit operations that we need to perform on w in order to obtain a word which is ∼_k-equivalent to u. In this paper, we consider this problem in a setting which seems interesting: when u is a k-subsequence universal word. A word u with alph(u) = Σ is called k-subsequence universal if the set of subsequences of length k of u contains all possible words of length k over Σ. As such, our results are a series of efficient algorithms computing the edit distance from w to the language of k-subsequence universal words.

For quadratic word equations, there exists an algorithm based on rewriting rules which generates a directed graph describing all solutions to the equation. For regular word equations - those for which each variable occurs at most once on each side of the equation - we investigate the properties of this graph, such as bounds on its diameter, size, and DAG-width, as well as providing some insights into symmetries in its structure. As a consequence, we obtain a combinatorial proof that the problem of deciding whether a regular word equation has a solution is in NP.

We investigate the locality number, a recently introduced structural parameter for strings (with applications in pattern matching with variables), and its connection to two important graph-parameters, cutwidth and pathwidth. These connections allow us to show that computing the locality number is NP-hard but fixed-parameter tractable (when the locality number or the alphabet size is treated as a parameter), and can be approximated with ratio O(sqrt{log{opt}} log n). As a by-product, we also relate cutwidth via the locality number to pathwidth, which is of independent interest, since it improves the best currently known approximation algorithm for cutwidth. In addition to these main results, we also consider the possibility of greedy-based approximation algorithms for the locality number.

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.

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.