# A meso-scale cartography of the AI ecosystem

Floriana Gargiulo  CNRS-GEMASS, 59 rue Pouchet 75017, Paris  Sylvain Fontaine
CREST, CNRS, IP PARIS, 91120 Palaiseau  Michel Dubois  Paola Tubaro

###### Abstract

In recent decades the set of knowledge, tools and practices, collectively
referred to as “artificial intelligence” (AI)’, have become a mainstay of
scientific research. Artificial intelligence techniques have not only
developed enormously within their native areas of development (computer
science, mathematics and statistics) but have also spread fast, in terms of
application, to multiple areas of science and technology. In this paper we
conduct a large scale analysis of artificial intelligence in science. The
first question we address is the composition of what is commonly labeled AI,
and how the various elements belonging to this domain are linked together. We
reconstruct the internal structure of the AI ecosystem through the co-
occurrence network of AI terms in publications’ abstracts and title, and we
propose to distinguish between 15 different specialities of AI, with different
temporal patterns. Further, we investigate the spreading of AI outside its
native disciplines. We reconstruct the temporal dynamics of the diffusion of
AI production in the whole scientific ecosystem and we describe the
disciplinary landscape of AI applications. Finally we take a further step
analyzing the role of collaborations for the interdisciplinary spreading of AI
techniques. While the study of science frequently emphasizes the openness of
scientific communities, we show that there are rarely any collaborations
between those scholars who primarily develop AI, and those who apply it. Only
a small group of researchers is able to gradually establish a bridge between
these communities.

###### keywords:

Artificial Intelligence, Science cartography, Science of science

## Introduction

Artificial intelligence (AI) is increasingly recognized as a vector of
technological and scientific innovation (Cockburn et al., (2018); Bianchini et
al., (2022)) with a potentially strong impact on economic growth (Aghion et
al., (2018)). A Nature editorial (nat, (2019)) describes it as one of the
scientific events that shaped the last decade: “Few fields are untouched by
the machine-learning revolution, from materials science to drug exploration;
quantum physics to medicine.”

The latest developments of AI, mostly as a result of the rise of Deep Learning
(DL), provide indeed a unique potential to extract information from the
unprecedented sources of data currently largely available in almost all
scientific and technological domains. AI has been described as enabling a
general paradigm shift toward a data immersive science (King et al., (2009),
Kitchin, (2014)), based on smart machines able to grasp the hidden patterns
and relationships from large masses of data.

The origins of AI are usually traced back to a renowned workshop held in 1956
in Dartmouth, where a group of scientists first used this term to define their
research activities and identify a distinct research area. According to the
definition given in 2004 by John Mc Carty, promoter of the Dartmouth workshop,
AI “is the science and engineering of making intelligent machines, especially
intelligent computer programs. It is related to the similar task of using
computers to understand human intelligence, but AI does not have to confine
itself to methods that are biologically observable.” (McCarthy, (2004))

This top-down definition, as well as similar ones (Annoni et al., (2018);
OECD, (2019); WIPO, (2019)), emphasizes the overall goals of AI but leaves
open the actual meaning of “intelligence”, the scope of the AI domain, and the
relationship between AI and the existing structure of scientific knowledge.

While the first question related to the definition of intelligence is highly
debated and controversial in the context of AI epistemology (McCarthy,
(1981)), our study sheds light on the second aspect and aims to reconstruct
the structure of the AI research area through a bottom-up approach based on a
cartography of AI–related scientific publications.

This bottom-up approach addresses two research questions:

  1. 1.

what is the structure of AI as a research area, i.e. the different
specialities within AI and their development over time?

  2. 2.

how has AI knowledge been dynamically embedded in traditional scientific
fields?

Previous works provide partial answers to these questions. For example (Frank
et al., (2019)) builds a classification based on citation networks among the
list of AI subfields, defined through the categories adopted in Microsoft
Academic Graph (MAG). However, this categorization does not allow a deep
understanding of which AI terms are explicitly present in a subdomain.
(Bianchini et al., (2020)) provide a mapping of the spreading of DL practices
in science and describe in great detail the geographical and disciplinary
spreading of DL, but do not address the connections of DL with other AI
practices. Other studies did so but only from the viewpoint of specific
disciplines (Baum et al., (2021)).

We start by establishing the semantic diversity of AI, building up a large
list of terms that are related to it without distinction of context,
generality, temporality, or other criteria. Assemblng a suitable set of
keywords for a bibliometric search is in itself a complex task, simplified in
our case by the possibility to rely on the multiple glossaries of AI
accessible online, first of all the Wikipedia AI glossary which also contains
synonyms for several terms. We therefore build the list of AI keywords by
mining a large number of AI glossaries available on the web, that represent
how different actors, dealing with AI, draw the perimeter of AI. These terms
represent the semantic building blocks of AI.

Whether we describe it as a body of knowledge, practice or tools, AI is a
dynamic phenomenon that has experienced several phases in its evolution over
time. As scientific innovation in general (Uzzi et al., (2013)) can be viewed
as a cumulative process where novelty arises from the recombination of
existing building blocks, a dynamical definition of AI can be seen as the
result of the recombination of its building blocks, i.e. the formation of its
specialities through the recombination of AI basic terms. Interdisciplinary
exchanges also play a central role in scientific innovation, proposing new
possible building blocks and thereby opening the “adjacent possible” of
scientific discoveries (Kauffman, (2000); Monechi et al., (2017)). Likewise,
extensions of AI arise from the recombination of pre–existing applications and
by interactions with other research areas: consider the example of DL,
resulting from AI research on Artificial Neural Networks recombined with the
connectionist approach in cognitive science. For this reason, understanding
the embedding of AI in the scientific ecosystem provides fundamental
information to grasp its building process.

In the last decade, a relevant increase of the application of AI techniques in
several and diverse scientific domains has been observed, above all in
relation with the development of DL (Bianchini et al., (2020, 2022)). The
common idea behind this phenomenon is that AI is spreading from its “native”
disciplines (mainly computer science, mathematics and statistics), where its
key tools were designed, to a series of applications in various fields of
knowledge. This distinction between native disciplines and application
disciplines can be found in several studies (Cockburn et al., (2018);
Bianchini et al., (2022)).

In this study we analyze a large corpus of papers from 1970 until 2017,
extracted from Microsoft Academic Graph, using AI keywords cited by the
authors and different relational structures among the scientometric data
(keyword co-occurrence network, authors’ collaboration network). To
characterize the keywords used in corpus selection, we define their
hierarchical structure in order to distinguish the core AI terms from the most
peripheral ones (mainly specific algorithms and techniques). We first focus on
the definition of the meso–scale structure of AI, namely on the identification
of the specialities of AI, their interactions and their temporal patterns
(Section 2.1). Second, we analyze how AI is globally spreading in muliple
research areas or disciplines. A first phase of concentration of AI in the
“native” disciplines of computer science, mathematics, and statistics can be
observed at the end of the 1980s, after the so-called “AI Winter”, with the
emergence of expert systems and the decline of symbolic AI. These disciplines
will remain responsible for the production of AI literature until today.
However, a spreading phase started in the last decade, corresponding with the
development of DL, where AI knowledge started to be largely applied to several
other disciplines (Section 2.2). We also show the disciplinary patterns
associated with the different specialities of AI. We can observe for example
that only a few specialities (like dimensionality reduction techniques and DL)
were able to reach a high degree of diversity in the application ecosystem.
Finally, we highlight the collaboration mechanisms responsible for knowledge
transfer from the originating domains to applications. We notice indeed that
very few collaborations exist between researchers in disciplines that create
AI and researchers in disciplines that only (or mainly) apply AI. The transfer
of AI knowledge is largely ascribable to a core of multidisciplinary
researchers mutually interacting both with AI developers and with researchers
in applied disciplines (Section 2.3).

##  1 Data and Methods

###  1.1 AI terms

There are several definitions of AI, and each of them implies a different
perimeter of the terms or lexical units associated with it. With the effort of
defining the perimeter of AI, several and diverse actors involved in its
production made available online glossaries containing lists of associated
keywords, with the objective of identifying the variety of terms that it
covers. In particular, Wikipedia has a large list of its pages connected to
AI, including synonyms.

We started by extracting the content of the Wikipedia index
page111https://en.wikipedia.org/wiki/Glossary_of_artificial_intelligence and,
after that, we performed a Google query searching for “AI glossary”,“AI
keywords”, “AI terms”, “ AI concepts”. We obtained a set of more than 20
specific glossaries, for example 222https://developers.google.com/machine-
learning/glossary 333https://machinelearning.wtf/
444https://link.springer.com/content/pdf/bbm:978-3-319-94878-2/1.pdf.

We built our original list of terms from all the keywords from these web
resources, removing duplicates and lemmatizing words. We manually cleaned the
list of keywords, removing very general words not strictly related to AI (like
“software”, “algorithm”, and “self-management”). The final list includes 594
terms, mostly bigrams or trigrams, with different levels of generality. There
are general terms like “machine learning” and specific algorithmic procedures
like “word2vec”. The full list of terms is reported in the appendix.

###  1.2 The bibliometric dataset

The bibliometric dataset on which this article is based starts from a recent
data dump of the Microsoft Academic Graph (MAG), disambiguated, and made
available by M. Färber on the Zenodo platform
555https://zenodo.org/record/4617285#.YlUoaS2ubs0 (Färber, (2019)). From this
dataset, we first selected all the papers including any of the previously
identified 594 AI-terms in their abstracts or title (2,737,813 papers with
associated metadata). From this set we only keep the papers published after
1970. This choice could appear too strict, missing almost two decades of early
AI research, but it avoids the heterogeneities that would result from
differences in editorial policies and scientific infrastructure in that period
compared to today, notably in terms of peer reviewing. Additionally, we retain
only studies published in or before 2017 because of a possible bias in the MAG
database for later entries, which can be guessed from an unmotivated decrease
in the total number of papers. We further filtered this dataset to the papers
published in journals or conferences indexed in the Web of Science (WoS),
getting a final set of metadata for 1,090,138 papers. We associate to each of
these papers two supplementary attributes with respect to the MAG metadata:
the disciplinary fields, according to the first label (which is indeed the
more specific) in the WoS classification of journals and conferences, and the
list of AI keywords contained in their abstracts. To build the authors’
collaboration network we used the disambiguated authors’ identifiers provided
by Färber et al. in the last version of the MAG database (Färber and Ao,
(2022)).

