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 We consider the longest common subsequence problem in the context of subsequences with gap constraints. In particular, following Day et al. (2022), we consider the setting when the distance (i. e., the gap) between two consecutive symbols of the subsequence has to be between a lower and an upper bound (which may depend on the position of those symbols in the subsequence or on the symbols bordering the gap) as well as the case where the entire subsequence is found in a bounded range (defined by a single upper bound), considered by Kosche et al. (2022). In all these cases, we present efficient algorithms for determining the length of the longest common constrained subsequence between two given strings, and discuss lower bounds for the respective problems.

An absent factor of a string w is a string u which does not occur as a contiguous substring (a.k.a. factor) inside w. We extend this well-studied notion and define absent subsequences: a string u is an absent subsequence of a string w if u does not occur as subsequence (a.k.a. scattered factor) inside w. Of particular interest to us are minimal absent subsequences, i.e., absent subsequences whose every subsequence is not absent, and shortest absent subsequences, i.e., absent subsequences of minimal length. We show a series of combinatorial and algorithmic results regarding these two notions. For instance: we give combinatorial characterisations of the sets of minimal and, respectively, shortest absent subsequences in a word, as well as compact representations of these sets; we show how we can test efficiently if a string is a shortest or minimal absent subsequence in a word, and we give efficient algorithms computing the lexicographically smallest absent subsequence of each kind; also, we show how a data structure for answering shortest absent subsequence-queries for the factors of a given string can be efficiently computed.

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.

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.

Simon's congruence $\sim_k$ is defined as follows: two words are $\sim_k$-equivalent if they have the same set of subsequences of length at most $k$. We propose an algorithm which computes, given two words $s$ and $t$, the largest $k$ for which $s\sim_k t$. Our algorithm runs in linear time $O(|s|+|t|)$ when the input words are over the integer alphabet $\{1,\ldots,|s|+|t|\}$ (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.