Constraint satisfaction problems involving strings have been a subject of theoretical study for decades, but the recent years have seen an increased interest in the development of practical solving methods. This interest in solving string constraints led to the development of various techniques and solvers, often accompanied by specific benchmark sets. As a result, there is now a substantial corpus of publicly available, yet largely unclassified, such benchmarks. In this context, we present SMTQuery , a framework for maintaining and analyzing benchmarks for SMT string problems. SMTQuery enables the execution of user-defined queries to extract domain-specific information from these benchmarks, facilitating a deeper analysis of the underlying problems. We demonstrate its utility by analyzing over 100,000 benchmarks and training an algorithm selection model to match benchmarks with suitable solvers.

Abstract String solvers are automated-reasoning tools that can solve combinatorial problems over formal languages. They typically operate on restricted first-order logic formulas that include operations such as string concatenation, substring relationship, and regular expression matching. String solving thus amounts to deciding the satisfiability of such formulas. While there exists a variety of different string solvers, many string problems cannot be solved efficiently by any of them. We present a new approach to string solving that encodes input problems into propositional logic and leverages incremental SAT solving. We evaluate our approach on a broad set of benchmarks. On the logical fragment that our tool supports, it is competitive with state-of-the-art solvers. Our experiments also demonstrate that an eager SAT-based approach complements existing approaches to string solving in this specific fragment.