To summarize, the bibliometric corpus that we have constituted starting from
the MAG dataset is a collection of documents having the following attributes
(Figure 1): The list of the AI keywords contained in the abstract and/or
title, the publication year, the list of authors, the journal (or conference),
and the disciplinary field derived from the journal’s classification and
categorical structure in the WoS.

Figure 1: The dataset. Left plot: filtering process of the MAG corpus. Top
right plot: Structure of the AI corpus. Bottom right plot: Building process of
the keywords co-occurrence network and of the author collaboration network

###  1.3 The network structures

With these data, we reconstruct two different network structures: the keyword
co-occurrence network (KCON) and the author collaboration network (ACN).

These networks are directly built from the documents of the corpus as
described in Figure 1. For the keyword co-occurrence, each document that
contains more than a keyword represents an hyperedge of the graph, namely a
fully connected subgraph among all the present keywords. These hyperedges are
merged together and each link gets a weight corresponding to the number of
hyperedges where it is present. The procedure is identical for the authors’
collaborations. Both these graphs are undirected weighted structures.

The keyword co-occurrence graph, KCON, has 535 nodes and 24,358 edges (some
less frequently used AI terms were indeed disconnected from the larger
component and were therefore omitted in the rest of the analyses). Being this
network extremely dense (density=0.17) and being the weights very
heterogeneous, we first apply a disparity filter on the original graph
(Serrano et al., (2009)) to get the relevant connections and simplify the
partitioning of the structure. The filtered graph DKCON has 3,276 edges. The
author collaboration network (ACN) has 103,175 nodes and 453,137 edges.

###  1.4 The disciplinary distance matrix

To reconstruct a distance matrix between all the WoS disciplines, we started
again from the whole MAG dataset, filtered on the WoS journals. To reduce
computation time, which would be very significant if we analyzed a single
large snapshot from this extremely large dataset, we followed a procedure of
producing several independent samples. Specifically, we extracted 10,000
random samples of 100,000 papers. For each paper in each random sample we
extracted the list of all the referenced papers and, from the latter, the set
of unique WoS disciplines relative to the references. From these lists of
disciplines, following the same procedure adopted for the KCON and the ACN
networks, we build the co-citation structure of disciplines in the sample.

Since the weighting structure of this graph (the number of co-occurrences
$w_{ij}$) is strongly related to the relative frequency of each discipline we
implement a similarity measure based on the pointwise mutual information
between the nodes (disciplines):

$\text{pmi}_{ij}=\text{max}\left(2\text{log}_{2}\left(\frac{w_{ij}}{\sum_{k}(w_{ik})\sum_{k}(w_{jk})}\right),0\right)$
(1)

The pointwise mutual information ranges indeed between -1 and 1; in our case,
the negative values, representing a very uncorrelated situation are put to
zero to obtain an indicator ranging from 0 to 1. From this similarity measure
we simply obtain a distance matrix whose values are given by:
$D_{ij}=1-pmi_{ij}$.

We repeat this computation for all the 10,000 samples and the final distance
matrix is derived from the average values on all the samples.

###  1.5 The spreading indicators

We measure how a corpus is concentrated around the so-called native
disciplines of AI (as above, computer science, mathematics and statistics)
with a measure inspired from solid body mechanics, the moment of inertia:

$m_{I}=\sum_{i}\frac{n_{i}}{N_{tot}}\text{min}(D_{i,CS},D_{i,Math},D_{i,Stat})^{2}$
(2)

where $i$ covers all the disciplines present in the corpus. If the moment of
inertia is small, the corpus is very concentrated around the native
disciplines; if not, it is largely diffused in the disciplinary ecosystem.

To measure how AI is represented in a discipline we compare the number
$n_{i}^{AI}$ of AI papers produced in this discipline with an expected value
given by the share of publications in the given discipline
($s_{i}=N_{tot}^{i}/N_{tot}$, extracted from the whole MAG corpus) multiplied
by the total number of AI publications. We define therefore the AI score of a
discipline:

$z_{i}=\frac{n_{i}^{AI}-N_{tot}^{AI}s_{i}}{n_{i}^{AI}+N_{tot}^{AI}s_{i}}$ (3)

This measure ranges between -1 and 1. Positive high values of this indicator
indicate that AI is more represented in the discipline than in a case in which
diffusion followed a random process, and vice-versa. The same measure also
applies at the level of journals.

Finally, we compute for each author in the corpus an AI score, $A_{I}$, given
by the fraction of papers published by the author in the native disciplines of
computer science, mathematics and statistics.

##  2 Results

###  2.1 The specialities of AI

AI is an umbrella term encompassing a broad set of knowledge, tools and
practices aimed to the general purpose of making intelligent machines and
computer programs. For a comprehensive understanding of AI, it is essential to
describe its specialities or thematic diversity. To do this, we adopt a
bottom-up approach based on the analysis of AI related scientific
publications. In particular, we study the co-occurrence of the AI keywords in
the abstracts, DKCON, as described in the methods section.

As we pointed out in the data presentation, the keywords used in the query
have different levels of “generality”. We first use the filtered keyword co-
occurence graph (DKCON) to identify the hierarchy of dependencies between
keywords. We build the $k$-shell structure of the graph and we calculate the
internal density of each shell, compared to the density of the whole DKCON
graph. This analysis allows to distinguish three dimensions: the super core,
the core and the periphery. Figure 2 shows that the first two shells are very
dense: they include a group of 25 keywords largely used and tightly connected
among them. We call these first two shells the “super-core”. This class
contains general AI categories (“artificial intelligence”,“‘machine learning”,
“DL”, “neural networks”) and very popular classes of methods (“random forest”,
“support vector machine”). The internal density decreases suddenly starting
from the third shell and goes to zero in the most external shells, starting
from the seventh one. We define shells 3-6 the “core” and the last ones as the
“periphery”. The core also contains general methods (such as “cluster
analysis”, “particle swarm optimization‘”, “stochastic gradient descent”) but
less connected among them and hierarchically depending on super-core terms
(namely connected to the corpus only through super-core terms). The periphery
mostly contains specific algorithms and specific methods not connected among
them but just to the more central cores.

Figure 2: AI term hierarchy.

We apply to the DKCON graph the well-known Louvain community detection
algorithm (Blondel et al., (2008)) and identify the presence of 15 meso-scale
structures that correspond to a partitioning of the network at the level of
specialities (Figure 3): expert systems, natural language processing,
dimensionality reduction, data mining, classifiers, neural networks, robotics,
genetic algorithms, speech recognition, logic programming, face recognition,
Turing machines, reinforcement learning, computer vision and DL. These
structures are labeled according to their internal concept characterized by
the term with the highest core position.

Figure 3: AI specialities and their relationships.

Some of these specialities show a significant degree of openness,
demonstrating a flow of knowledge from one domain to the other. For example
the DL speciality has several semantic relationships both with neural networks
and with classifiers. Classifiers and dimensionality reduction are strictly
related, being indeed the latter a particular form of classification. Computer
vision has connections with the classifier class but also with DL, as indeed
computer vision was one of the first application domains of DL techniques.

The different AI specialities are also characterized by different temporal
patterns that better define the temporality of the knowledge flows between
them. In Figure 4 we show the annual time series of the number of publications
in each area. AI general terms, as well as Turing machine and logic
programming (symbolic AI), widely diffused in the early days, disappeared
after the AI winter – around 1995 – while on the contrary the “expert systems”
speciality (together with agent-based systems) started to emerge. Just
afterwards, we observe the rapid growth of specialities like neural networks,
data mining, optimization and face recognition. Finally, the last two decades
see a fast decrease of specialities like optimization and dimensionality
reduction, parallel to the extremely fast development of DL. Analyzing the
relationships among specialities, while optimization research does not seem to
enter new combinations with keywords in emerging areas (indicating a gradual
fading of research interest in this domain), dimensionality reduction is being
gradually recombined with DL concepts.

Figure 4: The timeline of AI specialities.

###  2.2 AI: from development to applications

The study of our database highlights an important, and perhaps somewhat
surprising, fact : almost half of the publications included (48%) are
associated with disciplines outside the native computer science, mathematics
or statistics. This section strictly focuses on this subset of the corpus: the
applied side of AI.

For each year starting from 1970, we calculate the moment of inertia of the
corpus. As outlined above, this indicator measures the dispersion of the
corpus around the native disciplines. With this measure, the historical
dynamics of AI appears as an oscillation between periods marked by forms of
disciplinary dispersion followed by periods of disciplinary concentration.
Figure 5 shows that before 1988, AI was present in numerous disciplines beyond
computer science, mathematics and statistics (high moment of inertia). The so-
called native disciplines were not the exclusive founders of AI whose origins
appear to be much more interdisciplinary, with inputs from, among others,
engineering, philosophy and psychology. In 1988 a phase of concentration
around native disciplines began, reaching a maximum in 2010 (low $m_{I}$).
After 2010, the moment of inertia starts to increase again, indicating the
gradual spreading of AI knowledge to other disciplinary domains, more distant
from the native disciplines. Of note, the recent diffusion process started
with a delay of around ten years after the take-off of scientific production
in AI (around the year 2000).

Therefore, we observe cycles: a first phase of disciplinary diversity in the
AI ecosystem, then concentration (at the time of the AI winter and the
emergence of the expert systems tradition) followed by a recent diffusion
process (linked to the renewed interest in AI connected to DL applications).

