-
Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis
Authors:
Zhengyang Lu,
Stefan Siemer,
Piyush Jha,
Joel Day,
Florin Manea,
Vijay Ganesh
Abstract:
Modern SMT solvers, such as Z3, offer user-controllable strategies, enabling users to tailor solving strategies for their unique set of instances, thus dramatically enhancing solver performance for their use case. 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 fo…
▽ More
Modern SMT solvers, such as Z3, offer user-controllable strategies, enabling users to tailor solving strategies for their unique set of instances, thus dramatically enhancing solver performance for their use case. 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 automatic 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 kee** 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 the Z3 SMT solver.
△ Less
Submitted 30 April, 2024; v1 submitted 30 January, 2024;
originally announced January 2024.
-
Matching Patterns with Variables Under Simon's Congruence
Authors:
Pamela Fleischmann,
Sungmin Kim,
Tore Koß,
Florin Manea,
Dirk Nowotka,
Stefan Siemer,
Max Wiedenhöft
Abstract:
We introduce and investigate a series of matching problems for patterns with variables under Simon's congruence. Our results provide a thorough picture of these problems' computational complexity.
We introduce and investigate a series of matching problems for patterns with variables under Simon's congruence. Our results provide a thorough picture of these problems' computational complexity.
△ Less
Submitted 16 August, 2023;
originally announced August 2023.
-
Longest Common Subsequence with Gap Constraints
Authors:
Duncan Adamson,
Maria Kosche,
Tore Koß,
Florin Manea,
Stefan Siemer
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 t…
▽ More
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 effcient algorithms for determining the length of the longest common constrained subsequence between two given strings.
△ Less
Submitted 2 June, 2023; v1 submitted 11 April, 2023;
originally announced April 2023.
-
Combinatorial Algorithms for Subsequence Matching: A Survey
Authors:
Maria Kosche,
Tore Koß,
Florin Manea,
Stefan Siemer
Abstract:
In this paper we provide an overview of a series of recent results regarding algorithms for searching for subsequences in words or for the analysis of the sets of subsequences occurring in a word.
In this paper we provide an overview of a series of recent results regarding algorithms for searching for subsequences in words or for the analysis of the sets of subsequences occurring in a word.
△ Less
Submitted 10 October, 2022; v1 submitted 31 August, 2022;
originally announced August 2022.
-
Matching Patterns with Variables Under Edit Distance
Authors:
Paweł Gawrychowski,
Florin Manea,
Stefan Siemer
Abstract:
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 patter…
▽ More
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. If 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 (so matching under Hamming distance), one can devise efficient algorithms and matching conditional lower bounds for the class of regular patterns (in which no variable occurs twice), as well as for classes of patterns where we allow unbounded repetitions of variables, but restrict the structure of the pattern, i.e., the way the occurrences of different variables can be interleaved. Moreover, under Hamming distance, if a variable occurs more than once and its occurrences can be interleaved arbitrarily with those of other variables, even if each of these occurs just once, the matching problem is intractable. In this paper, we consider the problem of matching patterns with variables under edit distance. We still obtain efficient algorithms and matching conditional lower bounds for the class of regular patterns, but show that the problem becomes, in this case, intractable already for unary patterns, consisting of repeated occurrences of a single variable interleaved with terminals.
△ Less
Submitted 15 July, 2022;
originally announced July 2022.
-
Absent Subsequences in Words
Authors:
Maria Kosche,
Tore Koß,
Florin Manea,
Stefan Siemer
Abstract:
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 subse…
▽ More
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.
△ Less
Submitted 11 October, 2023; v1 submitted 31 August, 2021;
originally announced August 2021.
-
Matching Patterns with Variables under Hamming Distance
Authors:
Paweł Gawrychowski,
Florin Manea,
Stefan Siemer
Abstract:
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 patter…
▽ More
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.
△ Less
Submitted 11 June, 2021;
originally announced June 2021.
-
The Edit Distance to $k$-Subsequence Universality
Authors:
Pamela Fleischmann,
Maria Kosche,
Tore Koß,
Florin Manea,
Stefan Siemer
Abstract:
A word $u$ is a subsequence of another word $w$ if $u$ can be obtained from $w$ by deleting some of its letters. The word $w$ with alph$(w)=Σ$ is called $k$-subsequence universal if the set of subsequences of length $k$ of $w$ contains all possible words of length $k$ over $Σ$. We propose a series of efficient algorithms computing the minimal number of edit operations (insertion, deletion, substit…
▽ More
A word $u$ is a subsequence of another word $w$ if $u$ can be obtained from $w$ by deleting some of its letters. The word $w$ with alph$(w)=Σ$ is called $k$-subsequence universal if the set of subsequences of length $k$ of $w$ contains all possible words of length $k$ over $Σ$. We propose a series of efficient algorithms computing the minimal number of edit operations (insertion, deletion, substitution) one needs to apply to a given word in order to reach the set of $k$-subsequence universal words.
△ Less
Submitted 17 July, 2020;
originally announced July 2020.
-
Efficiently Testing Simon's Congruence
Authors:
Pawel Gawrychowski,
Maria Kosche,
Tore Koss,
Florin Manea,
Stefan Siemer
Abstract:
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 w…
▽ More
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.
△ Less
Submitted 15 March, 2021; v1 submitted 3 May, 2020;
originally announced May 2020.