In the lower plot of Figure 5 we analyze the relationship between the number
of papers in the native disciplines and the number of application papers. We
do this analysis both at the level of years (yellow points) and at the level
of specialities (coloured squares). The scaling shows the presence of two
different regimes: when the number of native papers (in computer science,
mathematics and statistics) is low ($<10,000$) we observe a sub–linear regime,
in that applications grow more slowly than development of new concepts and
tools. When the number of papers in native disciplines is high (and this trend
is also confirmed by the aggregated values in terms of specialities) we are in
a super–linear regime: the number of applications grows faster than the
development production, i.e. each paper in a native discipline gives rise to
more than an application paper.

Figure 5: AI development-vs-applications. Upper plot: Yellow line: moment of
inertia. Blue line: total number of AI publications. Lower plot: number of
application papers -vs- number of papers in native disciplines. Each yellow
point represents one year. Each square represents temporal aggregation at the
level of AI specialities.

After describing the aggregate scenario we explore the disciplinary
composition of the AI applied ecosystem. As could be expected, Figure 6 shows
that technological disciplines (such as engineering, robotics, imaging) are
the sectors in which AI is more largely over–represented. Some technical
medical disciplines, like neuroimaging and medical informatics, are also
intensely adopting AI methodologies. Our disciplinary AI score shows that the
physical sciences are not always well positioned. For example, AI techniques
are less prevalent in physics than in some social sciences fields such as
(following WoS classification) management, geography or linguistics. Only the
arts and humanities are consistently underrepresented.

This pattern can be also described at the granularity scale of journals where
we observe a dominance of AI in technology and multidisciplinary outlets. It
is important here to keep in mind that having excluded conferences for which
categorization is less fine, the physical sciences, life sciences, and social
sciences are mostly at the same level. However in all categories, the journals
that publish most AI-related papers are among those that specifically focus on
computational methods. In the multidisciplinary journal landscape, especially
noticeable is the presence of journals related to complex systems, which like
AI can be seen as a technological platform, with multiple contact points with
AI techniques (Li Vigni, (2021)).

Figure 6: AI application disciplinary landscape. Upper left plot: AI score
-vs- fraction of AI papers for all disciplines. The size of the points is
proportional to the total number of AI publications. Color indicates the WoS
disciplinary category. Upper right plot: boxplot of the AI score of the
journals in the six WoS disciplinary categories. Lower boxes: list of the top
10 journals publishing AI papers in each category.

Concerning the diffusion process of AI we can see that the disciplinary
ranking gets quite stable since the late 1990s (Figure 7). To measure distance
among rankings we use the “ranked Jaccard similarity” introduced in (Gargiulo
et al., (2016)). In the lower plots of Figure 7 we can observe some
prototypical trajectories of disciplines that experienced an important change
in the ranking from the 1990s until today. Some disciplines (above all in
social science) experienced a strong decrease being indeed strongly connected
to decreasing AI specialities like symbolic AI and Expert Systems. Disciplines
like physics and biology show a periodic growth (with a constant trend) in AI
adoption while others, like neuroimaging and green & sustainability
technologies, display a sudden climbing of the ranking since their creation.

Figure 7: AI application temporal disciplinary landscape. Upper plot: ranked
Jaccard similarity between disciplinary ranks in two subsequent years.

Examining specialities in more detail (Figure 8),. we observe that
“dimensionality reduction” is generally the most widespread in applications,
in quantitative terms (fraction of applications with respect to native papers)
and in terms of disciplinary distance from native disciplines. Instead, the
performance of “optimization” (the more represented speciality in terms of
total number of publications, as shown by the size of the point) is high in
terms of fraction of applications, but very low in terms of the moment of
inertia, namely it is largely applied in disciplines that are close to the
native ones.

The different knowledge domains have very diverse profiles in terms of the
adoption of AI specialities. In the arts and humanities, applications are
mostly related to Expert Systems. The social sciences have strong interest in
four AI specialities, namely machine learning, dimensionality reduction,
expert systems and natural language processing (NLP). Physical sciences, as
well as life sciences and multidisciplinary frameworks adopt dimensionality
reduction, classifiers and machine learning. Technology disciplines have a
much more uniform distribution on AI specialities. Optimization is relevant
only for technology and, to a lesser extent, for the physical sciences.

Figure 8: The disciplinary landscape of AI specialities. Left plot: Moment of
inertia around native disciplines -vs- fraction of applications, for all AI
specialities. Right plot: share of all the different AI specialities to the
main knowledge domains.

###  2.3 Authors’ collaborations in the AI landscape

The last part of this study analyzes the collaboration patterns driving the
diffusion of AI. The basic question we address is whether the writing process
of papers applying AI involves the direct collaboration of AI developers and
experts in the application domains.

We assign to each author an AI score, $A_{I}$, as described above. The
distribution of authors’ AI scores shows two distinct peaks on the extremes,
one around 0 (authors never publishing in AI journals) and the second around 1
(authors only publishing in AI journals). We divide the authors in groups
according to the quartiles of their AI score: the first group (Q0) only
contains authors publishing in out-disciplinary journals ($A_{I}=0$), the last
one authors only publishing in AI journals (Q3, $A_{I}=1$), the two
intermediate groups (Q1 and Q2) contain authors having respectively an AI-
score lower and higher than 0.7 (Figure 9A).

From the histograms in Figure 9D we can also observe that authors in the first
group (Q0) mostly publish in biomedical disciplines, but also astrophysics.
Authors in Q1 are mostly specialized in interdisciplinary mathematical and
technological applications (like mathematical biology, operation research,
energy, telecommunications). Finally, Q2 includes mostly researchers in
general engineering.

Looking at Figure 9C, authors in Q0 have the highest moment of inertia around
native disciplines but at the same time have a low global level of
interdisciplinarity. They interact with few disciplines, quite close to each
other. Q1 includes most authors involved in interdisciplinary collaborations.
Q2 authors publish in disciplines close to the native ones (low moment of
inertia) but at a quite large distance from them.

Then we analyze the author collaboration network (ACN), the weighted graph
structure where all authors present in the database are linked to all the
other authors they collaborated with. Weight is given by the number of joint
publications. Aggregating at the level of the four AI score groups of the
authors, we calculate the fraction of collaborations between each class and
all the others. To avoid the bias that might result from the different sizes
of the groups, we compare these values to the expected multinomial
distribution of these links (Figure 9B). As we can observe from the figure, AI
authors (those in the third and fourth quartiles of the AI-score distribution,
Q2 and Q3) mostly collaborate among themselves. Authors in Q2, as observed
before, are mostly involved in engineering disciplines and are therefore more
connected to AI developers. On the contrary, disciplinary experts (Q0 and Q1)
have few collaborations with AI developers (Q3) and collaborate among them.

This highlights a clear separation among the scholars who do research on AI
and those who do research with AI. Application of AI to other disciplines is
not primarily driven by direct collaborations between authors with different
backgrounds. However, there are some direct collaborations among the second
and the third groups. To some extent, authors in these groups constitute a
bridge between the theoretical development of AI and the disciplinary
applications.

Figure 9: AI collaborations. Plot A: Distribution of the authors’ AI score,
and identification of the quartiles. Plot B: Collaborations between groups of
authors. The map refers to the comparison with the multinomial expectations
for the links. Plot C: Box plots of the moment of inertia and of the inter-
disciplinary distance for each group of authors. Plot D: Top 10 disciplines
(sorted according to the disciplinary AI score in the group) in which the
authors of each group specialize. The color of the points represents the
knowledge domain associated to the discipline.

##  3 Discussion

We have built a bottom-up cartography of AI, based on an analysis of the
scientific production on AI, from 1970 until 2017.

We started from an expert-based definition of AI trough the identification of
all the terms that different actors involved in AI studies use to structure
the vocabulary of this research field (collected as mentioned above, through
an all-encompassing analysis of the web pages containing AI glossaries).

We show the effects of what historians of science call the “AI winters”,
periods in which interest in AI declined. We also show that the AI scientific
platform came out of these crises thanks to the innovation dynamics arising
from the recombination of specialities: for example expert systems in the
1990s and DL around 2010 (DL was initially defined in 2006 and largely spread
in 2012, with the ImageNet challenge).

The emergence of innovative specialities is partially due to the recombination
of pre–existing building blocks from other domains but also from the dynamics
of interdisciplinary participation.

We therefore studied the historical spread of AI in the traditional
disciplines. After the foundation of AI in a very interdisciplinary context,
we identified a first phase of disciplinary “concentration”, during the “AI
winter” during which the development of AI knowledge, previously distributed
among several fields, condensed on the so-called native disciplines: computer
science, mathematics and statistics. Only more recently, starting from 2010,
we observe a new interdisciplinary phase of AI, with its gradual spreading to
a larger number of fields where it is applied.

Transfer of AI knowledge from development to application of AI is mediated by
scientists in multiple fields of study, notably applied mathematical fields
(like for example mathematical biology), geology, biophysics, and some
engineering applied fields. A relevant role has been played in the last decade
by multidisciplinary journals where applied AI papers from several fields were
published.

The aim of this study was to reconstruct a bottom-up definition of AI,
building a dynamic cartography of this domain from its published traces. Its
deeper intent is, more generally, to be a precursor analysis on several
directions of study connected to the more comprehensive ambition to understand
the role of AI in the transformation of the scientific ecosystem.

For example the structure of AI specialities would require an in-depth
qualitative study based on interviews of the actors involved in each of them,
in order to investigate their overall perception of AI and their positioning
in this quantitative landscape. A study of this type would be necessary to
globally assess if AI can be really defined as a scientific platform (Li
Vigni, (2021)) with a well–defined research program and objectives.

In this paper we mostly focused on the presence of AI terms in applied
disciplines. We adopted the designation of “native” AI disciplines from the
current literature (Cockburn et al., (2018); Bianchini et al., (2022)) but our
findings challenge it by showing how by its historical origin, AI was rather
an interdisciplinary research area. This interdisciplinary contribution was
mostly evident in the historical practices commonly known as symbolic systems.
Later, different scientific fields have become, in turn, the central
originating domains and applicators of AI knowledge, for example operational
research which was for a long time one of the core actors of AI applications
related to expert systems. A deeper historical analysis of the disciplines
that developed AI, and the specialities of AI they focused on, would be worth
of studying.

One way to investigate this question would be based on disciplinary case
studies. A discipline can indeed be transformed by the introduction of a new
set of knowledge, expanding its adjacent possible. Likewise, serendipitous
interactions with external fields could spark new ideas. For example,
neuroscience could be considered in principle as an originating domain of AI,
notably concerning the development of neural network architectures, but the
centrality of neuroscience journals in AI scientific production will need to
be ascertained in detail.

This paper gives therefore important hints on how to navigate the AI
scientific ecosystem in order to select potentially interesting case studies
for subsequent analyses.

## Acknowledgments

This work is partially founded by the ANR project ScientIA. The PhD fellowship
of S.F. is founded by the CNRS-MiTi program EpiAI. We thank M. Färber for
providing us with very useful information about the structure of the MAG
database.

## References

  * nat, (2019) (2019).  The scientific events that shaped the decade.  Nature.
  * Aghion et al., (2018) Aghion, P., Jones, B. F., and Jones, C. I. (2018).  Artificial intelligence and economic growth.  In The economics of artificial intelligence: An agenda, pages 237–282. University of Chicago Press.
  * Annoni et al., (2018) Annoni, A., Benczur, P., Bertoldi, P., Delipetrev, B., De Prato, G., Feijoo, C., Macias, E. F., Gutierrez, E. G., Portela, M. I., and Junklewitz, H. (2018).  Artificial intelligence: A european perspective.
  * Baum et al., (2021) Baum, Z. J., Yu, X., Ayala, P. Y., Zhao, Y., Watkins, S. P., and Zhou, Q. (2021).  Artificial intelligence in chemistry: current trends and future directions.  Journal of Chemical Information and Modeling, 61(7):3197–3212.
  * Bianchini et al., (2020) Bianchini, S., Müller, M., and Pelletier, P. (2020).  Deep learning in science.  arXiv preprint arXiv:2009.01575.
  * Bianchini et al., (2022) Bianchini, S., Müller, M., and Pelletier, P. (2022).  Artificial intelligence in science: An emerging general method of invention.  Research Policy, 51(10):104604.
  * Blondel et al., (2008) Blondel, V. D., Guillaume, J.-L., Lambiotte, R., and Lefebvre, E. (2008).  Fast unfolding of communities in large networks.  Journal of statistical mechanics: theory and experiment, 2008(10):P10008.
  * Cockburn et al., (2018) Cockburn, I. M., Henderson, R., and Stern, S. (2018).  The impact of artificial intelligence on innovation: An exploratory analysis.  In The economics of artificial intelligence: An agenda, pages 115–146. University of Chicago Press.
  * Färber, (2019) Färber, M. (2019).  The microsoft academic knowledge graph: A linked data source with 8 billion triples of scholarly data.  In International semantic web conference, pages 113–129. Springer.
  * Färber and Ao, (2022) Färber, M. and Ao, L. (2022).  The microsoft academic knowledge graph enhanced: Author name disambiguation, publication classification, and embeddings.  Quantitative Science Studies, 3(1):51–98.
  * Frank et al., (2019) Frank, M. R., Wang, D., Cebrian, M., and Rahwan, I. (2019).  The evolution of citation graphs in artificial intelligence research.  Nature Machine Intelligence, 1(2):79–85.
  * Gargiulo et al., (2016) Gargiulo, F., Caen, A., Lambiotte, R., and Carletti, T. (2016).  The classical origin of modern mathematics.  EPJ Data Science, 5(1):26.
  * Kauffman, (2000) Kauffman, S. A. (2000).  Investigations.  Oxford University Press.
  * King et al., (2009) King, R. D., Rowland, J., Oliver, S. G., Young, M., Aubrey, W., Byrne, E., Liakata, M., Markham, M., Pir, P., Soldatova, L. N., et al. (2009).  The automation of science.  Science, 324(5923):85–89.
  * Kitchin, (2014) Kitchin, R. (2014).  Big data, new epistemologies and paradigm shifts.  Big Data & Society, 1(1):1–12.
  * Li Vigni, (2021) Li Vigni, F. (2021).  Complexity sciences: A scientific platform.  Science & Technology Studies, 34(4):30–55.
  * McCarthy, (1981) McCarthy, J. (1981).  Epistemological problems of artificial intelligence.  In Readings in artificial intelligence, pages 459–465. Elsevier.
  * McCarthy, (2004) McCarthy, J. (2004).  What is artificial intelligence.  URL: http://www-formal. stanford. edu/jmc/whatisai. html.
  * Monechi et al., (2017) Monechi, B., Ruiz-Serrano, A., Tria, F., and Loreto, V. (2017).  Waves of novelties in the expansion into the adjacent possible.  PloS one, 12(6):e0179303.
  * OECD, (2019) OECD (2019).  Artificial Intelligence in Society.
  * Serrano et al., (2009) Serrano, M. Á., Boguná, M., and Vespignani, A. (2009).  Extracting the multiscale backbone of complex weighted networks.  Proceedings of the national academy of sciences, 106(16):6483–6488.
  * Uzzi et al., (2013) Uzzi, B., Mukherjee, S., Stringer, M., and Jones, B. (2013).  Atypical combinations and scientific impact.  Science, 342(6157):468–472.
  * WIPO, (2019) WIPO (2019).  Wipo technology trends 2019: Artificial intelligence.  Geneva: World Intellectual Property Organization.


11institutetext:  Academia Sinica, Taipei, Taiwan 22institutetext: Brno
University of Technology, Brno, Czech Republic

#  Z3-Noodler: An Automata-based String Solver
(Technical Report)

Yu-Fang Chen 11 David Chocholatý 22 Vojtěch Havlena 22
Lukáš Holík 22 Ondřej Lengál 22 Juraj Síč 22

###### Abstract

Z3-Noodler is a fork of Z3 that replaces its string theory solver with a
custom solver implementing the recently introduced stabilization-based
algorithm for solving word equations with regular constraints. An extensive
experimental evaluation shows that Z3-Noodler is a fully-fledged solver that
can compete with state-of-the-art solvers, surpassing them by far on many
benchmarks. Moreover, it is often complementary to other solvers, making it a
suitable choice as a candidate to a solver portfolio.

##  1 Introduction

Recently, many tools for solving string constraints have been developed,
motivated mainly by techniques for finding security vulnerabilities such as
SQL injection or cross-site scripting (XSS) in web applications [33, 34, 35].
String solving has also found its applications in, e.g., analysis of access
user policies in Amazon Web Services [25, 8, 38] or smart contracts [7].
Solvers for string constraints are usually implemented as string theory
solvers inside SMT solvers, such as cvc5 [9] or Z3 [30], allowing combination
with other theories, most commonly the theory of integers for string lengths.
Amonong well known string solvers other than than cvc5 and Z3 are Z3str3RE
[13, 12], Z3-Trau [1], Z3str4 [29], OSTRICH [19], and there are many more.

In this paper, we present Z3-Noodler 1.0.0 [46], a fork of Z3 4.12.2 where the
string theory solver is replaced with the _stabilization-based procedure_ for
solving string (dis)equations with regular and length constraints [14, 20].
The procedure makes heavy use of _nondeterministic finite automata_ (NFAs) and
operations over them, for which we use the efficient Mata library for NFAs
[22, 28].

The presented version implements multiple improvements over a previous
Z3-Noodler prototype from [20]. Firstly, it extends the support for string
predicates from the SMT-LIB string theory standard [11] by (1) applying
smarter and more specific axiom saturation and (2) adding support for their
solving inside the decision procedure (e.g., for the $\neg\texttt{contains}$
predicate). It also implements various optimizations (e.g., for regular
constraints handling) and other decision procedures, e.g., the _Nielsen
transformation_ [31] for quadratic equations or a procedure for regular
language (dis)equations; moreover, we added heuristics for choosing the best
decision procedure to use.

We compared Z3-Noodler with other string solvers on standard SMT-LIB
benchmarks [10, 41, 42]. The results indicate that Z3-Noodler is competitive,
superior especially on benchmarks containing mostly regular constraints and
word (dis)equations, and that the improvements since [20] had a large impact
on the number of solved instances as well as its overall performance.

##  2 Architecture

Z3-Noodler replaces the string theory solver in the DPLL(T)-based SMT solver
Z3 [30] (version 4.12.2) by our solver Noodler [14], which is based on the
_stabilization algorithm_ (cf. Section 3). DPLL(T)-based solvers in general
combine a SAT solver providing satisfying assignments to the Boolean skeleton
of a formula with multiple theory solvers for checking conjunctions of theory
literals.

Z3-Noodler still uses the infrastructure of Z3, most importantly the parser,
string theory rewriter and the _linear integer arithmetic_ (LIA) solver. The
Z3 parser takes formulae in the SMT-LIB format [10], where Z3-Noodler can
handle nearly all predicates/functions (such as substr, len, and , replace,
regular membership, word equations, etc.) in the string theory as defined by
SMT-LIB [11]. See Appendix 0.A for a definition of the fragment that we
support.

Even though we do use the string theory rewriter of Z3, we disabled those
rewritings that do not benefit our core string solver. For instance, we
removed rules that rewrite regular membership constraints to other types of
constraints since solving regular constraints and word equations using our
stabilization-based approach is efficient.

Noodler string theory LIA solver instance Mata LIA solver core string rewriter
SMT string formula1243Z3

Figure 1: Architecture of Z3-Noodler

The interaction of the Noodler solver with Z3 is shown in Fig. 1 and works as
follows. Upon receiving a satisfying Boolean assignment from the SAT solver (
1), we first remove irrelevant assignments (using Z3’s relevancy propagation),
which allows us to work with smaller instances and return more general theory
lemmas. An assignment consists of string (dis)equations, regular constraints,
and, possibly, predicates that were not _axiom-saturated_ before (cf. Section
3).

The core Noodler string decision procedure then reduces the conjunction of
string literals to a LIA constraint over string lengths, and returns it to Z3
as a theory lemma ( 2), to be solved together with the rest of the input
arithmetic constraints by Z3’s internal LIA solver. Noodler implements a
couple of decision procedures (discussed in Section 3), heavily employing the
Mata automata library (version 0.109.0) [28] ( 3). As an optimization of the
theory lemma generation, when the string constraint reduces into a disjunction
of LIA length constraints, we check the satisfiability of individual disjuncts
(generated lazily on demand) separately in order to get a positive answer as
soon as possible. For testing the disjuncts, the current solver context is
cloned and queried about satisfiability of the LIA constraint conjoined with
the disjunct ( 4).

##  3 String Theory Core

In this section, we provide details about Z3-Noodler’s string theory
implementation.

### Axiom Saturation.

In order to best utilize the power of Z3’s internal LIA solver during the
generation of a satisfiable assignment, we saturate the input formula with
length-aware theory axioms and axioms for string predicates (this happens
during Z3’s processing of the input formula, before the main SAT solver starts
generating assignments). We can then avoid checking SAT assignments that
trivially violate length conditions. Most importantly, we add length axioms
$\texttt{len}(t_{1})\geq 0$,
$\texttt{len}(t_{1}.t_{2})=\texttt{len}(t_{1})+\texttt{len}(t_{2})$ where
$t_{1},t_{2}$ are arbitrary string terms, and
$\texttt{len}(t_{1})=\texttt{len}(t_{2})$ for the word equation $t_{1}=t_{2}$.

Moreover, for string functions/predicates, Noodler saturates the original
formula with an equivalent formula composed of word (dis)equations and
length/regular constraints, which are more suitable for our core procedure
(e.g., for $\neg\texttt{contains}(s,\texttt{"abc"})$ in the input formula, we
add the regular constraint $s\notin\Sigma^{*}\texttt{abc}\Sigma^{*}$). We use
different saturation rules for instances of predicates with concrete values.
For instance, for $\texttt{substr}(s,\texttt{4},\texttt{1})$, we add just the
formula $\and(s,\texttt{4})$. On the other hand, for
$\texttt{substr}(s,t_{i},t_{j})$, where $s$ is a string term and $t_{i},t_{j}$
are general integer terms (possibly containing variables), we need to add a
more general formula talking about the prefix and suffix of $s$ of given
lengths. The original predicate occurrence is then removed from received
assignments by Noodler (Z3 does not allow to remove parts of the original
formula).

### Decision Procedures.

Z3-Noodler’s string theory core contains several complementary decision
procedures. The main one is the _stabilization-based_ algorithm for solving
word equations with regular constraints introduced in [14] and later extended
with efficient handling of length constraints and disequations [20]. The
stabilization-based algorithm starts, for every string variable, with an NFA
encoding regular constraints on the variable and iteratively refines the NFA
according to the word equations until the stability condition is achieved. The
stability condition holds when, for every word equation, the language of the
left-hand side (obtained as the language of the concatenation of NFAs for
variables and string literals) equals the language of the right-hand side.
When stability is achieved, length constraints of the solutions are generated
and passed to the LIA solver. The algorithm is complete for the _chain-free_
[5] combinations of equations, regular and length constraints, together with
unrestricted disequations, making it the largest known decidable fragment of
these types of constraints.

The stabilization-based decision procedure starts by inductively converting
the initial regular constraints into NFAs. During the construction, we utilize
eager simulation-based reduction [16, 17] with on-demand determinization and
minimization. In particular, if the regular expression contains complement, we
try to keep the automata from the corresponding regex subtrees in the form of
minimal deterministic automata.

For an efficient handling of _quadratic_ equations (systems of equations with
at most two occurrences of each variable) with lengths, Noodler implements a
decision procedure based on the _Nielsen transformation_ [31]. The algorithm
constructs a graph corresponding to the system and reasons about it to
determine if the input formula is satisfiable or not [37, 21]. If the system
contains length variables, we also create a counter automaton corresponding to
the Nielsen graph (in a similar way as in [27]). In the subsequent step, we
contract edges, saturating the set of self-loops and, finally, we iteratively
generate flat counter sub-automata (a flat counter automaton only allows
cycles that are self-loops), which are later transformed into LIA formulae
describing lengths of all possible solutions (see an example in Appendix 0.B).

In order to solve _(dis)equations of regular expressions_ , we reduce the
problem to reasoning about the corresponding NFAs (similarly as for regular
constraints handling). In particular, we use efficient NFA equivalence and
universality checking from Mata, which implements advanced antichain-based
algorithms [45, 6].

### Preprocessing.

Each decision procedure employs a sequence of preprocessing rules transforming
the string constraint to a more suitable form. Our portfolio of rules includes
transformations reducing the number of equations by a conversion to regular
constraints, propagating epsilons and variables over equations,
underapproximation rules, and rules reducing the number of disequations (cf.
[20]). On top of that, Z3-Noodler employs information about length-equivalent
variables allowing to infer simpler constraints (e.g., for $xy=zw$ with
$\texttt{len}(x)=\texttt{len}(z)$, we can infer $y=w$). Z3-Noodler also checks
for simple unsatisfiable patterns for early termination. A sequence of
preprocessing rules is composed for each of the decision procedures
differently, maximizing their strengths.

### Supported String Predicates and Limitations.

Z3-Noodler currently supports handling of basic string predicates replace,
substr, and , indexof, prefix, suffix, contains, and a limited support for
$\neg\texttt{contains}$. From the extended constraints, the core solver
currently does not support the replace_all function (and variants of
replacement based on regular expressions) and to/from_int conversions. The
decision procedures used in Z3-Noodler make it complete for the chain-free
fragment with unbounded disequations and regular constraints [20] (and for SAT
assignments when if constraints are added), and quadratic equations. Outside
this fragment, our theory core is sound but incomplete.

##  4 Experiments

### Tools and environment.

We compared Z3-Noodler with the following state-of-the-art tools: cvc5 [9]
(version 1.0.8), Z3 [30] (version 4.12.2), Z3str3RE [13, 12], Z3str4 [29],
OSTRICH [19]111Latest commit 70d01e2d2, run with -portfolio=strings option.,
and Z3-Noodlerpr (version 0.1.0 used in [20]). We did not compare with Z3-Trau
[2] as it is no longer under active development and gives incorrect results on
newer benchmarks. The experiments were executed on a workstation with an Intel
Xeon Silver 4314 CPU @ 2.4 GHz with 128 GiB of RAM running Debian GNU/Linux.
The timeout was set to 120 s, memory limit was set to 8 GiB.

### Benchmarks.

The benchmarks come from the SMT-LIB [10] repository, specifically categories
QF_S [41] and QF_SLIA [42]. These benchmarks were also used in SMT-COMP’23
[40], in which Z3-Noodler participated (version 0.2.0). As Z3-Noodler does not
support to/from_int conversions and replace_all-like predicates, we excluded
formulae whose satisfiability checking needs their support. Based on the
occurrences of different kinds of constraints, we divide the benchmarks into
three groups:

Regex

This category contains formulae with dominating regular membership and length
constraints. It consists of AutomatArk [13], Denghang, StringFuzz [15], and
Sygus-qgen benchmark sets. We excluded 1,568 formulae from StringFuzz that
require support of the to_int predicate.

Equations

The formulae in this category consist mostly of word equations with length
constraints and a small amount of other predicates. It contains Kaluza [39,
26], Kepler [24], Norn [3, 4], Slent [43], Slog [44], Webapp, and Woorpje [23]
benchmark sets. We excluded 414 formulae from Webapp that require support of
replace_all, replace_re, and replace_re_all predicates.

Predicates-small

Although Z3-Noodler focuses mainly on word equations with length and regular
constraints, the evaluation includes also a group consisting of smaller
formulae that use string predicates such as substr, and , contains, etc. It is
formed from FullStrInt, LeetCode, and StrSmallRw [32] benchmark sets. We
removed 5,509 formulae containing the to/from_int predicates from FullStrInt
and StrSmallRw.

We also consider the PyEx [36] benchmark, which we do not put into any of
these groups, as it contains large formulae with complex predicates (substr,
contains, etc.). We note that we omit the small Transducer+ [18] benchmark
because it contains exclusively formulae with replace_all.

Table 1:  Results of experiments on all benchmark sets. For each tool and
benchmark set (as well as whole groups under $\Sigma$), we give the number of
unsolved instances. Results for tools with the highest number of solved
instances are in bold. Numbers with ∗ contain also incorrect results.

| Regex | Equations | Predicates-small |
---|---|---|---|---
| Aut | Den | StrFuzz | Syg | $\Sigma$ | Kal | Kep | Norn | Slent | Slog | Web | Woo | $\Sigma$ | StrInt | Leet | StrSm | $\Sigma$ | PyEx
_Included_ | 15,995 | 999 | 10,050 | 343 | 27,387 | 19,432 | 587 | 1,027 | 1,128 | 1,976 | 267 | 809 | 25,226 | 11,669 | 2,652 | 1,670 | 15,991 | 23,845
_Unsupported_ | 0 | 0 | 1,568 | 0 | 1,568 | 0 | 0 | 0 | 0 | 0 | 414 | 0 | 414 | 5,299 | 0 | 210 | 5,509 | 0
Z3-Noodler | 62 | 0 | 0 | 0 | 62 | 259 | 4 | 0 | 5 | 0 | 0 | 243 | 511 | 4 | 4 | 55 | 63 | 4,424
cvc5 | 94 | 18 | 1037 | 0 | 1149 | 0 | 240 | 85 | 22 | 0 | 40 | 54 | 441 | 0 | 0 | 4 | 4 | 34
Z3 | 113 | 118 | 340 | 0 | 571 | 164 | 313 | 124 | 74 | 71 | 61 | 25 | 832 | 4 | 0 | 32 | 36 | 1,071
Z3str4 | 60 | 4 | 27 | 0 | 91 | 174 | 254 | 73 | 73 | 16 | 62 | 78 | 730 | 5 | 4 | 37 | 46 | 570
OSTRICH | 55 | 15 | 229 | 0 | 299 | 288 | 387 | 1 | 130 | 7 | 65 | 53 | 931 | 37 | 26 |  ∗106 |  ∗169 | 12,290
Z3str3RE | 66 | 27 |  ∗143 | 1 |  ∗237 |  ∗144 | 311 | 133 | 87 | 55 |  ∗104 |  ∗118 |  ∗952 | 64 | 192 |  ∗179 |  ∗435 | 17,764
Z3-Noodlerpr | 86 | 1 |  ∗1,014 | 0 |  ∗1,101 | 508 | 575 | 0 | 6 | 0 |  ∗3 | 256 |  ∗1,348 | 40 | 29 |  ∗493 |  ∗562 |  ∗13,362

### Results.

Table 2: Average run times (in seconds) of solved instances and their standard
deviations.

| Reg | Eq | Pred
---|---|---|---
| avg | std | avg | std | avg | std
Z3-Noodler | 0.11 | 1.35 | 0.11 | 2.13 | 0.11 | 2.16
cvc5 | 1.17 | 8.51 | 0.11 | 2.15 | 0.03 | 0.15
Z3 | 1.92 | 9.71 | 0.18 | 2.83 | 0.04 | 0.42
Z3str4 | 0.35 | 2.00 | 0.25 | 3.40 | 0.02 | 0.31
OSTRICH | 4.29 | 8.67 | 4.28 | 9.28 | 12.71 | 15.08
Z3str3RE | 0.31 | 3.28 | 0.13 | 2.72 | 0.01 | 0.08
Z3-Noodlerpr | 0.27 | 2.86 | 0.12 | 2.93 | 0.09 | 1.69

We show the number of unsolved instances for each benchmark and tool (as well
as whole groups) in Table 1. Some tools gave incorrect results (determined by
comparing to the output of cvc5 and Z3) for some benchmarks. Usually, this was
less than 10 instances, except for Z3str3RE on StringFuzz and StrSmallRw (50
and 12 incorrect results respectively) and Z3-Noodlerpr on StrSmallRw (218
incorrect results). Table 2 then shows the average run times and their
standard deviations for solved instances for each category and tool.

The results show that Z3-Noodler outperforms other tools on the Regex group
(in particular on Denghang, StringFuzz, and Sygus-qgen) both in the number of
solved instances and the average run time. Only on AutomatArk it cannot solve
the most formulae (but it solves only 7 less than the winner OSTRICH, while
being much faster).

On the Equations group, Z3-Noodler also outperforms other tools on most of the
benchmarks. In particular on Kepler, Norn, Slent, Slog, and Webapp. On Kaluza,
it is outperformed by other tools, but it still solves the vast majority of
formulae. Z3-Noodler has worse performance on Woorpje, which seems to be a
synthetic benchmark generated to showcase the strength of a specialized
algorithm [23] (this benchmark is the reason for Z3-Noodler taking the second
place in the whole group). With 0.11 s, Z3-Noodler and cvc5 have the lowest
average run time.

The winner of Predicates-small is cvc5\. In particular, on FullStrInt and
LeetCode the difference with Z3-Noodler is equally 4 instances and on
StrSmallRw the difference is 51 cases. The average time of Z3-Noodler is also
a bit higher, with 0.11 s for Z3-Noodler compared to the 0.03 s for cvc5\.
Similarly, Z3-Noodler is outperformed by cvc5, Z3, and Z3str4 on PyEx. Indeed,
we have not optimized Z3-Noodler for formulae with large numbers of predicates
yet. The results of Z3-Noodler could, however, be further improved by proper
axiom saturation for predicates or lazy predicate evaluation.

Table 3: Evaluating solver contribution to a portfolio. Times are in seconds.

| Regex | Equations
---|---|---
| Unsolved | Time | Unsolved |  Time
VBS+ | 1 | 427 | 19 | 1,304
VBS+\- Z3-Noodler | 1 | 2,914 | 131 | 6,830
VBS+\- cvc5 | 1 | 549 | 145 | 1,401
VBS+\- Z3 | 1 | 430 | 29 | 1,579
VBS+\- Z3str4 | 1 | 473 | 19 | 1,416
VBS+\- OSTRICH | 1 | 427 | 21 | 1,270
VBS+\- Z3str3RE | 1 | 510 | 20 | 1,307
cvc5 + Z3 \+ Z3-Noodler | 1 | 608 | 22 | 1,471
cvc5 + Z3 | 278 | 27,916 | 303 | 2,805

(a) Z3-Noodler vs. cvc5

(b) Z3-Noodler vs. Z3

(c) Z3-Noodler vs. VBS

Figure 2:  Comparison of Z3-Noodler with cvc5, Z3, and the virtual best solver
(VBS). Times are in seconds, axes are logarithmic. Dashed lines represent
timeouts (120 s). Colours distinguish groups:
${\color[rgb]{0.46875,0.0390625,0.765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.46875,0.0390625,0.765625}\bullet}$
Regex,
${\color[rgb]{0.76171875,0.46484375,0.03515625}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.46484375,0.03515625}\bullet}$
Equations, and
${\color[rgb]{0.140625,0.76171875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.76171875,0.46875}\bullet}$
Predicates-small.

In Fig. 2 we show scatter plots comparing running time of Z3-Noodler with
cvc5, Z3, and virtual best solver (VBS; a solver that takes the best result
from all tools other than Z3-Noodler) on all three benchmark groups. See
Appendix 0.C for comparison with other solvers. The plots show that Z3-Noodler
outperforms the competitors on a vast number of instances, in many cases being
complementary to them. To validate this claim, we also checked how different
solvers contribute to a portfolio. That is, we took the VBS including
Z3-Noodler (VBS+) and then checked how well the portfolio works without each
of the solvers. Table 3 shows the results on the Regex and Equations groups
(we omit Predicates-small, where Z3-Noodler does not help the portfolio). The
results show that on the two groups, Z3-Noodler is the most valuable solver in
the portfolio. We also include results on the small portfolio of Z3 and cvc5
(with and without Z3-Noodler) showing that, on the two groups, using just
these three solvers is almost as good as using the whole portfolio of all
solvers.

Comparing with the older version Z3-Noodlerpr from [20], we can see that there
is a significant improvement in most benchmarks, most significantly in
AutomatArk, StringFuzz, Kepler, StrSmallRw, and Kaluza. We note that adding
more complicated algorithm selection strategies significantly improved the
overall performance of Z3-Noodler, but, on the other hand, decreased the
performance on Kaluza (cf. [20]). Better results in AutomatArk and StringFuzz
stem from the improvements in Mata and from heuristics tailored for regular
expressions handling. Including Nielsen’s algorithm [31] has the largest
impact on the Kepler benchmark. The improvement on predicate-intensive
benchmarks is caused by optimizations in axiom saturation for predicates. The
older version also had multiple bugs that have been fixed in the current
version.

## References

  * [1] Abdulla, P.A., Atig, M.F., Chen, Y., Diep, B.P., Dolby, J., Janků, P., Lin, H., Holík, L., Wu, W.: Efficient handling of string-number conversion. In: Proc. of PLDI’20. pp. 943–957. ACM (2020). https://doi.org/10.1145/3385412, https://doi.org/10.1145/3385412
  * [2] Abdulla, P.A., Atig, M.F., Chen, Y., Diep, B.P., Holík, L., Rezine, A., Rümmer, P.: Trau: SMT solver for string constraints. In: Bjørner, N.S., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018. pp. 1–5. IEEE (2018). https://doi.org/10.23919/FMCAD.2018.8602997, https://doi.org/10.23919/FMCAD.2018.8602997
  * [3] Abdulla, P.A., Atig, M.F., Chen, Y., Holík, L., Rezine, A., Rümmer, P., Stenman, J.: String constraints for verification. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8559, pp. 150–166. Springer (2014). https://doi.org/10.1007/978-3-319-08867-9_10, https://doi.org/10.1007/978-3-319-08867-9_10
  * [4] Abdulla, P.A., Atig, M.F., Chen, Y., Holík, L., Rezine, A., Rümmer, P., Stenman, J.: Norn: An SMT solver for string constraints. In: Kroening, D., Pasareanu, C.S. (eds.) Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Lecture Notes in Computer Science, vol. 9206, pp. 462–469. Springer (2015). https://doi.org/10.1007/978-3-319-21690-4_29, https://doi.org/10.1007/978-3-319-21690-4_29
  * [5] Abdulla, P.A., Atig, M.F., Diep, B.P., Holík, L., Janků, P.: Chain-free string constraints. In: Chen, Y., Cheng, C., Esparza, J. (eds.) Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11781, pp. 277–293. Springer (2019). https://doi.org/10.1007/978-3-030-31784-3_16, https://doi.org/10.1007/978-3-030-31784-3_16
  * [6] Abdulla, P.A., Chen, Y.F., Holík, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: TACAS’10. LNCS, vol. 6015, pp. 158–174. Springer (2010)
  * [7] Alt, L., Blicha, M., Hyvärinen, A.E.J., Sharygina, N.: SolCMC: Solidity compiler’s model checker. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13371, pp. 325–338. Springer (2022). https://doi.org/10.1007/978-3-031-13185-1_16, https://doi.org/10.1007/978-3-031-13185-1_16
  * [8] Backes, J., Bolignano, P., Cook, B., Dodge, C., Gacek, A., Luckow, K., Rungta, N., Tkachuk, O., Varming, C.: Semantic-based automated reasoning for aws access policies using smt. In: 2018 Formal Methods in Computer Aided Design (FMCAD). pp. 1–9 (2018). https://doi.org/10.23919/FMCAD.2018.8602994
  * [9] Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial-strength smt solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 415–442. Springer International Publishing, Cham (2022)
  * [10] Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)
  * [11] Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB): Strings. https://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml (2023)
  * [12] Berzish, M., Day, J.D., Ganesh, V., Kulczynski, M., Manea, F., Mora, F., Nowotka, D.: Towards more efficient methods for solving regular-expression heavy string constraints. Theor. Comput. Sci. 943, 50–72 (2023). https://doi.org/10.1016/j.tcs.2022.12.009, https://doi.org/10.1016/j.tcs.2022.12.009
  * [13] Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J.D., Nowotka, D., Ganesh, V.: An SMT solver for regular expressions and linear arithmetic over string length. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12760, pp. 289–312. Springer (2021). https://doi.org/10.1007/978-3-030-81688-9_14, https://doi.org/10.1007/978-3-030-81688-9_14
  * [14] Blahoudek, F., Chen, Y.F., Chocholatý, D., Havlena, V., Holík, L., Lengál, O., Síč, J.: Word equations in synergy with regular constraints. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) Formal Methods. pp. 403–423. Springer International Publishing, Cham (2023)
  * [15] Blotsky, D., Mora, F., Berzish, M., Zheng, Y., Kabir, I., Ganesh, V.: StringFuzz: A fuzzer for string solvers. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification. pp. 45–51. Springer International Publishing, Cham (2018)
  * [16] Bustan, D., Grumberg, O.: Simulation based minimization. In: Proceedings of CADE-17. LNCS, vol. 1831, pp. 255–270. Springer (2000)
  * [17] Cécé, G.: Foundation for a series of efficient simulation algorithms. In: LICS’17. pp. 1–12. IEEE Computer Society (2017)
  * [18] Chen, T., Hague, M., He, J., Hu, D., Lin, A.W., Rümmer, P., Wu, Z.: A decision procedure for path feasibility of string manipulating programs with integer data type. In: Hung, D.V., Sokolsky, O. (eds.) Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12302, pp. 325–342. Springer (2020). https://doi.org/10.1007/978-3-030-59152-6_18, https://doi.org/10.1007/978-3-030-59152-6_18
  * [19] Chen, T., Hague, M., Lin, A.W., Rümmer, P., Wu, Z.: Decision procedures for path feasibility of string-manipulating programs with complex operations. Proc. ACM Program. Lang. 3(POPL), 49:1–49:30 (2019). https://doi.org/10.1145/3290362, https://doi.org/10.1145/3290362
  * [20] Chen, Y.F., Chocholatý, D., Havlena, V., Holík, L., Lengál, O., Síč, J.: Solving string constraints with lengths by stabilization. Proc. ACM Program. Lang. 7(OOPSLA2) (oct 2023). https://doi.org/10.1145/3622872
  * [21] Chen, Y.F., Havlena, V., Lengál, O., Turrini, A.: A symbolic algorithm for the case-split rule in solving word constraints with extensions. Journal of Systems and Software 201, 111673 (2023). https://doi.org/https://doi.org/10.1016/j.jss.2023.111673, https://www.sciencedirect.com/science/article/pii/S0164121223000687
  * [22] Chocholatý, D., Fiedor, T., Havlena, V., Holík, L., Hruška, M., Lengál, O., Síč, J.: Mata: A fast and simple finite automata library (technical report). CoRR abs/2310.10136 (2023). https://doi.org/10.48550/arXiv.2310.10136, https://doi.org/10.48550/arXiv.2310.10136
  * [23] Day, J.D., Ehlers, T., Kulczynski, M., Manea, F., Nowotka, D., Poulsen, D.B.: On solving word equations using SAT. In: Filiot, E., Jungers, R.M., Potapov, I. (eds.) Reachability Problems - 13th International Conference, RP 2019, Brussels, Belgium, September 11-13, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11674, pp. 93–106. Springer (2019). https://doi.org/10.1007/978-3-030-30806-3_8, https://doi.org/10.1007/978-3-030-30806-3_8
  * [24] Le, Q.L., He, M.: A decision procedure for string logic with quadratic equations, regular expressions and length constraints. In: Ryu, S. (ed.) Programming Languages and Systems. pp. 350–372. Springer International Publishing, Cham (2018)
  * [25] Liana Hadarean: String solving at Amazon. https://mosca19.github.io/program/index.html (2019), presented at MOSCA’19
  * [26] Liang, T., Reynolds, A., Tsiskaridze, N., Tinelli, C., Barrett, C., Deters, M.: An efficient SMT solver for string constraints. Formal Methods in System Design 48(3), 206–234 (2016)
  * [27] Lin, A.W., Majumdar, R.: Quadratic word equations with length constraints, counter systems, and presburger arithmetic with divisibility. In: Automated Technology for Verification and Analysis. pp. 352–369. Springer International Publishing, Cham (2018)
  * [28] Mata: An efficient automata library (2023), https://github.com/VeriFIT/mata
  * [29] Mora, F., Berzish, M., Kulczynski, M., Nowotka, D., Ganesh, V.: Z3str4: A multi-armed string solver. In: Huisman, M., Pasareanu, C.S., Zhan, N. (eds.) Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings. Lecture Notes in Computer Science, vol. 13047, pp. 389–406. Springer (2021). https://doi.org/10.1007/978-3-030-90870-6_21, https://doi.org/10.1007/978-3-030-90870-6_21
  * [30] de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS’08. LNCS, vol. 4963, pp. 337–340. Springer (2008), https://doi.org/10.1007/978-3-540-78800-3_24
  * [31] Nielsen, J.: Die isomorphismen der allgemeinen, unendlichen gruppe mit zwei erzeugenden. Mathematische Annalen 78(1), 385–397 (1917)
  * [32] Nötzli, A., Reynolds, A., Barbosa, H., Niemetz, A., Preiner, M., Barrett, C., Tinelli, C.: Syntax-guided rewrite rule enumeration for SMT solvers. In: Janota, M., Lynce, I. (eds.) Theory and Applications of Satisfiability Testing – SAT 2019. pp. 279–297. Springer International Publishing, Cham (2019)
  * [33] OWASP: Top 10. https://www.owasp.org/images/f/f8/OWASP_Top_10_-_2013.pdf (2013)
  * [34] OWASP: Top 10. https://owasp.org/www-project-top-ten/2017/ (2017)
  * [35] OWASP: Top 10. https://owasp.org/Top10/ (2021)
  * [36] Reynolds, A., Woo, M., Barrett, C., Brumley, D., Liang, T., Tinelli, C.: Scaling up DPLL(T) string solvers using context-dependent simplification. In: Majumdar, R., Kunčak, V. (eds.) Computer Aided Verification. pp. 453–474. Springer International Publishing, Cham (2017)
  * [37] Robson, J.M., Diekert, V.: On quadratic word equations. In: Annual Symposium on Theoretical Aspects of Computer Science. pp. 217–226. Springer (1999)
  * [38] Rungta, N.: A billion SMT queries a day (invited paper). In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13371, pp. 3–18. Springer (2022). https://doi.org/10.1007/978-3-031-13185-1_1, https://doi.org/10.1007/978-3-031-13185-1_1
  * [39] Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: Kaluza web site (2023), https://webblaze.cs.berkeley.edu/2010/kaluza/
  * [40] SMT-COMP’23: https://smt-comp.github.io/2023/ (2023)
  * [41] SMT-LIB: https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_S (2023)
  * [42] SMT-LIB: https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_SLIA (2023)
  * [43] Wang, H.E., Chen, S.Y., Yu, F., Jiang, J.H.R.: A symbolic model checking approach to the analysis of string and length constraints. In: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering. p. 623–633. ASE 2018, Association for Computing Machinery, New York, NY, USA (2018). https://doi.org/10.1145/3238147.3238189, https://doi.org/10.1145/3238147.3238189
  * [44] Wang, H., Tsai, T., Lin, C., Yu, F., Jiang, J.R.: String analysis via automata manipulation with logic circuit representation. In: CAV’16. LNCS, vol. 9779, pp. 241–260. Springer (2016)
  * [45] Wulf, M.D., Doyen, L., Henzinger, T.A., Raskin, J.: Antichains: A new algorithm for checking universality of finite automata. In: CAV’06. LNCS, vol. 4144, pp. 17–30. Springer (2006)
  * [46] Z3-Noodler: Automata-based string solver (2023), https://github.com/VeriFIT/z3-noodler

##  Appendix 0.A Logic of Strings

Let $\Sigma$ be a finite alphabet. We use $\Sigma^{*}$ to denote the set of
all finite words over $\Sigma$. In Z3-Noodler, we consider the logic of
strings over $\Sigma$, a set of string variables $\mathbb{X}_{s}$ ranging over
$\Sigma^{*}$, and a set of integer variables $\mathbb{X}_{i}$ ranging over
$\mathbb{Z}$, with the syntax of a formula $\varphi$ given using the following
grammar:

$\displaystyle\varphi$
$\displaystyle:=\varphi_{i}\mid\varphi_{s}\mid\varphi\wedge\varphi\mid\neg\varphi$
$\displaystyle\varphi_{s}$ $\displaystyle:=t_{s}=t_{s}\mid
t_{s}\in\mathcal{R}\mid\mathcal{R}=\mathcal{R}\mid\texttt{contains}(t_{s},t_{s})\mid\texttt{prefix}(t_{s},t_{s})\mid\texttt{suffix}(t_{s},t_{s})$
$\displaystyle\varphi_{i}$ $\displaystyle:=t_{i}\leq t_{i}$ $\displaystyle
t_{s}$ $\displaystyle:=v_{s}\mid w\mid t_{s}\cdot
t_{s}\mid\texttt{substr}(t_{s},t_{i},t_{i})\mid\and(t_{s},t_{i})\mid\texttt{replace}(t_{s},t_{s},t_{s})$
$\displaystyle t_{i}$ $\displaystyle:=v_{i}\mid k\mid t_{i}\cdot
t_{i}\mid\texttt{len}(t_{s})\mid\texttt{indexof}(t_{s},t_{s})$

with $\mathcal{R}$ is a regular language, $v_{s}\in\mathbb{X}_{s}$,
$w\in\Sigma^{*}$, $v_{i}\in\mathbb{X}_{i}$, and $k\in\mathbb{Z}$. Here, a
string atomic formula $\varphi_{s}$ is given as either an equation of string
terms $t_{s}$, a regular constraint checking whether the value of a string
term belongs to a regular language (specified by an extended regular
expression222I.e., regular expressions enriched with operators for
intersection and complement.), regex equality, or application of predicates
contains, prefix, and suffix. String terms are then concatenations of strings
and variables extended by string predicates substr, $\and$, and replace. A
length atomic formula is given as a  _linear integer arithmetic_ atomic
formula with terms containing also $\texttt{len}(t_{s})$ denoting the length
of $t_{s}$ and application of indexof. We consider the usual semantics of the
predicates as defined by SMT-LIB [11].

##  Appendix 0.B Example of Nielsen Transformation

$xy=ax$$y=a$$y=\epsilon$$\epsilon=\epsilon$${x}\hookrightarrow{ax}$${x}\hookrightarrow{\epsilon}$${y}\hookrightarrow{ay}$${y}\hookrightarrow{\epsilon}$
(a)

$x:=x+1$$x:=0$$y:=y+1$$y:=0$ (b)

Figure 3:  Example of Nielsen graph and the corresponding counter system.

Consider the quadratic equation $xy=ax$ with the corresponding Nielsen graph
Fig. 3(a) (redundant nodes are omitted). The Nielsen graph is derived from the
initial equation $yx=ax$ by application of rewriting rules and trimming the
common prefix. For instance if we apply the substitution
${y}\hookrightarrow{ay}$ on the node $y=a$, we get $ay=a$ yielding to
$y=\epsilon$. The counter system corresponding to the Nielsen graph is shown
in Fig. 3(b). Since the system is flat, the length formula describing lengths
of $x$ and $y$ is given as $\varphi(x,y)=\exists
y_{0},y_{1},x_{0},x_{1}:y_{0}=0\wedge y_{1}=y_{0}+1\wedge
x_{0}=0\wedge(\exists k:k\geq 0\wedge x_{1}=x_{0}+k)\wedge x_{1}=x\wedge
y_{1}=y$, which is equivalent to $y=1\wedge x\geq 0$.

##  Appendix 0.C Detailed Results

(a) Z3-Noodler vs. cvc5

(b) Z3-Noodler vs. Z3

(c) Z3-Noodler vs. Z3str4

(d) Z3-Noodler vs. OSTRICH

(e) Z3-Noodler vs. Z3str3RE

(f) Z3-Noodler vs. Z3-Noodlerpr

Figure 4:  Comparison of Z3-Noodler with other tools on all three benchmark
categories. Times are in seconds, axes are logarithmic. Dashed lines represent
timeouts (120 s). Colors distinguish categories:
${\color[rgb]{0.46875,0.0390625,0.765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.46875,0.0390625,0.765625}\bullet}$
Regex,
${\color[rgb]{0.76171875,0.46484375,0.03515625}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.46484375,0.03515625}\bullet}$
Equations, and
${\color[rgb]{0.140625,0.76171875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.76171875,0.46875}\bullet}$
Predicates-small.

(a) Z3-Noodler vs. cvc5

(b) Z3-Noodler vs. Z3

(c) Z3-Noodler vs. Z3str4

(d) Z3-Noodler vs. OSTRICH

(e) Z3-Noodler vs. Z3str3RE

(f) Z3-Noodler vs. Z3-Noodlerpr

Figure 5:  Comparison of Z3-Noodler with other tools on PyEx benchmark. Times
are in seconds, axes are logarithmic. Dashed lines represent timeouts (120 s).
Colors distinguish categories:
${\color[rgb]{0.46875,0.0390625,0.765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.46875,0.0390625,0.765625}\bullet}$
Regex,
${\color[rgb]{0.76171875,0.46484375,0.03515625}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.46484375,0.03515625}\bullet}$
Equations, and
${\color[rgb]{0.140625,0.76171875,0.46875}\definecolor[named]{pgfstrokecolor}{rgb}{0.140625,0.76171875,0.46875}\bullet}$
Predicates-small.  Table 4: Detailed results for run times (in seconds) of the
tools and the portfolio.

| Regex | Equations | Predicates-small | PyEx
---|---|---|---|---
| Unsolved | Total time | Avg | Med | Std | Unsolved | Total time | Avg | Med | Std | Unsolved | Total time | Avg | Med | Std | Unsolved | Total time | Avg | Med | Std
Z3-Noodler | 62 | 2971.92 | 0.11 | 0.03 | 1.35 | 511 | 2603.78 | 0.11 | 0.02 | 2.13 | 63 | 1762.30 | 0.11 | 0.02 | 2.16 | 4424 | 65974.61 | 3.40 | 0.24 | 12.58
cvc5 | 1149 | 30620.78 | 1.17 | 0.02 | 8.51 | 441 | 2840.58 | 0.11 | 0.01 | 2.15 | 4 | 505.40 | 0.03 | 0.02 | 0.15 | 34 | 7665.50 | 0.32 | 0.13 | 2.59
Z3 | 571 | 51577.89 | 1.92 | 0.04 | 9.71 | 832 | 4509.83 | 0.18 | 0.02 | 2.83 | 36 | 633.79 | 0.04 | 0.03 | 0.42 | 1071 | 63069.90 | 2.77 | 0.24 | 10.54
Z3str4 | 91 | 9470.04 | 0.35 | 0.02 | 2.00 | 730 | 6002.32 | 0.25 | 0.01 | 3.40 | 46 | 291.45 | 0.02 | 0.01 | 0.31 | 570 | 33858.89 | 1.45 | 0.18 | 6.43
OSTRICH | 299 | 116317.79 | 4.29 | 2.30 | 8.67 | 931 | 104014.91 | 4.28 | 2.20 | 9.28 | 165 | 201112.88 | 12.71 | 6.73 | 15.08 | 12290 | 635163.13 | 54.97 | 45.37 | 78.76
Z3str3RE | 187 | 8349.97 | 0.31 | 0.01 | 3.28 | 937 | 3169.81 | 0.13 | 0.01 | 2.72 | 423 | 167.68 | 0.01 | 0.01 | 0.08 | 17764 | 4037.72 | 0.66 | 0.04 | 4.21
Z3-Noodlerpr | 1095 | 7004.06 | 0.27 | 0.04 | 2.86 | 1346 | 2826.53 | 0.12 | 0.02 | 2.93 | 344 | 1466.71 | 0.09 | 0.03 | 1.69 | 13356 | 31277.58 | 2.98 | 0.07 | 10.41
VBS+ | 1 | 427.01 | 0.02 | 0.01 | 0.03 | 19 | 1303.56 | 0.05 | 0.00 | 1.62 | 2 | 162.90 | 0.01 | 0.01 | 0.14 | 24 | 7292.52 | 0.31 | 0.12 | 2.54
VBS+\- Z3-Noodler | 1 | 2913.72 | 0.11 | 0.01 | 0.60 | 131 | 6829.67 | 0.27 | 0.00 | 3.97 | 2 | 166.86 | 0.01 | 0.01 | 0.14 | 24 | 7297.62 | 0.31 | 0.12 | 2.54
VBS+\- cvc5 | 1 | 548.62 | 0.02 | 0.01 | 0.07 | 145 | 1400.79 | 0.06 | 0.00 | 1.79 | 17 | 480.98 | 0.03 | 0.01 | 1.13 | 359 | 33867.84 | 1.44 | 0.17 | 6.58
VBS+\- Z3 | 1 | 429.84 | 0.02 | 0.01 | 0.03 | 29 | 1579.40 | 0.06 | 0.00 | 1.87 | 2 | 164.41 | 0.01 | 0.01 | 0.14 | 27 | 7114.44 | 0.30 | 0.12 | 2.41
VBS+\- Z3str4 | 1 | 473.03 | 0.02 | 0.01 | 0.04 | 19 | 1416.13 | 0.06 | 0.01 | 1.68 | 2 | 207.57 | 0.01 | 0.01 | 0.14 | 28 | 7638.42 | 0.32 | 0.13 | 2.65
VBS+\- OSTRICH | 1 | 427.01 | 0.02 | 0.01 | 0.03 | 21 | 1269.91 | 0.05 | 0.00 | 1.61 | 2 | 162.90 | 0.01 | 0.01 | 0.14 | 24 | 7292.52 | 0.31 | 0.12 | 2.54
VBS+\- Z3str3RE | 1 | 509.62 | 0.02 | 0.01 | 0.03 | 20 | 1306.84 | 0.05 | 0.01 | 1.50 | 2 | 215.62 | 0.01 | 0.01 | 0.14 | 24 | 7332.53 | 0.31 | 0.12 | 2.54
cvc5 + Z3 \+ Z3-Noodler | 1 | 608.48 | 0.02 | 0.01 | 0.05 | 22 | 1470.72 | 0.06 | 0.01 | 1.58 | 2 | 342.24 | 0.02 | 0.02 | 0.14 | 28 | 7715.58 | 0.32 | 0.13 | 2.65
cvc5 + Z3 | 278 | 27916.42 | 1.03 | 0.02 | 7.69 | 303 | 2805.47 | 0.11 | 0.01 | 2.25 | 2 | 396.73 | 0.02 | 0.02 | 0.15 | 28 | 7728.58 | 0.32 | 0.13 | 2.65