Chennai Mathematical Institute, India and CNRS, ReLaX, IRL 2000,
Indiaaiswarya@cmi.ac.inhttps://orcid.org/0000-0002-4878-7581 Chennai
Mathematical Institute,
Indiasoumodevmal@cmi.ac.inhttps://orcid.org/0000-0001-5054-5664 Institute of
Mathematical Sciences, HBNI, India and CNRS, ReLaX, IRL 2000,
Indiapsaivasan@imsc.res.inhttps://orcid.org/0000-0001-5060-0117MATRICS GRANT
(MTR/2022/000312) C Aiswarya, Soumodev Mal, and Prakash Saivasan [500]Theory
of computation Logic and verification This is the full version of a paper
accepted in STACS’24

###### Acknowledgements.

We thank Paul Gastin for helpful discussions.

# Satisfiability of Context-free String Constraints with Subword-ordering and
Transducers

C. Aiswarya  Soumodev Mal  Prakash Saivasan

###### Abstract

We study the satisfiability of string constraints where context-free
membership constraints may be imposed on variables. Additionally a variable
may be constrained to be a subword of a word obtained by shuffling variables
and their transductions. The satisfiability problem is known to be undecidable
even without rational transductions. It is known to be NExptime-complete
without transductions, if the subword relations between variables do not have
a cyclic dependency between them. We show that the satisfiability problem
stays decidable in this fragment even when rational transductions are added.
It is 2NExptime-complete with context-free membership, and NExptime-complete
with only regular membership. For the lower bound we prove a technical lemma
that is of independent interest: The length of the shortest word in the
intersection of a pushdown automaton (of size $\mathcal{O}(n)$) and $n$
finite-state automata (each of size $\mathcal{O}(n)$) can be double
exponential in $n$.

###### keywords:

satisfiability, subword, string constraints, context-free, transducers

###### category:

##  1 Introduction

The theory of strings has always been an important and active area of research
for long. In fact, as Hilbert notes, it is the very foundation of mathematical
logic itself [45, 24]. The recent successes in employing the theory for
practical verification has only re-iterated its importance. The study of the
theory of string constraints dates back to Tarski and Hermes [44, 32], who in
1933 provided the axiomatic foundation for it. There have been several other
advancements of string theories since then, some of the notable ones include
[24, 43, 41, 40, 42, 17]. In 1977, Makanin studied the algorithmic aspect of
the word equations (equation involving concatenation and equality) and showed
that the satisfiability problem is decidable [40]. The complexity for this
problem was improved in [42]. Despite receiving much attention, the theory of
strings has long standing unsolved open problems, indicating the intrinsic
difficult nature of the theory.

One important aspect of the study here is the satisfiability of string
constraints. The question here asks whether it is possible to assign a word to
each variable such that the given set of string constraints is satisfied. The
constraints themselves can be either relational, which relate variables or
membership, that define the domain for each variable.

In the recent years, the constraint satisfaction problem of strings (CSPS) has
received much attention from verification community due to its usefulness in
modeling and reasoning about programs. This problem has particularly been
useful in verifying web services [31] and database applications from injection
attacks [10]. In such attacks, the attacker constructs an input string in such
a way that the underlying semantics of the interpretation is changed. The
CSPS, and more importantly its implementations in solvers [38, 1, 16, 36, 37,
25, 35] have provided the much needed power to model and verify programs for
such vulnerabilities. This in turn has directed the study to explore the
boundaries of solvability.

However one impediment for this has been the theoretical limitation. For
instance, with respect to word equations, adding a transducer renders the
model undecidable. Similarly introducing membership in context free language
also renders the model undecidable (see [27], [29] for more details). Despite
this, there have been several advancements in this regard [19, 39, 33, 22, 21,
18, 5, 8, 28].

The context-free membership constraints are particularly useful feature to
have since checking vulnerabilities include checking for programs, that are
inherently context-free, masquerading as string queries. In [9], the authors
provided first such model that could handle context-free membership queries
and yet has decidability for CSPS, under some restrictions. They showed that
if every relational constraint has sub-word relation instead of equality and
assuming an _acyclicity_ restriction, the satisfaction problem is NExptime
complete. In fact, the authors in their model include a more powerful shuffle
operator against the usual concatenation. Further they show that the
complexity of the satisfiability problem when only regular membership is
involved is also the same i.e, NExptime complete. They also provide an
interesting connection of their model with lossy channel systems that include
pushdown automata.

Yet another feature in string solvers that has been much desired is that of
transductions. As noted in [33, 21], most modern applications, especially
browsers include implicit transductions that mutates the input string. To
verify such applications, one also needs the power of transductions. There
have been very few successful attempt towards decidability of string
constraints that involve transductions, some of them being [33, 8, 21, 19].

We investigate string constraints when sub-word ordering, context-free
membership and transducers are involved. Unfortunately, in its full generality
this problem is undecidable. However we show that imposing the same acyclicity
restriction as in [9] gives decidability under this setting. This extends the
decidability result of [9] to include transductions.

In [9] the satisfiability of the acyclic variant of the string constraints
without transducers was shown to be inter-reducible with the control-state
reachability problem of acyclic networks of pushdown systems communicating
over lossy fifo channels. They showed that both these problems are NExptime-
complete. In our setting, with the additional feature of transductions, we can
enrich the model of communicating pushdown to allow transductions to be sent
in the channels. Such transductions naturally model encoders such as error
correcting codes or injection of noise.

We show that, when only regular membership is allowed, adding transductions do
not alter the complexity. It is still NExptime-complete. Interestingly when
context-free membership is involved, it becomes 2NExptime-complete.

Our 2NExptimelower bound argument relies on a new technique that is of
independent interest. In fact, we show that we can count exactly $2^{2^{n}}$
using one pushdown automaton with a binary stack alphabet and 3 states, and
$n$ finite state automata each of size $\mathcal{O}(n)$. Along the way we also
show that 1) we can count exactly $2^{n}$ using a pushdown automaton with
$\mathcal{O}(n)$ states and a binary stack alphabet, and 2) we can count
exactly $2^{n}$ using $n$ finite state automata each of size $\mathcal{O}(n)$.

As an application of this, we obtain a tight bound on the size of the smallest
DFA of the downward closure, upward closure and the Parikh image closure of
the intersection language of $n$ finite state automata, each of size
$\mathcal{O}(n)$. This size is ${\Theta}(2^{n})$. Likewise, the size of the
smallest DFA of the downward, upward and Parikh image closure for the
intersection of language of $n$ finite state automata with the language of a
pushdown automaton, each of size $\mathcal{O}(n)$ is ${\Theta}(2^{2^{n}})$.

#### Related work

Apart from the work mentioned in the introduction, there are several other
work on string constraints. In [18], the authors consider word equations
equipped with replace all function and show decidability for the acyclic
fragment.

In [3], the authors develop an uniform framework to decide the satisfiability
and unsatisfiability of string constraints based on identifying patterns. In
[2], the authors consider string constraints extended with negation and show
how to solve them. In [22], the authors provide a semantic restriction on
string manipulating programs that guarantees decidability for checking path
feasibility. In [7], the authors study the problem of regular separability of
the language of two word equations. In [26], the authors compare the
expressive power of the logical theories built around word equations.

In [33], word equations with equality, transducers and regular membership is
considered. This problem in full generality is immediately undecidable. The
authors consider a straight line fragment and show that the satisfiability
problem is Expspace complete. In [22], the authors investigated the
decidability of string constraints in the presence of regular membership
constraints, replaceAll operator involving regular expressions and straight
line restriction. In [20], the authors consider a stronger match and replace
operator and show decidability. In [8], word equations with equality,
transducers, length constraints and regular membership is considered and a
chain free fragment of it was shown to be decidable. The authors show that the
chain-free fragment of the satisfiability problem in this setting is
decidable.

All of these work consider word equation (uses equality for comparison) in the
model, our work uses subword ordering as the comparison operator. Further
more, none of the work mentioned above considers context free membership
constraints. In [9], subword ordering and context free membership is
considered, where as it does not include transductions.

Apart from these, there are several approaches which attempts to solve the
problem from a practical perspective, some of them being [4, 6, 2, 5, 16, 15,
33].

##  2 Preliminaries

####  Sets, Multisets, Functions

We denote the set of natural number $\\{1,2,\dots\\}$ by $\mathbb{N}$. For
$n\in\mathbb{N}$, we denote by $[n]$ the set of natural numbers up to $n$:
$\\{1,2,\dots,n\\}$. Let $\mathbb{N}_{0}$ denote the set $\\{0,1,2,\dots\\}$.
That is, $\mathbb{N}_{0}=\\{0\\}\cup\mathbb{N}$.

Let $S$ be any set. A multiset $X$ of $S$ assigns a multiplicity
$X(s)\in\mathbb{N}_{0}$ to each element $s\in S$. We say that $s\in X$ if
$X(s)>0$. For a usual subset $X$, the multiplicity $X(s)\in\\{0,1\\}$. A
multiset $X$ may also be written as
$\\{\\!\\!\\{s_{1},s_{2},\dots\\}\\!\\!\\}$, by listing each element $s$,
$X(s)$ many times. The set of all multisets of $S$ is denoted
$\mathbb{N}_{0}^{S}$, and the set of all usual subsets of $S$ is denoted by
$2^{S}$. The size of a multiset $X$, denoted $|X|$ is the sum of the
multiplicities of the elements. That is, $|X|=\sum_{s\in X}X(s)$.

####  Word, Subword, Shuffle, Projection

Let $\Sigma$ be an alphabet. $\Sigma^{\ast}$ denotes the set of all words over
$\Sigma$, $\epsilon$ denotes the empty word, and
$\Sigma_{\epsilon}=\Sigma\cup\\{\epsilon\\}$. For a word $w=a_{1}a_{2}\dots
a_{n}\in\Sigma^{\ast}$, we denote by $\textsf{len}(w)$, the length of $w$
($\textsf{len}(w)=n$) and by $w[i]$ its $i$th letter $a_{i}$. The set of
positions of $w$ is denoted $\textsf{pos}(w)$. That is,
$\textsf{pos}(w)=[\textsf{len}(w)]$. For $Y\subseteq\textsf{pos}(w)$, we
denote by ${w}_{\downarrow{Y}}$ the projection of $w$ to the positions in $Y$.
If $Y=\\{i_{1},i_{2},\dots i_{m}\\}$ with $0<i_{1}<i_{2}<\dots<i_{m}\leq n$,
then ${w}_{\downarrow{Y}}=a_{i_{1}}a_{i_{2}}\dots a_{i_{m}}$. For
$u,v\in\Sigma^{\ast}$, we say $u$ is a (scattered) subword of $v$, denoted
$u\preceq v$, if there is $Y\subseteq\textsf{pos}(v)$ such that
$u={v}_{\downarrow{Y}}$. In this case we say $v$ is a superword of $u$. Let
$\Sigma^{\prime}\subseteq\Sigma$ be a sub-alphabet and let
$w\in\Sigma^{\ast}$. Projection of $w$ to $\Sigma^{\prime}$, denoted
${w}_{\downarrow{\Sigma^{\prime}}}$, is defined to be ${w}_{\downarrow{Y}}$
where $Y=\\{i\mid w[i]\in\Sigma^{\prime}\\}$.

Let $X$ be a finite multiset of words from $\Sigma^{\ast}$ given by
$X=\\{\\!\\!\\{w_{1},\dots w_{n}\\}\\!\\!\\}$. We define the shuffle of $X$,
denoted $\mathsf{Shuffle}(X)$ to be the set $\\{w\mid$ there are
$Y_{1},Y_{2}\dots Y_{n}\subseteq\textsf{pos}(w)$ forming a partition of
$\textsf{pos}(w)$ and $w_{i}={w}_{\downarrow{Y_{i}}}$ for all $i\in[n]\\}$.

#### Finite-state automaton, Transducers, Pushdown Automaton

A (nondeterministic) finite-state automaton (NFA) over an alphabet $\Sigma$ is
given by a tuple $A=(\textsf{States},\textsf{Trans},s_{\text{in}},F)$ where
States is the finite set of states,
$\textsf{Trans}\subseteq\textsf{States}\times\Sigma_{\epsilon}\times\textsf{States}$
is the set of transitions, $s_{\text{in}}\in\textsf{States}$ is the initial
state, and $F\subseteq\textsf{States}$ is the set of final/accepting states.
We write $s\xrightarrow{t}s^{\prime}$ for some $t\in\textsf{Trans}$ if $t$ is
of the form $(s,a,s^{\prime})$. Define the homomorphism
$\textsf{label}:\textsf{Trans}^{\ast}\to\Sigma^{\ast}$ given by
$\textsf{label}((s,a,s^{\prime}))=a$. The language of an NFA $A$, denoted
$L(A)$ is given by $L(A)=\\{w\mid w=\textsf{label}(t_{1}t_{2}\dots t_{n})$ and
$s_{\text{in}}\xrightarrow{t_{1}}s_{1}\xrightarrow{t_{2}}s_{2}\dots
s_{n-1}\xrightarrow{t_{n}}s_{n}$ with $s_{n}\in F\\}$.

A transducer from $\Sigma^{\ast}$ to $\Sigma^{\ast}$ is a tuple
$T=(\textsf{States},\textsf{Trans},s_{\text{in}},F,\textsf{out})$ where
$A=(\textsf{States},\textsf{Trans},s_{\text{in}},F)$ is an NFA, and
$\textsf{out}:\textsf{Trans}\to\Sigma^{\ast}$ defines the outputs on each
transition. The function out defines a homomorphism
$\textsf{out}:\textsf{Trans}^{\ast}\to\Sigma^{\ast}$. The relation
$R\subseteq\Sigma^{\ast}\times\Sigma^{\ast}$ recognized by $T$, denoted $R(T)$
is given by $\\{(u,v)\mid u=\textsf{label}(t_{1}t_{2}\dots
t_{n}),v=\textsf{out}(t_{1}t_{2}\dots t_{n})$ and
$s_{\text{in}}\xrightarrow{t_{1}}s_{1}\xrightarrow{t_{2}}s_{2}\dots
s_{n-1}\xrightarrow{t_{n}}s_{n}$ with $s_{n}\in F\\}$. The equality relation
is realised by a transducer $T_{\text{id}}$. A transducer is depicted in
Figure 1.

$2$$3$$1$$\epsilon/\epsilon$$\epsilon/\epsilon$$b/bb$$a/a$$b/b$$a/aa$

Figure 1: A transducer. Here the label $x/y$ on a transition $t$ indicates
that $\textsf{label}(t)=x$ and $\textsf{out}(t)=y$. It nondeterministically
chooses to duplicates $a$s leaving $b$s as such, or duplicates $b$s leaving
$a$s as such.

A pushdown automaton over $\Sigma$ is given by a tuple
$P=(\textsf{States},\textsf{Trans},s_{\text{in}},F,\textsf{op},\Gamma)$ where
$A=(\textsf{States},\textsf{Trans},s_{\text{in}},F)$ is an NFA, $\Gamma$ is
the finite set of stack symbols, and
$\textsf{op}:\textsf{Trans}\to\textsf{Ops}$ defines the stack operation of
each transition, where
$\textsf{Ops}=\\{\textsf{push}(\gamma)\mid\gamma\in\Gamma\\}\cup\\{\textsf{pop}(\gamma)\mid\gamma\in\Gamma\\}\cup\\{\textsf{nop}\\}$.
When depicting the pushdown automaton pictorially, we represent a transition
$t=(s,a,s^{\prime})$ as $s\xrightarrow{a\mid op(t)}s^{\prime}$. When
$\textsf{op}(t)=\textsf{nop}$, we may simply write
$s\xrightarrow{a}s^{\prime}$. Further if $a=\epsilon$ then we may write it as
$s\xrightarrow{op(t)}s^{\prime}$. A configuration of a PDA is a pair
$(s,w)\in\textsf{States}\times\Gamma^{\ast}$, indicating the current state and
the stack contents. For two configurations $(s,w)$ and
$(s^{\prime},w^{\prime})$ we write
$(s,w)\xrightarrow{t}(s^{\prime},w^{\prime})$ for some $t\in\textsf{Trans}$ if
$t$ is of the form $(s,a,s^{\prime})$ and 1)
$\textsf{op}(t)=\textsf{push}(\gamma)$ and $w^{\prime}=\gamma\cdot w$, or 2)
$\textsf{op}(t)=\textsf{pop}(\gamma)$ and $w=\gamma\cdot w^{\prime}$, or 3)
$\textsf{op}(t)=\textsf{nop}$ and $w=w^{\prime}$. The language of a PDA P,
denoted $L(P)$ is given by $L(P)=\\{w\mid w=\textsf{label}(t_{1}t_{2}\dots
t_{n})$ and
$(s_{\text{in}},\epsilon)\xrightarrow{t_{1}}(s_{1},w_{1})\xrightarrow{t_{2}}(s_{2},w_{2})\dots(s_{n-1},w_{n-1})\xrightarrow{t_{n}}(s_{n},\epsilon)$
with $s_{n}\in F\\}$.

The set of all NFA / transducers / PDA over the alphabet $\Sigma$ is denoted
$\mathsf{NFA}(\Sigma)$ / $\mathsf{TRANSD}(\Sigma)$ / $\mathsf{PDA}(\Sigma)$. A
language $L\subseteq\Sigma^{\ast}$ is said to be context-free (resp. regular)
if there is a PDA (resp. NFA) $A$ such that $L=L(A)$. A relation
$R\subseteq\Sigma^{\ast}\times\Sigma^{\ast}$ is said to be rational if it is
recognized by some transducer $T$.

Given an NFA $A$ (resp. transducer $T$), its number of states is denoted by
$\textsf{state-size}(A)$ (resp. $\textsf{state-size}(T))$. Given a PDA $P$ by
$\textsf{state-size}(P)$ we denote the sum of the number of states and number
of stack symbols. That is $\textsf{state-size}(P)=|\textsf{States}|+|\Gamma|$.

##  3 String constraints

A string constraint over a set of variables $\mathcal{V}$ and an alphabet
$\Sigma$ is given by a set of membership constraints and a set of subword
ordering constraints. The membership constraint is given by associating a
pushdown automaton to each variable, indicating that the word assigned to the
variable must belong to the language of the pushdown automaton. A subword
order constraint is given by a pair $(x,Y)$ where $x\in\mathcal{V}$ and $Y$ is
a finite multiset over $\mathcal{V}\times\mathsf{TRANSD}(\Sigma)$.

For example, the constraint
$(x,{\\{\\!\\!\\{(y,T_{1}),(y,T_{2}),(y,T_{2}),(z,T_{2})\\}\\!\\!\\}})$ means
that the words assigned to $x$, $y$ and $z$, say $w_{x}$, $w_{y}$ and $w_{z}$
respectively, must satisfy $w_{x}\preceq w$ for some
$w\in\mathsf{Shuffle}(\\{\\!\\!\\{u_{1},u_{2},u_{3},u_{4}\\}\\!\\!\\})$, where
$(w_{y},u_{1})\in R(T_{1})$, $(w_{y},u_{2})\in R(T_{2})$, $(w_{y},u_{3})\in
R(T_{2})$, and $(w_{z},u_{4})\in R(T_{2})$. Note that the transducers can be
identity in which case the input and the output are the same. For instance, if
$T_{1}=T_{\text{id}}$ then $u_{1}$ must be same as $w_{y}$.

We sometimes denote the constraint $(x,Y)$ by $x\preceq\mathsf{Shuffle}(Y)$.
Abusing notation, we may write a pair
$(x,T)\in\mathcal{V}\times\mathsf{TRANSD}(\Sigma)$ as $T(x)$. If
$Y=\\{\\!\\!\\{(y,T)\\}\\!\\!\\}$ (i.e., a singleton), then we may simply
write $x\preceq T(y)$ instead of
$x\preceq\mathsf{Shuffle}(\\{\\!\\!\\{T(y)\\}\\!\\!\\})$. Further, we may
simply write $x$ for $(x,T_{\text{id}})$. For instance,
$(x,\\{\\!\\!\\{(y,T_{\text{id}})\\}\\!\\!\\})$ may be also written as
$x\preceq y$.

######  Definition 3.1.

A string constraint $C$ is a tuple
$\sc=(\Sigma,\mathcal{V},\mathsf{Mem},\mathsf{Rel})$ where
$\mathsf{Mem}:\mathcal{V}\to\mathsf{PDA}(\Sigma)\cup\mathsf{NFA}(\Sigma)$
assigns a PDA or an NFA to each variable, and
$\mathsf{Rel}\subseteq\mathcal{V}\times\mathbb{N}_{0}^{\mathcal{V}\times\mathsf{TRANSD}(\Sigma)}$
is a finite set of subword-order constraints.

We denote by $\textsc{trset}(C)$ the finite set of transducers occurring in
the string constraint $C$. That is,
$\textsc{trset}(C)=\\{T\mid\exists(x,Y)\in\mathsf{Rel},y\in\mathcal{V},(y,T)\in
Y\\}$. Similarly, $\textsc{autset}(C)$ is the finite set of PDA/NFA occurring
in $C$. That is, $\textsc{autset}(C)=\\{\mathsf{Mem}(x)\mid
x\in\mathcal{V}\\}$. A string constraint is regular if for every
$v\in\mathcal{V}$, $\mathsf{Mem}(v)$ is an NFA, (equivalently, if
$\textsc{autset}(C)\subseteq\mathsf{NFA}(\Sigma)$). An important parameter for
our complexity considerations will be the number of times a variable is used
in the right hand side (RHS). We denote it by
$\textsf{multiplicity}_{C}(x)=\sum_{T\in\textsc{trset}(C),(y,Y)\in\mathsf{Rel}}Y((x,T))$.
We omit the subscript and simply write $\textsf{multiplicity}(x)$ when $C$ is
clear from the context.

######  Definition 3.2.

A string constraint $C$ is _satisfiable_ if there exists an assignment
$\sigma:\mathcal{V}\to\Sigma^{\ast}$ that satisfies every membership and
relational constraints in $C$ — that is,

  1. 1.

$\sigma(v)\in L(\mathsf{Mem}(v))$ for all $v\in\mathcal{V}$

  2. 2.

For every $(x,Y)\in\mathsf{Rel}$, if
$Y=\\{\\!\\!\\{(y_{1},T_{1}),(y_{2},T_{2}),\dots(y_{n},T_{n})\\}\\!\\!\\}$,
then there are words $u_{1},u_{2},\dots,u_{n}$ such that
$(\sigma(y_{i}),u_{i})\in R(T_{i})$ for each $i\in\\{1,2,\dots,n\\}$, and
there is a word
$w\in\mathsf{Shuffle}(\\{\\!\\!\\{u_{1},u_{2},\dots,u_{n}\\}\\!\\!\\})$ such
that $\sigma(x)\preceq w$ .

Such an assignment $\sigma$ is called a _satisfying assignment_.

######  Example 3.3.

Consider a string constraint on two variables $x$ and $y$. The membership
constraints are as follows. $\mathsf{Mem}(x)$ is an NFA for $\\{ababab\\}$,
and $\mathsf{Mem}({y})$ is an NFA for $\\{ab\\}$. There is only one relational
constraint: $x\preceq\mathsf{Shuffle}(\\{\\!\\!\\{(y,T)(y,T)\\}\\!\\!\\})$,
where $T$ is the transducer defined in Figure 1. This string constraint is
satisfiable.

######  Definition 3.4.

(Satisfiability Problem for String Constraints)
Input : A string constraint $C$. Question: Is $C$ satisfiable ?

The satisfiability problem is undecidable already for regular string
constraints without transducers (or, equivalently, when only $T_{\text{id}}$
is allowed) [9]. To circumvent undecidability, acyclic fragment of string
constraints were considered in [9]. Formally, let $x<y$ if
$(x,Y)\in\mathsf{Rel}$ with $(y,T)\in Y$ for some transducer $T$. The string
constraint is acyclic if $<$ is acyclic. For the acyclic fragment without
transducers, satisfiability was shown in [9] to be NExptime-complete. The
lower bound already holds for regular acyclic string constraints without
transducers.

We study the satisfiability problem for acyclic string constraints in the
presence of transducers. Our main results are:

######  Theorem 3.5.

Satisfiability problem for acyclic context-free string constraints with
transducers is 2NExptime-complete.

######  Theorem 3.6.

Satisfiability problem for acyclic regular string constraints with transducers
is NExptime-complete.

######  Remark 3.7.

Our result shows an interesting contrast with string equations (with equality
instead of subword order in relational constraints). Satisfiability of string
equations (with concatenation, no shuffle) is decidable, when regular
membership constraints are allowed. Adding transducers on top however render
the satisfiability undecidable. In our setting, where subword order is used
instead of equality, adding transducers to the acyclic fragment retains
decidability.

######  Remark 3.8.

Without transducers, regular and context-free string constraints have the same
complexity. In the presence of transducers they are in different complexity
classes.

######  Remark 3.9.

It was shown in [9] that concatenation can be expressed by shuffle. This
simulation is only linear and furthermore it preserves acyclicity. Thus our
complexity upper bounds already hold for string constraints which uses the
more popular concatenation operation instead of shuffle. Interestingly, the
lower bounds in Theorem 3.5 and Theorem 3.6 already hold for the variant
without shuffle.

In Section 4 and Section 5 we prove the lower bound and upper bound claimed in
Theorem 3.5 respectively. The proof of Theorem 3.6 is given in Section 6. In
Section 7, we discuss some implications of our results and conclude.

##  4 2NEXPTIME Hardness

We prove the hardness by giving a reduction from a bounded variant of the PCP
problem that is 2NExptime-complete.

###  4.1 (Double-exponentially) Bounded PCP problem

In this decidable variant of the PCP problem, we are also given a parameter
$\ell$ as part of the input in unary, and we ask whether there is a solution
of length $2^{2^{\ell}}$. Formally the problem is stated as follows.

######  Definition 4.1.

(Double-exponentially) Bounded PCP problem (2eBPCP).
Input : $(\Sigma_{1},\Sigma_{2},f,g,\ell)$ where $\Sigma_{1}$ and $\Sigma_{2}$
are two disjoint finite alphabets, $f,g:\Sigma_{1}\to\Sigma_{2}^{\ast}$ are
two functions which naturally extend to a homomorphism from
$\Sigma_{1}^{\ast}\to\Sigma_{2}^{\ast}$, and $\ell\in\mathbb{N}$ is a natural
number. Question: Is there a word $w\in\Sigma_{1}^{+}$ with
$|f(w)|=2^{2^{\ell}}$ and $f(w)=g(w)$ ?

The above problem is 2NExptime-complete. If the problem asked for the length
of $f(w)$ to be $\ell$, it would be NP-complete [30], and if it was $2^{\ell}$
it would be NExptime-complete [9].

######  Theorem 4.2.

(Double-exponentially) Bounded PCP problem is 2NExptime-complete.

######  Proof 4.3.

Clearly the 2eBPCP problem is in 2NExptimeas we can guess a solution of the
appropriate size and verify it.

For the hardness, we first consider a modified version of bounded PCP called
the bounded MPCP and show that this problem is 2NExptime-hard. Out proof
strategy is similar to that in [9]. Following the technique provided in [34],
it is easy to reduce this problem to bounded PCP. The bounded MPCP asks, given
two equi-dimensional vector of words $\mathcal{U}=(u_{1},\cdots,u_{n})$ and
$\mathcal{V}=(v_{1},\cdots,v_{n})$ over an alphabet $\Sigma$ and an integer
$\ell\in\mathbb{N}$, whether there is a sequence $i_{1},\cdots
i_{k}\in[n]^{+}$ such that $u_{1}\cdot u_{i_{1}}\cdot u_{i_{2}}\cdots
u_{i_{k}}=v_{1}\cdot v_{i_{1}}\cdot v_{i_{2}}\cdots v_{i_{k}}$ and
$|u_{1}\cdot u_{i_{1}}\cdot u_{i_{2}}\cdots u_{i_{k}}|=|v_{1}\cdot
v_{i_{1}}\cdot v_{i_{2}}\cdots v_{i_{k}}|=2^{2^{\ell}}$. Notice that here we
require that the solution start from a designated initial index. Going from
bounded MPCP to bounded PCP requires only a linear blowup.

In order to give the reduction, we fix a non-deterministic Turing machine TM
over the alphabet $\\{0,1\\}$ of size $n$ and an input $w$ and show how to
construct an bounded MPCP $\mathcal{P}$ and an $\ell$ instance such that the
TM has an accepting run on $w$ of size at most $2^{2^{\textsf{poly}(|w|,n)}}$
for some polynomial $\textsf{poly}()$ if and only if $\mathcal{P}$ has a
solution of size exactly $2^{2^{\ell}}$. Further more, the size of
$\mathcal{P}$ and $\ell$ will only be quadratically dependent on
$\textsf{poly}()$, $n$ and $\textsf{len}(w)$.

We first recall the construction that reduces an unrestricted TM to
unrestricted MPCP from [34]. We assume that the transitions of the Turing
machine $\delta\subseteq{Q}\times\Sigma\times{Q}\times\Sigma\times\\{R,L\\}$,
where ${Q}$ are the set of states of the Turing machine and $\\{R,L\\}$
denotes the directions of the head movement i.e. right, left. Further we will
assume that $q_{0}$ is the start state of our Turing machine and that $F$ is
the set of final states.

The required PCP instance is $\mathcal{P}$ and is given below. Here
$\mathcal{U}$ ( $\mathcal{V}$ ) are obtained by projecting to the first
(second) component of the pairs given below.

$\displaystyle\\{(\\#,\\#q_{0}w\\#),(0,0),(1,1),(\\#,\\#)\\}$
$\displaystyle\cup$ $\displaystyle\\{(qx,yp)\mid(q,x,p,y,R)\in\delta,q\notin
F\\}$ $\displaystyle\\{(xqy,pxz)\mid(q,y,p,z,L)\in\delta,q\notin F\\}$
$\displaystyle\cup$ $\displaystyle\\{(qx,q),(xq,q)\mid q\in F,x\in\Sigma\\}$
$\displaystyle\\{(q\\#\\#,\\#)\mid q\in F\\}$

The following lemma provides us with the required correctness and the value of
$\ell$.

######  Lemma 4.4.

The Turing machine TM has an accepting run of size $m$ on $w$ then the MPCP
instance $\mathcal{P}$ has a solution of size $c\times m^{2}$ for some
constant $c\in\mathbb{N}$.

######  Proof 4.5 (Proof idea:).

Assume that there is a computation of the Turing machine of the form
$C_{1}{\xrightarrow{}}C_{2}\xrightarrow{}\cdots\xrightarrow{}C_{n}$, where
each $C_{i}$ is a configuration of the Turing machine. We will assume that
each configuration is of size at most $n$. In this case, there is a partial
solution to the MPCP instance of the form
$\\#C_{1}\\#C_{2}\\#\cdots\\#C_{n}\\#,\\#C_{1}\\#C_{2}\\#\cdots\\#C_{n-1}$.
Suppose $C_{n}$ contains a final state then the completion is done by reducing
one letter from the final configuration at a time using the pairs
$(qx,q),(xq,q)$. We refer to these as the completion suffix. Notice that the
completion suffix is of size $|C_{n}|\times(|C_{n}|-1)$. Hence we have a
bounded-MPCP solution of size $2\times n^{2}$.

The other direction is as in the following lemma and is easy to see.

######  Lemma 4.6.

If the MPCP instance $\mathcal{P}$ that we have constructed has a solution of
size $m$, then The Turing machine TM has an accepting run of size at most $m$
on $w$

Now suppose we want to find if TM has an accepting run on $w$ of size at most
$2^{2^{\textsf{poly}(|w|,n)}}$, we let
$\ell=c\times(\textsf{poly}(|w|,n))^{2}$. Then by Lemmas 4.6 and 4.4, we have
TM has an accepting run on $w$ of size at most $2^{2^{\textsf{poly}(|w|,n)}}$
if and only if the bounded-MPCP instance $\mathcal{P}$, $\ell$ has a solution.

###  4.2 Towards a reduction

Our idea is to use 4 variables $x_{1},x_{2},x_{f},x_{g}$. The membership
constraint for $x_{f}$ is a PDA for the language
$L_{f}=\\{w\cdot\\#^{\ast}\cdot f(w^{r})\mid w\in\Sigma_{1}^{\ast}\\}$, and
that for $x_{g}$ is a PDA for the language $L_{g}=\\{w\cdot\\#^{\ast}\cdot
g(w^{r})\mid w\in\Sigma_{1}^{\ast}\\}$. Recall that $w^{r}$ denotes the
reverse of $w$, and $\\#$ is a special symbol not in $\Sigma_{1}$ or
$\Sigma_{2}$. Suppose $x_{1}$ and $x_{2}$ are constrained to the language
$\Sigma_{1}^{m}\\#^{n}\Sigma_{2}^{2^{2^{\ell}}}$ such that $m+n=2^{2^{\ell}}$,
by polynomial-sized constraints. Then with the relational constraints 1)
$x_{1}\preceq x_{f}$ 2) $x_{f}\preceq x_{g}$ and 3) $x_{g}\preceq x_{2}$, we
will achieve our reduction. Recall that $x\preceq y$ is a short hand for
$x\preceq\mathsf{Shuffle}(\\{\\!\\!\\{(y,T_{\text{id}})\\}\\!\\!\\})$. Indeed
these constraints are satisfiable if and only if the 2eBPCP has a solution.

Notice that our constraints for $x_{1}$ and $x_{2}$ requires counting exactly
$2^{2^{\ell}}$. This is not possible with a polynomial-sized PDA. In the above
paragraph we did not use transducers either. Without transducers, the
satisfiability problem of string constraints is not 2NExptime-hard, it is
indeed in NExptime[9].

However, with the help of $\ell$ many transducers (or FSA) of size
$\mathcal{O}(\ell)$ we can have a PDA that counts $2^{2^{\ell}}$. We will
describe this technique with PDA and DFA in the next subsection, and in the
following subsection using this idea, we complete the reduction.

###  4.3 Counting $2^{2^{\ell}}$ using one PDA and $\ell$ DFA

Let
$\Gamma_{1}=\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1},\textsf{inc},\textsf{dec}\\}$,
and let $\Gamma_{2}$ be another finite alphabet disjoint from $\Gamma_{1}$.
Our objective is to come up with a PDA $A$ and $\ell$ DFAs $A_{1},A_{2},\dots
A_{\ell}$ over the alphabet $\Gamma_{1}\cup\Gamma_{2}$, each of size
$\mathcal{O}(\ell)$ such that any word accepted by all of them (i.e., in
$\cap_{i}L(A_{i})\cap L(A)$) has $2^{2^{\ell}}$ occurrences of letters from
$\Gamma_{2}$.

$\langle 0,\textsf{push}\rangle$$\langle 1,\textsf{push}\rangle$$\langle
2,\textsf{push}\rangle$

$\cdots$

$\langle n-1,\textsf{push}\rangle$$\langle n,\textsf{push}\rangle$$\langle
0,\textsf{switch}\rangle$$\langle 1,\textsf{switch}\rangle$$\langle
2,\textsf{switch}\rangle$

$\cdots$

$\langle n-1,\textsf{switch}\rangle$$\langle 0,\textsf{pop}\rangle$$\langle
1,\textsf{pop}\rangle$$\langle 2,\textsf{pop}\rangle$

$\cdots$

$\langle n-1,\textsf{pop}\rangle$$\langle
n,\textsf{pop}\rangle$$\textsf{push}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0})$$\textsf{push}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0})$$\textsf{push}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0})$$\textsf{push}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1})$$\textsf{push}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1})$$\textsf{push}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1})$$\textsf{pop}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0})$$\textsf{pop}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0})$$\textsf{pop}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1})$$\textsf{pop}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1})$$\textsf{pop}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1})$$\textsf{pop}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0})$$\Gamma_{2}$

Figure 2: A PDA with $3n+2$ states that accepts $(\Gamma_{2})^{2^{n}}$.

First we give a PDA with $3n+2$ states and stack symbols
$\\{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}\\}$
that accepts $(\Gamma_{2})^{2^{n}}$.

######  Claim 1.

There is a PDA with $3n+2$ states and stack symbols
$\\{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}\\}$
with stack-height never exceeding $n$ that accepts $(\Gamma_{2})^{2^{n}}$.

######  Proof 4.7.

Such a PDA is depicted in Figure 2. In this PDA the stack height never exceeds
$n$. The PDA has three modes - a push mode where it keeps pushing
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}$s until
the stack height is $n$, a pop mode where it keeps popping the symbol
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$, and a
switch mode that switches from a pop mode to push mode by replacing a
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}$ on the
top of the stack by a
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$. The
states then represent the current stack height and the mode.

When the PDA is in the state $\langle n,\textsf{push}\rangle$, the stack
contents represents an $n$-bit binary number. At this point it reads a symbol
from $\Gamma_{2}$ and goes to the state $\langle n,\textsf{pop}\rangle$. From
there, it does a sequence of transitions such that the next time it reaches
$\langle n,\textsf{push}\rangle$, the binary number in the stack would be
incremented. For this it replaces the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}^{m}$
suffix with a
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}^{m}$.

The initial state is $\langle 0,\textsf{push}\rangle$. The first time it
reaches $\langle n,\textsf{push}\rangle$, the stack content would be
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0}^{n}$.
The last time it reaches $\langle n,\textsf{push}\rangle$ (or $\langle
n,\textsf{pop}\rangle$) the stack content would be
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}^{n}$,
and from there it reaches $\langle 0,\textsf{pop}\rangle$ by popping the
entire stack. The state $\langle 0,\textsf{pop}\rangle$ is accepting. Since
this PDA reaches the state $\langle n,\textsf{push}\rangle$ exactly once for
every $n$-bit binary number, the number of $\Gamma_{2}$ symbols it reads is
$2^{n}$.

$\langle 0,\textsf{push}\rangle$$\langle 1,\textsf{push}\rangle$$\langle
2,\textsf{push}\rangle$

$\cdots$

$\langle n-1,\textsf{push}\rangle$$\langle n,\textsf{push}\rangle$$\langle
0,\textsf{switch}\rangle$$\langle 1,\textsf{switch}\rangle$$\langle
2,\textsf{switch}\rangle$

$\cdots$

$\langle n-1,\textsf{switch}\rangle$$\langle n,\textsf{switch}\rangle$$\langle
0,\textsf{pop}\rangle$$\langle 1,\textsf{pop}\rangle$$\langle
2,\textsf{pop}\rangle$

$\cdots$

$\langle n-1,\textsf{pop}\rangle$$\langle
n,\textsf{pop}\rangle$$\textsf{push}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0})$$\textsf{push}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0})$$\textsf{push}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0})$$\textsf{push}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1})$$\textsf{push}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1})$$\textsf{push}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1})$$\textsf{pop}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0})$$\textsf{pop}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0})$$\textsf{pop}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1})$$\textsf{pop}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1})$$\textsf{pop}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1})$$\textsf{pop}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0})$$\Gamma_{2}$$\Gamma_{2}$

Figure 3: A PDA with $3n+3$ states that accepts $(\Gamma_{2})^{2^{n+1}}$.

If $n=2^{\ell}$ we will be able to get $2^{2^{\ell}}$ length words from
$\Gamma_{2}$ as we wanted. However, we are allowed to use only
$\mathcal{O}(\ell)$ states. To overcome this, we will use $\ell$ length binary
numbers to indicate the current stack height. We then use $\ell$ DFAs, one for
each bit, to update the binary numbers representing the stack height as
required. We describe this below.

There is a small caveat that we need to address first. Since we will be using
$\ell$ bit numbers for representing the stack height, the maximum height we
can faithfully represent is $2^{\ell}-1$. With this, we would only get
$(\Gamma_{2})^{2^{\ell}-1}$ and not the desired $(\Gamma_{2})^{2^{\ell}}$.
Hence we modify the PDA in Figure 2 to accept words of length $2^{n+1}$ by
adding an extra state. This new PDA is depicted in Figure 3. It reads two
$\Gamma_{2}$ symbols each time a different $n$-bit number is present in the
stack. Thus the language of this $3n+3$ state PDA is $(\Gamma_{2})^{2^{n+1}}$.

######  Claim 2.

There is a PDA with $3n+3$ states and stack symbols
$\\{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}\\}$
with stack-height never exceeding $n$ that accepts $(\Gamma_{2})^{2^{n+1}}$.

We will next describe the $\ell$ DFAs that succinctly record the stack height.
We then give a PDA that, along with these $\ell$ DFAs, accepts words with
$2^{2^{\ell}}$ occurrences of letters from $\Gamma_{2}$.

Let $\\{\textsf{inc},\textsf{dec}\\}$ disjoint from $\Gamma_{2}$ be the
increment and the decrement operators on integers. Further, we may treat
symbols from $\Gamma_{2}$ as ‘keep unchanged’ operators. That is,
$\textsf{inc}(n)=n+1$, $\textsf{dec}(n)=n-1$ and $a(n)=n$ for all
$a\in\Gamma_{2}$. Consider the following language over the alphabet
$\Gamma=\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1},\textsf{inc},\textsf{dec}\\}\cup\Gamma_{2}$
of alternating sequences of $\ell$-bit numbers and operators, where each
operator when applied on the previous number gives the next number. Here, the
binary numbers are written with the most-significant bit on the left. That is
$\textsf{val}(b_{1}b_{2}\dots b_{\ell})=\sum_{i}b_{i}\times 2^{\ell-i}$.

$\displaystyle L_{\ell}=\\{n_{0}o_{1}n_{1}o_{2}n_{2}\cdots o_{k}n_{k}$
$\displaystyle\mid$ $\displaystyle k\geq
0,n_{i}\in({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}+{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1})^{\ell}\textrm{
for all }i:0\leq i\leq k$ $\displaystyle
o_{i}\in\\{\textsf{inc},\textsf{dec}\\}\cup\Gamma_{2}\textrm{ for all
}i:0<i\leq k$ $\displaystyle\textsf{val}(n_{i})\equiv
o_{i}(\textsf{val}(n_{i-1}))\mod 2^{\ell}\textrm{ for all }i:0<i\leq k\\}$

######  Claim 3.

There are $\ell$ DFAs $B_{1},B_{2},\dots B_{\ell}$, each with
$\mathcal{O}(\ell)$ states such that $L_{\ell}=\bigcap_{i}L(B_{i})$.

######  Proof 4.8.

We describe the $\ell$ DFAs $B_{1},B_{2},\dots B_{\ell}$ below.

The $i$th DFA $B_{i}$ guarantees that the $i$th bit takes the correct value.
This DFA is depicted in the Figure 4. The automaton has two disconnected
‘forks’ (the top one starting at $s^{i}_{0}$ and the bottom one starting at
$s^{i}_{1}$). In the top fork, the $i$th bit read is always
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$, and in
the bottom fork the $i$th bit read is always
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$.
Consider $n_{j-1}o_{j}n_{j}$ occurring in the above sequence. Let
$n_{j-1}=b_{1}b_{2}\dots b_{\ell}$ and let
$n_{j}=b^{\prime}_{1}b^{\prime}_{2}\dots b^{\prime}_{\ell}$. If $o_{j}$ is
inc, the $i$th bit $b_{i}$ is toggled ($b^{\prime}_{i}\neq b_{i}$) iff
$b_{m}=1$ for all $m:m>i$. If $o_{j}$ is dec, the $i$th bit $b_{i}$ is toggled
($b^{\prime}_{i}\neq b_{i}$) iff $b_{m}=0$ for all $m:m>i$. If
$o_{j}\in\Gamma_{2}$ the $i$th bit is never toggled. The initial states are
$s^{i}_{0}$ and $s^{i}_{1}$, and the accepting states are $t^{i}_{0},\dots
t^{i}_{5}$. Clearly $L_{\ell}=\bigcap_{i}L(B_{i})$.

$s^{i}_{0}$$\cdots$$\cdots$$t^{i}_{0}$$\cdots$$t^{i}_{1}$$\cdots$$t^{i}_{2}$$s^{i}_{1}$$\cdots$$\cdots$$t^{i}_{3}$$\cdots$$t^{i}_{4}$$\cdots$$t^{i}_{5}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$$\Gamma_{2}$$\Gamma_{2}$incincdecdec

Figure 4: The automaton $B_{i}$. The transitions on
$\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}\\}$
are depicted in blue. The transitions on $\Gamma_{2}$ (resp. inc, dec) are
depicted in brown (resp. green, red).

However, for succinctly simulating the PDA given in Figure 3, we need the
$\ell$ DFAs to faithfully reflect the stack height. For this we consider a
slight modification of $L_{\ell}$.

$\displaystyle L^{\prime}_{\ell}=\\{n_{0}o_{1}n_{1}o_{2}n_{2}\cdots
o_{k}n_{k}$ $\displaystyle\mid$ $\displaystyle k\geq
0,n_{i}\in({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}+{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1})^{\ell}\textrm{
for all }i:0\leq i\leq k$ $\displaystyle
o_{i}\in\\{\textsf{inc},\textsf{dec}\\}\cup\Gamma_{2}\textrm{ for all
}i:0<i\leq k$ $\displaystyle\textsf{val}(n_{i})\equiv
o_{i}(\textsf{val}(n_{i-1}))\textrm{ for all }i:0<i\leq k$ $\displaystyle
n_{0}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}^{\ell}=n_{k},\textrm{
if }o_{i}=\textsf{inc}\textrm{ then
}n_{i-1}\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}^{\ell}$
$\displaystyle\textrm{ if }o_{i}=\textsf{dec}\textrm{ then
}n_{i-1}\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}^{\ell}\\}$

This ensures that the PDA starts and ends with an empty stack. Further inc
after $1^{\ell}$ and dec after $0^{\ell}$ are forbidden. Otherwise, the value
will not faithfully represent the stack height.

######  Claim 4.

There are $\ell$ DFAs $A_{1},A_{2},\dots A_{\ell}$, each with
$\mathcal{O}(\ell)$ states such that $L^{\prime}_{\ell}=\bigcap_{i}L(A_{i})$.

######  Proof 4.9.

The states of $A_{i}$ are exactly those of $B_{i}$. For $i\geq 2$, the
transitions of $A_{i}$ is exactly the same as that of $B_{i}$. The transitions
for $A_{1}$ is obtained by removing two transitions from that of $B_{1}$,
namely the outgoing inc transition from $t^{1}_{5}$ and the outgoing dec
transition from $t^{1}_{0}$. For all $i\geq 1$, the initial state of $A_{i}$
is $s^{i}_{0}$ and the final state is $t^{i}_{0}$.

######  Claim 5.

There is a PDA $A$ with 3 states and stack symbols
$\\{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}\\}$
such that $L(A)\cap L^{\prime}_{\ell}$ when projected to $\Gamma_{2}$ is
exactly $(\Gamma_{2})^{2^{2^{\ell}}}$.

pushswitchpop$\textsf{inc}\\!\mid\\!\textsf{push}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1})$$\textsf{dec}\\!\mid\\!\textsf{pop}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0})$$\Gamma_{2}$$\Gamma_{2}$$\textsf{inc}\\!\mid\\!\textsf{push}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}0})$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$$\textsf{dec}\\!\mid\\!\textsf{pop}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1})$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}$

Figure 5: The PDA $A$. This PDA and the $\ell$ DFAs together faithfully encode
the accepting runs of the PDA in Figure 3 with $n=2^{\ell}-1$. Thus they
accept words with exactly $2^{2^{\ell}}$ occurrences of $\Gamma_{2}$.

######  Proof 4.10.

The PDA $A$ is depicted in Figure 5. The three states represents the three
modes of the PDA in Figure 3. The $\ell$ DFAs will guarantee that we start
with the number
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}0}^{\ell}$.
Because of $A_{1}$, the PDA cannot take the inc transition from the state
$\langle\textsf{push}\rangle$ immediately after the number
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}^{\ell}$.
It will have to read a $\Gamma_{2}$ symbol and move to the state
$\langle\textsf{switch}\rangle$. The PDA will loop in this state once by
reading the same number
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}^{\ell}$)
as mandated by the $\Gamma_{2}$ transitions of the DFAs. From this state,
again inc is disabled by $A_{1}$, and hence the PDA will read another
$\Gamma_{2}$ symbol and go to the state $\langle\textsf{pop}\rangle$. The PDA
will read
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}^{\ell}$
staying in the state $\langle\textsf{pop}\rangle$ after which it can take a
dec transition.

###  4.4 Completing the reduction

Before giving the reduction, let us first define a PDA and the transducers
that we use in the reduction. Let $P_{1}$ be the PDA in Claim 5 with
$\Gamma_{2}=\Sigma_{1}\cup\\{\\#\\}$. Let $P_{2}$ the PDA for
$L(P_{1})\cap(\Sigma_{1}^{\ast}\\#^{\ast})$. Let $P_{3}$ be the PDA in Claim 5
with $\Gamma_{2}=\Sigma_{2}$. Let $P_{4}$ be the PDA for $L(P_{2})\cdot
L(P_{3})$. Let $T_{1},\dots T_{\ell}$ be $\ell$ transducers. The input
automaton of $T_{i}$ is exactly the DFA $A_{i}$ from Claim 4 with
$\Gamma_{2}=\Sigma_{1}\cup\Sigma_{2}\cup\\{\\#\\}$. The output of the
transducer $T_{i}$ on every transition is $\epsilon$.

Now we are ready to give the reduction. Let
$\mathcal{P}=(\Sigma_{1},\Sigma_{2},f,g,\ell)$ be an input to a 2eBPCP
problem. We describe how to obtain a string constraint $C_{P}$ from this. We
use the alphabet $\Sigma=\Sigma_{1}\cup\Sigma_{2}\cup\Gamma_{1}\cup\\{\\#\\}$,
and the variable set $\mathcal{V}=\\{x_{0},x_{1},x_{2},x_{f},x_{g}\\}$. Next
we define the membership constraints $\mathsf{Mem}$. Let
$\mathsf{Mem}(x_{0})=A_{\epsilon}$ where $A_{\epsilon}$ is an NFA for
$\\{\epsilon\\}$. We have
$\mathsf{Mem}(x_{1})=P_{4},\mathsf{Mem}(x_{2})=P_{4}$. Now we need to augment
the language of $x_{f}$ and $x_{g}$ to also account for the letters from
$\Gamma_{1}$, which can be achieved by adding $\Gamma_{1}$ self loops in all
the states in the PDA for $L_{f}$ and $L_{g}$ respectively. Thus the language
for $x_{f}$ is $\mathfrak{W}(L_{f},\Gamma_{1}^{\ast})$, where
$\mathfrak{W}(L_{f},\Gamma_{1}^{\ast})=\\{w\mid w\in\mathsf{Shuffle}(u,v),u\in
L_{f},v\in\Gamma_{1}^{\ast}\\}$. Similarly the language for $x_{g}$ is
$\mathfrak{W}(L_{g},\Gamma_{1}^{\ast})$. Let $P_{5}$ and $P_{6}$ be PDAs
recognizing $\mathfrak{W}(L_{f},\Gamma_{1}^{\ast})$, and
$\mathfrak{W}(L_{g},\Gamma_{1}^{\ast})$ respectively. We have
$\mathsf{Mem}(x_{f})=P_{5}$ and $\mathsf{Mem}(x_{g})=P_{6}$. Let
$\mathsf{Rel}$ be the following relational constraints: 1)$x_{0}\preceq
T_{i}(x_{1})$, for all $i:1<i<\ell$, 2) $x_{0}\preceq T_{i}(x_{2})$, for all
$i:1<i<\ell$, 3) $x_{1}\preceq x_{f}$, 4) $x_{f}\preceq x_{g}$ and 5)
$x_{g}\preceq x_{2}$. We have $2\ell+3$ relational constraints. Further
$\textsf{multiplicity}(x_{1})=\ell=\textsf{multiplicity}(x_{2})$ in our
construction. Let
$C_{\mathcal{P}}=(\Sigma,\mathcal{V},\mathsf{Mem},\mathsf{Rel})$.

######  Claim 6.

The string constraint $C_{\mathcal{P}}$ is satisfiable if and only if the
2eBPCP instance $\mathcal{P}$ has a solution.

######  Proof 4.11.

Suppose the string constraint $C_{\mathcal{P}}$ is satisfiable, let $\sigma$
be the satisfying assignment. Then we claim that
$\sigma(x_{f})=\sigma(x_{g})=\sigma(x_{1})=\sigma(x_{2})$. Further more,
${\sigma(x_{f})}_{\downarrow{\Gamma_{2}}}=\Sigma_{1}^{m_{1}}\\#^{m_{2}}\Sigma_{2}^{m_{1}+m_{2}}$,
where $m_{1}$ and $m_{2}$ are such that $m_{1}+m_{2}=2^{2^{\ell}}$. This,
combining with the membership constraints of $x_{f},x_{g}$ immediately
provides us with the solution for the 2eBPCP instance $\mathcal{P}$.

To see why $\sigma(x_{f})=\sigma(x_{g})=\sigma(x_{1})=\sigma(x_{2})$, note
that the constraints in $1$ and $2$ will ensure that
$\sigma(x_{1})\in\bigcap_{i=1}^{\ell}L(A_{i})$. The membership constraint
$\mathsf{Mem}(x_{1})=P_{4}$ will entail $\sigma(x_{1})=w_{1}\cdot w_{2}$ with
$w_{1}\in L(P_{2})$ and $w_{2}\in L(P_{3})$. This will in turn ensure that
${w_{1}}_{\downarrow{\Gamma_{2}}}=\Sigma_{1}^{m_{1}}\\#^{m_{2}}$, where
$m_{1}+m_{2}=2^{2^{\ell}}$ and
${w_{1}}_{\downarrow{\Gamma_{2}}}=\Sigma_{2}^{2^{2^{\ell}}}$. Similar argument
can also be made for $\sigma(x_{2})$. From this, we also obtain that
$|\sigma(x_{1})|=|\sigma(x_{2})|$. From the relational constraints $3,4,5$, we
also have $x_{1}\preceq x_{2}$ implying $\sigma(x_{1})=\sigma(x_{2})$.

For the other direction, suppose $\mathcal{P}$ has a solution, then we
construct the satisfying assignment for $C_{\mathcal{P}}$ as follows. Let the
solution for $\mathcal{P}$ be $w\in\Sigma_{1}^{*}$ such that $f(w)=g(w)$ and
$|f(w)|=2^{2^{\ell}}$. Let $w^{\prime}\in L^{\prime}_{\ell}$ be such that
${w^{\prime}}_{\downarrow{\Sigma_{1}\cup\Sigma_{2}\cup\\{\\#\\}}}=v$, where
$v=w\cdot\\#^{m}\cdot f(w)^{r}$, for some $m=2^{2^{\ell}}-|w|$. We let
$\sigma(x_{1})=\sigma(x_{2})=\sigma(x_{g})=\sigma(x_{f})=w^{\prime}$. Notice
that the constraints $1,2$ are satisfied since the word is picked from
$L^{\prime}_{\ell}$. It satisfies the constraints $3,4,5$ since all the
variables are assigned the same word. It is also easy to verify that the
membership constraints are satisfied. Hence, $\sigma$ that we constructed is a
satisfying assignment.

Notice that we construct $C_{\mathcal{P}}$ from $\mathcal{P}$ in polynomial
time, and it is acyclic. Hence, it follows that the satisfiability checking of
acyclic string constraints is 2NExptime-hard, proving the lower bound of
Theorem 3.5.

##  5 Satisfiability is in 2NEXPTIME

We will show that if an acyclic string constraint is satisfiable, then there
is a satisfying assignment of double exponential size.

######  Theorem 5.1 (Small model property).

Let $C$ be a satisfiable acyclic string constraint. Then $C$ has a satisfying
assignment $\sigma$ such that $\textsf{len}(\sigma(x))\leq B$ where $B$ is

$2^{2^{\mathcal{O}(m\log t+\log p+\log k)}}$

where

  * •

$m=\max_{x\in\mathcal{V}}\textsf{multiplicity}(x)$, the maximum multiplicity
of any variable,

  * •

$t=\max_{T\in\textsc{trset}(C)}\textsf{state-size}(T)$, the maximum number of
states of any transducer,

  * •

$p=\max_{P\in\textsc{autset}(C)}\textsf{state-size}(P)$, the maximum number of
states (and stack symbols) of any automaton.

  * •

$k=|\mathcal{V}|$, the number of variables.

Our aim, towards a 2NEXPTIME procedure, is to non-deterministically guess an
assignment of size at most double exponential, and check that it satisfies the
Conditions 1 and 2 (see Definition 3.2). However, Condition 2 uses more
existentially quantified variables, and it is not evident that verifying
Condition 2 can be done within the complexity limits. Towards this, we define
an extended assignment which considers the values given to these existentially
quantified variables as well, and show that every word used in this extended
assignment is of length at most $B$. We define the extended assignment and the
related notions and notations, and state the small model property for the
extended assignment.

Recall that $\textsf{multiplicity}(x)$ denotes the number of times a variable
occurs on the RHS of the constraints. In each such occurrence, the variable
occurs in a pair along with a transducer (of the form $(x,T)$), which belongs
to the RHS of a constraint from $\mathsf{Rel}$ of the form $(y,Y)$. Let us fix
some enumeration of these occurrences, and define the respective transducer
and constraint of the $i$th occurrence of $x$ by $T_{i}^{x}$ and
$\textsf{constraint}(x,i)$. Now, as per Condition 2, there are words (output
words of the respective transducers), that witness the transduction. For every
$x\in\mathcal{V}$ and $i\in[\textsf{multiplicity}(x)]$, let $o_{i}^{x}$ be a
new variable. This variable is intended to take as value a witness word for
the output of the transducer $T_{i}^{x}$ on the word provided by $x$, so that
the constraint $\textsf{constraint}(x,i)$ is satisfied. Let
$\widehat{\mathcal{V}}(C)$, or simply $\widehat{\mathcal{V}}$ when $C$ is
clear from the context, contain the output variables in addition to the
original variables. That is, $\widehat{\mathcal{V}}=O\cup\mathcal{V}$, where
$O=\\{o_{i}^{x}\mid x\in\mathcal{V},i\in[\textsf{multiplicity}(x)]\\}$. An
extended assignment $\widehat{\sigma}:\widehat{\mathcal{V}}\to\Sigma^{\ast}$
satisfies a string constraint $C$ if

  1. E1

$\widehat{\sigma}(x)\in\mathsf{Mem}(x)$ for all $x\in\mathcal{V}$

  2. E2

$(\widehat{\sigma}(x),\widehat{\sigma}(o_{i}^{x}))\in R(T_{i}^{x})$, for all
$x\in\mathcal{V}$, $i\in[\textsf{multiplicity}(x)]$

  3. E3

For every $(y,Y)\in\mathsf{Rel}$, we have
$\widehat{\sigma}(y)\preceq\mathsf{Shuffle}(\widehat{\sigma}(Y))$ where
$\widehat{\sigma}(Y)$ is an overloaded notation for the multiset

$\\{\\!\\!\\{\widehat{\sigma}(o_{i}^{x})\mid
x\in\mathcal{V},i\in[\textsf{multiplicity}(x)],\textsf{constraint}(x,i)=(y,Y)\\}\\!\\!\\}.$
(1)

We will actually prove the small model property for the extended assignments.

######  Lemma 5.2.

Let $C$ be a satisfiable acyclic string constraint. Let $B$ be
$2^{2^{\mathcal{O}(m\log t+\log p+\log k)}}$. Then $C$ has a satisfying
extended assignment $\widehat{\sigma}$ such that
$\textsf{len}(\widehat{\sigma}(x))\leq B$ for all $x\in\mathcal{V}(C)$, and
$\textsf{len}(\widehat{\sigma}(y))\leq 2ctB$ for all $y\in O$. The parameters
$m,t,p,k$ are as defined in Theorem 5.1, and
$c=\max\\{\textsf{len}(\textsf{out}(tr))\mid tr\textrm{ is a transition of
}T,\textrm{ and }T\in\textsc{trset}(C)\\}$.

With this, our non-deterministic procedure guesses an extended assignment and
verifies that it satisfies the conditions 1, 2 and 3. In fact, checking
whether a given word $w$ is a subword of some word in $\mathsf{Shuffle}(W)$
where $W$ is a finite mutliset of words is NP-complete [9, 23]. It remains to
prove Lemma 5.2.

######  Proof 5.3 (Proof of Lemma 5.2).

Consider an acyclic string constraint $C$. Recall that we write $x<y$ if
$(x,Y)\in\mathsf{Rel}$ with $(y,T)\in Y$ for some $T\in\textsc{trset}(C)$.
Consider a topological sorting of the variables respecting the relation $<$,
say $x_{1},x_{2},\dots,x_{k}$. Note that $x_{1}$ does not appear in the RHS of
any subword order constraint (in other words,
$\textsf{multiplicity}(x_{1})=0$). If $(x_{i},T)$ appears on the RHS of any
constraint for some $T$, then the LHS of that constraint is $x_{j}$ for some
$j<i$.

Suppose $C$ is satisfiable. Let $\widehat{\sigma}_{0}$ be a satisfying
extended assignment. In order to get the $\widehat{\sigma}$ as per Lemma 5.2,
we will construct a sequence of $k$ extended assignments, each progressively
modifying the previous one until we reach our goal. That is, we will construct
the sequence,
$\widehat{\sigma}_{0},\widehat{\sigma}_{1},\dots,\widehat{\sigma}_{k}=\widehat{\sigma}$
such that for each $i\in[k]$

  1. I1

$\widehat{\sigma}_{i}$ is satisfiable. That is, 1) membership constraints are
satisfied (Condition E1), 2) transductions are accepted by the transducers
(Condition E2), and 3) the relational constraints are satisfied (Condition
E3).

  2. I2

for all $j:j\leq i$, $\textsf{len}(\widehat{\sigma}_{i}(x_{j}))\leq B_{j}$ and
for each $\ell\in\textsf{multiplicity}(x_{j})$,
$\textsf{len}(\widehat{\sigma}_{i}(o_{\ell}^{x_{j}}))\leq 2ctB_{j}$. We define
$B_{n}$ as follows. $B_{1}=2^{p^{3}}$, and for $n>1$, $B_{n}=2m\cdot
t^{2m}\cdot p^{3}\cdot B_{n-1}\cdot 2^{p^{3}t^{2m}}$.

Note that, $B_{n}$ increases with $n$ and $B_{k}$ is at most $B$.

Base cases We consider $\widehat{\sigma}_{0}$ and $\widehat{\sigma}_{1}$ as
base cases. For $\widehat{\sigma}_{0}$, it is given to be satisfiable, and
Condition I2 above holds vacuously.

Towards constructing $\widehat{\sigma}_{1}$, consider the variable $x_{1}$,
and a context-free grammar $G_{1}$ for $\mathsf{Mem}(x_{1})$ in Chomsky Normal
Form with at most $p^{3}$ non-terminals [14]. Note that $G_{1}$ can be
constructed in polynomial time. Since $\widehat{\sigma}_{0}$ is satisfying,
the word $w_{1}=\widehat{\sigma}_{0}(x_{1})$ has a valid parse tree in
$G_{1}$. If a non terminal repeats in any leaf to root path in this tree, say
at node $n_{1}$ and node $n_{2}$ with $n_{2}$ an ancestor of $n_{1}$, then we
can shrink the parse tree (pump down) by replacing the subtree rooted at
$n_{2}$ by the subtree rooted at $n_{1}$ to get a smaller parse tree of a
smaller word in the language. Furthermore, this smaller word will be a subword
of $w_{1}$. Consider a shrinking of the parse tree of $w_{1}$ which cannot be
shrunk any further. This tree has size at most $2^{p^{3}}$, and hence its
yield $\widehat{w_{1}}$ satisfies Condition I2. Setting $x_{1}$ to
$\widehat{w_{1}}$ will also satisfy Condition I1. Further, note that there are
no output variables corresponding to $x_{1}$. Hence we get
$\widehat{\sigma}_{1}$:
$\widehat{\sigma}_{1}(x)=\begin{cases}\widehat{w_{1}}&\text{ if }x=x_{1}\\\
\widehat{\sigma}_{0}(x)&\text{ otherwise. }\end{cases}$

Inductive Step Now, for the inductive case, assume we have constructed
$\widehat{\sigma}_{i-1}$. We will describe how to obtain
$\widehat{\sigma}_{i}$. Let $G_{i}$ be the context-free grammar in Chomsky
Normal Form for $\mathsf{Mem}(x_{i})$ with $p^{3}$ non-terminals. We will
basically do a “conservative” pumping down of $w_{i}=\sigma_{i-1}(x_{i})$,
which ensures that the constraints are still satisfied, which we explain
below.

Challenges  In order to bound the length of $\widehat{\sigma}_{i}(x_{i})$ we
may consider subwords $w^{\prime}_{i}\preceq w_{i}$, so that the constraints
in which $x_{i}$ appear on the left continue to be satisfied. In addition,
such a subword $w^{\prime}_{i}$ must not only satisfy the membership
constraint ($w^{\prime}_{i}\in\mathsf{Mem}(x_{i})$) but also admit the
specified transductions – that is, for all
$\ell\in[\textsf{multiplicity}(x_{i})]$, we must have
$(w^{\prime}_{i},u_{\ell}^{\prime})\in R(T_{\ell}^{x_{i}})$ for some
$u^{\prime}_{\ell}$. Furthermore, a mere existence of such a
$u^{\prime}_{\ell}$ is not sufficient – consider the constraint
$(x_{j},Y)=\textsf{constraint}(x_{i},\ell)$ and let
$\widehat{\sigma}_{i-1}(x_{j})=w_{j}$ and $\widehat{\sigma}_{i-1}(Y)=U$ with
$\widehat{\sigma}_{i-1}(o_{\ell}^{x_{i}})=u_{\ell}$ (recall,
$\widehat{\sigma}(Y)$ is defined in Equation 1)). Since
$\widehat{\sigma}_{i-1}$ is satisfying we know that
$w_{j}\preceq\mathsf{Shuffle}(U)$. However, it need not be the case that
$w_{j}\preceq\mathsf{Shuffle}(U\setminus\\{u_{\ell}\\}\cup\\{u^{\prime}_{\ell}\\})$.
Hence we need to find a suitable $u^{\prime}_{\ell}$ such that $w_{j}\preceq
U\setminus\\{u_{\ell}\\}\cup\\{u^{\prime}_{\ell}\\}$. One way to ensure this,
is by insisting that $u_{\ell}^{\prime}$ provides the same “witnessing
subword” that $u_{\ell}$ provided. We formalise this notion of “witnessing
subword” below.

We give two equivalent definitions for $w\preceq\mathsf{Shuffle}(U)$.

######  Claim 7.

Let $w$ be a word and $U=\\{\\!\\!\\{u_{1}^{\prime},u_{2}^{\prime}\dots
u_{n}^{\prime}\\}\\!\\!\\}$ be a multiset of words. The following statements
are equivalent.

  1. 1.

There exists $w^{\prime}$: 1) $w^{\prime}\in\mathsf{Shuffle}(U)$ and 2)
$w\preceq w^{\prime}$.

  2. 2.

There exist $u_{1}^{\prime},u_{2}^{\prime}\dots u_{n}^{\prime}$: 1)
$w\in\mathsf{Shuffle}(\\{\\!\\!\\{u_{1}^{\prime},u_{2}^{\prime}\dots
u_{n}^{\prime}\\}\\!\\!\\})$ and 2) $u_{i}^{\prime}\preceq u_{i}$.

######  Proof 5.4.

Let $w\preceq w^{\prime}$ for some $w^{\prime}\in\mathsf{Shuffle}(U)$. Then
there is an injective map from the positions of $w$ to $w^{\prime}$. Further
since $w^{\prime}\in\mathsf{Shuffle}(U)$, there is an injective map from
$w^{\prime}$ to positions in the disjoint union of the positions of $u_{i}$.
Composing the two injective map and projecting to the relevant positions in
$u_{1},u_{2},\dots u_{n}$ will provide us with the required
$u_{1}^{\prime},u_{2}^{\prime}\dots u_{n}^{\prime}$such that
$w\in\mathsf{Shuffle}(\\{\\!\\!\\{u_{1}^{\prime},u_{2}^{\prime}\dots
u_{n}^{\prime}\\}\\!\\!\\})$.

Suppose $u_{1}^{\prime},u_{2}^{\prime}\dots u_{n}^{\prime}$ is such that
$w\in\mathsf{Shuffle}(\\{\\!\\!\\{u_{1}^{\prime},u_{2}^{\prime}\dots
u_{n}^{\prime}\\}\\!\\!\\})$ and $u_{i}^{\prime}\preceq u_{i}$. We can obtain
the required $w^{\prime}$ by iterating over all $i$ and inserting into $w$,
the positions in $u_{i}$ but not in $u^{\prime}_{i}$, in order.

We refer to $v_{1},\dots v_{n}$ as the _witnessing subwords_ of $u_{1},\dots
u_{n}$ for $w\preceq\mathsf{Shuffle}(U)$. We can also define the witnessing
projection for these witnessing subwords.

######  Definition 5.5 (Witnessing Projection of a subword expression).

Let $U$ be a multiset of words, and $w$ be a word. Let $u_{1},\dots u_{n}$ be
an enumeration of $U$. Let $\pi:\\{1,\dots,n\\}\to\Sigma^{\ast}$ be a map. We
say that $\pi$ is a _witnessing projection_ for the expression
$w\preceq\mathsf{Shuffle}(U)$ if

  1. 1.

${\pi(i)}\preceq u_{i}$

  2. 2.

$w\in\mathsf{Shuffle}(\\{{\pi(i)}\mid i\in\\{1,\dots,n\\}\\})$.

######  Claim 8.

The expression $w\preceq\mathsf{Shuffle}(U)$ is satisfiable if and only if it
has a witnessing projection.

######  Proof 5.6.

We use the second statement from Claim 7. If the expression is satisfiable,
then a witnessing projection $\pi$ will assign $u_{i}^{\prime}$ to each $i$.
Conversely if there is a witnessing projection, then clearly that gives us the
necessary $u_{i}^{\prime}$.

Next we extend the notion of witnessing projections to a set of expressions.

######  Definition 5.7 (Witnessing Projection for a set of expressions).

Let $R$ be a set of expressions of the form $w\preceq\mathsf{Shuffle}(U)$. Let
$\Pi$ be a map that assigns to each expression $r\equiv
w\preceq\mathsf{Shuffle}(U)$ a map
$\pi_{r}:\\{1,2,\dots|U|\\}\to\Sigma^{\ast}$. We say $\Pi$ is a witnessing
projection for $R$ if for each $r\in R$, $\Pi(r)$ is a witnessing projection
for $r$.

######  Example 5.8.

Consider the expression
$baab\preceq\mathsf{Shuffle}(\\{\\!\\!\\{aba,aba\\}\\!\\!\\})$. A witnessing
projection for this expression assigns $ba$ to the first occurrence and $ab$
to the second occurrence of $aba$ in the RHS.

In light of the above definition, we can write Condition E3 in the
satisfaction of a constraint using extended assignment, equivalently as

  1. E3’

There exists a witnessing projection for $\widehat{\sigma}(\mathsf{Rel})$,
where $\widehat{\sigma}(\mathsf{Rel})=\\{\\!\\!\\{\widehat{\sigma}(r)\mid
r\in\mathsf{Rel}\\}\\!\\!\\}$. Here
$\widehat{\sigma}(y,Y)\equiv\widehat{\sigma}(y)\preceq\mathsf{Shuffle}(\widehat{\sigma}(Y))$.

Recall that $\widehat{\sigma}(Y)$ is an overloaded notation for the multiset
$\\{\\!\\!\\{\widehat{\sigma}(o_{i}^{x})\mid
x\in\mathcal{V},i\in\\{1,2,\dots,\textsf{multiplicity}(x)\\},\textsf{constraint}(x,i)=(y,Y)\\}\\!\\!\\}.$
Suppose $\Pi$ is a witnessing projection for $\widehat{\sigma}(\mathsf{Rel})$.
Let $r\equiv(x,Y)\in\mathsf{Rel}$ and let $\Pi(r)=\pi_{r}$. Consider the
enumeration of
$\widehat{\sigma}(Y)=\\{\\!\\!\\{\widehat{\sigma}(o_{1}),\widehat{\sigma}(o_{2}),\dots\\}\\!\\!\\}$
where each $o_{j}$ is an output variable. Instead of $\pi_{r}(i)$ we may also
write $\pi_{r}(o_{i})$.

Thus, for the inductive case, we need to find good $w^{\prime}_{i}$,
$u_{1}^{\prime},\dots u^{\prime}_{\textsf{multiplicity}(x_{i})}$ such that

  1. 1.

$|w^{\prime}_{i}|\leq B_{i}$

  2. 2.

for each $\ell$, $|u^{\prime}_{\ell}|\leq 2\cdot t\cdot B_{i}$,

  3. 3.

$w^{\prime}_{i}\in\mathsf{Mem}(x_{i})$,

  4. 4.

$(w^{\prime}_{i},u_{\ell}^{\prime})\in R(T_{\ell}^{x_{i}})$ for each $\ell$,
and

  5. 5.

$v_{\ell}\preceq u^{\prime}_{\ell}$ where $v_{\ell}$ is a witnessing subword
of $u_{\ell}=\widehat{\sigma}_{i-1}(o_{\ell}^{x_{i}})$ for the relation
$\widehat{\sigma}_{i-1}(y)\preceq\mathsf{Shuffle}(\widehat{\sigma}_{i-1}(Y))$
letting $(y,Y)=\textsf{constraint}(x_{i},\ell)$. (Note that $v_{\ell}$ exists
because $\widehat{\sigma}_{i-1}$ is satisfiable by induction hypothesis.)

Block decomposition  Towards the above goal, let us consider $w_{i}$ and
$\rho_{1}\dots\rho_{m}$ where $m=\textsf{multiplicity}(x_{i})$ and for
$\ell:1\leq\ell\leq m$, $\rho_{\ell}$ is an accepting run of the transducer
$T_{\ell}^{x_{i}}$ on the input $w_{i}$ producing
$u_{\ell}=\widehat{\sigma}_{i-1}(o_{\ell}^{x_{i}})$. This is depicted in
Figure 6. We factorize each $\rho_{\ell}$ into blocks. The number of blocks is
exactly $n+1$, where $n=|w_{i}|$. For $j>0$, the $j$th block contains the
transition on the $j$th letter of $w_{i}$, followed by all the trailing
$\epsilon$-input transitions. The very first block (block $0$), contains the
leading $\epsilon$-input transitions if present. Now, we decompose the output
of $\rho_{\ell}$ according to the blocks. That is,
$u_{\ell}=u^{0}_{\ell}u^{1}_{\ell}\cdot u^{2}_{\ell}\dots u^{n}_{\ell}$. Next
we want to identify the subword of $w_{i}$ (and subruns of $\rho_{\ell}$) that
needs to be preserved.

$\cdots$$\cdots$$\cdots$$a_{1}$$a_{2}$$a_{n}$$a_{1}$$a_{2}$$a_{n}$$a_{1}$$a_{2}$$a_{n}$$\overline{q_{0}}$$\overline{q_{1}}$$\overline{q_{2}}$$\overline{q_{n}}$${a_{1}}$${a_{2}}$$\cdots$${a_{n}}$${\rho_{1}}$${\rho_{2}}$$\vdots$${\rho_{m}}$${w}$

Figure 6: The figure describes the block decomposition of the runs of
transducers. The very first block includes the sequence of
$\epsilon$-transitions (if any) before the first letter of the input is read.
Every other block includes a transition on input letter followed by a sequence
of $\epsilon$ transitions. Blocks here are represented as overlapping
rectangles coloured in red. The transition on input is represented as a solid
arrow and a sequence of $\epsilon$ transitions is represented as a dashed
arrows.

Identifying crucial blocks and positions. Consider $v_{\ell}$, the witnessing
subword of $u_{\ell}$ for
$\widehat{\sigma}_{i-1}(y)\preceq\mathsf{Shuffle}(\widehat{\sigma}_{i-1}(Y))$
where $(y,Y)=\textsf{constraint}(x_{i},\ell)$. Fix an embedding of $v_{\ell}$
in $u_{\ell}$. If this embedding is incident111This means that the image of
the witnessing projection intersects the positions of the factor
$u^{j}_{\ell}$. on the factor $u^{j}_{\ell}$ for $j>0$, we will mark the the
$j$th block as well as the $j$th letter of $w_{i}$ as _crucial_. Since
$|\widehat{\sigma}_{i-1}(y)|\leq B_{i-1}$ (by induction hypothesis), the
number of crucial blocks in $\rho_{\ell}$ is at most $B_{i-1}$. Hence the
number of crucial positions in $w_{i}$ is at most $m\times B_{i-1}$ where
$m=\textsf{multiplicity}(x_{i})$. Notice that if we shrink $w_{i}$ to a
subword that 1) preserves the crucial positions, 2) preserves membership in
$\mathsf{Mem}(x_{i})$ and 3) yields subruns of $\rho_{\ell}$ that preserves
the crucial blocks, then the satisfiability would be preserved. Our next aim
is to obtain such a shrinking, which is sufficiently small to also satisfy the
length requirements.

Annotated parse trees Consider a grammar $G_{i}$ for $\mathsf{Mem}(x_{i})$ in
Chomsky Normal Form and a parse tree of $w_{i}$ in $G_{i}$. Annotate the nodes
of this parse-tree by pairs of $m$-tuple of states. The $m$-tuple of states
$\overline{q_{j}}$ correspond to the states of the transducers at the boundary
between $(j-1)$th block and $j$th block. A node is annotated with
$\langle\overline{q_{j-1}},\overline{q_{j^{\prime}}}\rangle$ if the yield of
the subtree rooted at that node generates the factor of $w_{i}$ from $j$th
letter to $j^{\prime}$th letter (for some $j^{\prime}\geq j$). Notice that
some of the leaves are marked as crucial. We will mark an internal node as
crucial if it is the least common ancestor of two crucial nodes.

$A,\langle\mkern 1.5mu\overline{\mkern-1.5muq_{1}\mkern-1.5mu}\mkern
1.5mu,\mkern 1.5mu\overline{\mkern-1.5muq_{2}\mkern-1.5mu}\mkern
1.5mu\rangle$$A,\langle\mkern
1.5mu\overline{\mkern-1.5muq_{1}\mkern-1.5mu}\mkern 1.5mu,\mkern
1.5mu\overline{\mkern-1.5muq_{2}\mkern-1.5mu}\mkern
1.5mu\rangle$$a_{1}$$a_{i}$$a_{i^{\prime}}$$a_{j^{\prime}}$$a_{j}$$a_{n}$$\cdots$$\cdots$$\cdots$$\cdots$$\cdots$

Figure 7: The figure illustrates the annotations of a nodes and pumping down
in a parse tree

Shrinking the parse tree Now, if there are two nodes $n_{1}$ and $n_{2}$ in
this tree such that 1) both have the same annotated non-terminal, 2) $n_{1}$
is an ancestor of $n_{2}$, 3) there are no crucial nodes in the path from
$n_{1}$ to $n_{2}$, then we replace the subtree rooted at $n_{1}$ with the
subtree rooted at $n_{2}$ (pumping down). This is illustrated in Figure 7. We
repeat this until no more pumping down is possible. The yield of this shrunk
parse tree is the required word ${w^{\prime}_{i}}$. Let us analyse the size of
${w^{\prime}_{i}}$. Any path without a crucial node is of length at most
$p^{3}t^{2m}$. Hence the _skeleton_ of the parse tree that contains all the
crucial nodes and the paths from them to the root will be of size at most
$2n_{C}\times p^{3}t^{2m}$, where $n_{C}$ is the number of crucial positions
of $w_{i}$.

Any sub tree rooted at any of the nodes of the skeleton is of size at most
$2^{p^{3}t^{2m}}$. Hence the total size of the tree is at most $2n_{C}\times
p^{3}t^{2m}\times 2^{p^{3}t^{2m}}$. Since $n_{C}\leq mB_{i-1}$, we have
$\textsf{len}(w^{\prime}_{i})\leq B_{i}$.

Shrinking the transducer runs  Note that, since the shrinking preserves the
annotations, shrinking the $\rho_{\ell}$s appropriately gives us an accepting
subrun $\rho^{\prime}_{\ell}$ that preserves the crucial blocks. The number of
blocks in $\rho^{\prime}_{\ell}$ is at most $B_{i}$. Now, we need to shrink
the size of each block as well, in order to satisfy
$\textsf{len}(u^{\prime}_{\ell})\leq 2ctB_{i}$. For this, consider the
witnessing subword of $u_{\ell}$. Note that it is still embedded in
$\textsf{out}(\rho^{\prime}_{\ell})$. If this embedding is incident on the
output of a transition we will mark this transition as crucial. Further all
the transitions that read a letter from $w^{\prime}_{i}$ are also crucial.
Note that the number of crucial transitions is at most $B_{i}+B_{i-1}$. Now,
let us shrink the run $\rho^{\prime}_{\ell}$ without losing crucial
transitions to get $\rho^{\prime\prime}_{\ell}$. The number of transitions in
$\rho^{\prime\prime}_{\ell}$ is at most $t\times(B_{i}+B_{i-1}+1)$ where $t$
is the number of states. Let
$u_{\ell}^{\prime}=\textsf{out}(\rho^{\prime\prime}_{\ell})$. Then it is easy
to see that $\textsf{len}(u^{\prime}_{\ell})\leq 2ctB_{i}$.

Finally, we can give the required $\widehat{\sigma}_{i}$. Below, $x_{j}$ comes
from $\mathcal{V}$ and $o_{\ell}^{x}$ comes from $O$.

$\widehat{\sigma}_{i}(x_{j})=\begin{cases}{w^{\prime}_{i}}&\text{ if }j=i\\\
\widehat{\sigma}_{i-1}(x_{j})&\text{ if }j\neq i\end{cases}$
$\widehat{\sigma}_{i}(o_{\ell}^{x})=\begin{cases}{u^{\prime}_{\ell}}&\text{ if
}x=x_{i}\\\ \widehat{\sigma}_{i-1}(o_{\ell}^{x})&\text{ otherwise}\end{cases}$

This establishes the proof of Lemma 5.2.

##  6  Satisfiability in NEXPTIME for regular constraints

Our approach towards an NExptime procedure is very similar to that of the
previous section. Towards this, we prove the following lemma that shows that
if there is a satisfying assignment, then there is a satisfying extended
assignment of at most exponential size. Further more, the proof of the lemma
is very similar to the proof of Lemma 5.2. We only highlight the main
differences with it here.

######  Lemma 6.1.

Let $C$ be a satisfiable acyclic regular string constraint. Then $C$ has a
satisfying extended assignment $\widehat{\sigma}$ such that
$\textsf{len}(\widehat{\sigma}(x))\leq D$ for all
$x\in\widehat{\mathcal{V}}(C)$, where $D$ is ${2^{\mathcal{O}(m\cdot
k\cdot\log t)}}$ where
$t=\max_{T\in\textsc{trset}(C)\cup\textsc{autset}(C)}\textsf{state-size}(T)$
is the maximum number of states of any transducer or the NFA occurring in $C$,
and $m,k$ are as in Theorem 5.1.

As in the previous section, to obtain a satisfying extended assignment of
exponential size, we will construct a sequence of $k$ extended assignments
$\widehat{\sigma}_{0},\widehat{\sigma}_{1},\dots,\widehat{\sigma}_{k}$ such
that for each $i\in\\{1,\dots,k\\}$, $\widehat{\sigma}_{i}$ is a satisfying
extended assignment and further for each $j\leq i$,
$\widehat{\sigma}_{i}(j)\leq D_{i}$, where $D_{i}={2^{((m+1)\cdot i\cdot\log
t+i\cdot\log m)}}$. The base case is immediate, the smallest assignment for
the variable $x_{1}$ is of size at most $t$. For the inductive case, we assume
that we have already constructed the extended assignment
$\widehat{\sigma}_{i-1}$ of appropriate size. Consider $w_{i}=a_{1}\dots
a_{n}=\widehat{\sigma}_{i-1}(x_{i})$ and $\rho_{1}\dots\rho_{m}$ where
$m=\textsf{multiplicity}(x_{i})$ and for $\ell:1\leq\ell\leq m$, $\rho_{\ell}$
is an accepting run of the transducer $T_{\ell}^{x_{i}}$ on the input $w_{i}$
producing $u_{\ell}=\widehat{\sigma}_{i-1}(o_{\ell}^{x_{i}})$. Further let
$\rho$ be a run in $\mathsf{Mem}(x_{i})$ on $w_{i}$. Now consider the block
decomposition of each $\rho_{i}$, $i\in\\{1,\dots,m\\}$ as in the previous
section and mark the crucial blocks based on the witnessing subwords. Notice
that there are at most $m\times D_{i-1}$ crucial blocks. We annotate each
input letter with the $m$-tuple of states that appears in the corresponding
block boundary, as in the previous section. Further, we mark the input letter
as crucial if the corresponding block is crucial. Now for any two input
letters $a_{i},a_{j}$, if the annotations ($m$ tuple of states) for it are the
same, there are no crucial letters between them and the states reached in
$\rho$ after reading it is the same, then we delete all the transitions
between them. Further, we also delete the corresponding blocks. Let
$\rho^{\prime}$ be a sub-run of $\rho$ and
$(\rho^{\prime}_{j})_{j\in\\{1,\dots m\\}}$ be sub-runs of
$(\rho_{j})_{j\in\\{1,\dots m\\}}$ such that no more deletions are possible.
Firstly notice that each of these are a valid runs in the respective automata.
We claim that $\textsf{len}(\textsf{out}(\rho^{\prime}_{0}))\leq D_{i}$, for
this we note that there can be at most $m\times D_{i-1}$ many crucial letters
and between any two of them there can be at most $t^{m+1}$ many letters. With
this we obtain that $\textsf{len}(\textsf{out}(\rho^{\prime}))\leq(m\times
D_{i-1}\times t^{m+1})\leq D_{i}$. The length of each $\rho^{\prime}_{j}$ for
$j\in\\{1,\dots,m\\}$ can still be very large. An analysis similar to the one
done in the previous section that shrinks any long sequence of $\epsilon$
transitions within each block, will also provide us with the required bounds
for the variables from $O$.

##  7 Discussions

###  7.1 Application: Regular abstractions and DFA sizes

Let $L$ be any language. We define the Parikh image closure ($\Pi(L)$),
downward closure ($L\downarrow$) and upward closure ($L\uparrow$) of it as
follows. Let $\Sigma=\\{a_{1},\cdots a_{n}\\}$. For any word $w\in\Sigma^{*}$,
we let
$p(w)=\langle\textsf{len}(w)_{a_{1}},\cdots,\textsf{len}(w)_{a_{n}}\rangle$
denote the Parikh image of $w$, that is, it counts the occurrences of each
letter from $\Sigma$. Here, by $\textsf{len}(w)_{a}$, we mean the number of
times $a$ occurs in $w$.

$\begin{array}[]{lr}\Pi(L)=\\{v\in\Sigma^{*}\mid\exists w\in
L,p(v)=p(w)\\}&\qquad L\downarrow=\\{v\in\Sigma^{*}\mid\exists w\in L,v\preceq
w\\}\\\ L\uparrow=\\{v\in\Sigma^{*}\mid\exists w\in L,w\preceq
v\\}\end{array}$

Efficient computability of these regular abstractions of languages of infinite
state systems is a relevant question for verification and automata theory [13,
11, 46, 12]. It is interesting to see if small automata representing these
abstractions can be computed for succinctly given infinite state systems.

We address here the case where a large pushdown system is presented as a small
pushdown system and a certain number of finite state automata (referred to as
the smaller components). Here the language of the large pushdown system is
same as the intersection of the languages of the smaller component. We argue
that the lower bound on the size of the regular abstraction holds even when
the language of a pushdown system is presented succinctly as an intersection
of smaller components.

For any $n\in\mathbb{N}$, let $L(n)$ be the language over $\Sigma=\\{0,1,a\\}$
that accepts the word $w=n_{0}o_{1}n_{1}o_{2}n_{2}\cdots n_{k}$, where
$n_{0}=0^{n}$, $n_{k}=1^{n}$, $o_{1},o_{2},\cdots o_{k}=\textsf{inc}$, then
$\textsf{len}(w)_{\textsf{inc}}=2^{n}$. From Section 4 we know that we can
construct $n$ DFAs $B_{1},B_{2},\dots B_{n}$ such that
$\bigcap_{i}L(B_{i})=\\{w\\}$. Since any DFA recognising the closure of this
language requires at least $2^{n}$ states, we have the following claim.

######  Claim 9.

Given $n$ regular languages as $n$ finite state automata, let $L$ be the
language obtained by intersecting the languages of these automata. Then, the
regular representations for Parikh image closure, downward closure and upward
closure of $L$ can be of exponential size.

Consider the language given in Claim 5 i.e. $L(A)\cap L^{\prime}_{\ell}$,
since it can recognize words with exactly $2^{2^{n}}$ many symbols from
$\Gamma_{2}$, we have the following claim.

######  Claim 10.

Given $n$ regular languages as $n$ finite state automata and a pushdown
system, let $L$ be the language got by intersecting the languages of these
automata. Then, the regular representations for Parikh image closure, downward
closure and upward closure of $L$ can be of double exponential size.

###  7.2 Concatenation instead of Shuffle

In [9] it is shown that shuffle can express concatenation with a polynomial
blow-up, but preserving acyclicity. It is interesting to see if the hardness
holds in the presence of concatenation alone. Already, in the setting of [9]
(no transductions), if acyclicity is not imposed, it is not known whether
satisfiability of the regular string constraints is decidable if only
concatenation is allowed instead of shuffle. In our setting (in the presence
of tranducers), it turns out that satisfiability is undecidable. We show this
by modifying the reduction in [9].

Let $\mathcal{P}=(\Sigma_{1},\Sigma_{2},f,g)$ be a given PCP instance, let
$\mathcal{L}_{u}=(\\{i\cdot f(i)\mid i\in\Sigma_{1}\\})^{*}$,
$\mathcal{L}_{v}=(\\{i\cdot g(i)\mid i\in\Sigma_{1}\\})^{*}$,
$\mathcal{L}_{i}=\Sigma_{1}^{+}$ and $\mathcal{L}_{s}=\Sigma_{2}^{*}$. Notice
that all these four languages are regular, let
$\mathcal{A}_{u},\mathcal{A}_{v},\mathcal{A}_{i}$ and $\mathcal{A}_{s}$ be
their corresponding NFA. Then the required string constraint is
$(\Sigma,\mathcal{V},\mathsf{Mem},\mathsf{Rel})$, where
$\mathcal{V}=\\{u,v,i,s\\}$, for any $x\in\mathcal{V}$,
$\mathsf{Mem}(x)=\mathcal{A}_{x}$. Let $T_{\Sigma}=\\{(a_{1}\dots
a_{n},\Sigma^{*}a_{1}\Sigma^{*}a_{1}\dots\Sigma^{*}a_{n}\Sigma^{*})\\}$ be the
transduction that arbitrarily inserts words from $\Sigma$. Then the set
$\mathsf{Rel}$ is given by

$\displaystyle i\preceq u$ $\displaystyle s\preceq u$ $\displaystyle u\preceq
T_{\Sigma_{1}}(s)$ $\displaystyle u\preceq T_{\Sigma_{2}}(t)$ $\displaystyle
i\preceq v$ $\displaystyle s\preceq v$ $\displaystyle v\preceq
T_{\Sigma_{1}}(s)$ $\displaystyle v\preceq T_{\Sigma_{2}}(t)$

In the case of acyclic string constraints, one may wonder if the lower bounds
hold in a setting where only concatenation is allowed instead of shuffle. This
was not discussed in [9]. Infact, in our case, the lower bound holds even when
only concatenation is allowed. Notice that, in our 2NExptime-hard reduction,
all relational constraints have only one variable in the RHS. Hence, the
2NExptime-hard holds for acyclic pushdown string constraints with transducers,
even when shuffle (or even concatenation) is disallowed.

In fact, it is not known whether the lower bounds in [9] hold for the variant
with only concatenation instead of shuffle. It is also open whether
satisfiability is decidable for the unrestricted regular string constraints
(without acyclicity restriction) when only concatenation is allowed.

##  8 Conclusions

In this paper, we considered string constraints in the presence of sub-word
relation, shuffle operator (which subsumes concatenation [9]) and transducers.
We studied this problem for two different kinds of membership constraints,
namely regular and context free. We showed that in the case when only regular
membership constraints are involved, the problem is NExptime-complete.
Whereas, when context-free membership constraints are involved, the problem is
2NExptime-complete. Towards the hardness proof, we showed how to count exactly
$2^{n}$ using $n$ finite state automata each of size $\mathcal{O}(n)$. As a
consequence of this result, we also obtained a lower bound for any regular
representation of the upward closure, downward closure and Parikh image
closure of the intersection of the language of $n$ finite state automata.
Similarly, we showed that we can count exactly $2^{2^{n}}$ using a pushdown
automaton and $n$ finite state automata, each of size $\mathcal{O}(n)$. With
this, we also obtained a lower bound for any regular representation of the
upward closure, downward closure and Parikh image closure of the intersection
language of a pushdown and $n$ finite state automata.

## References

  * [1] A. Parosh Abdulla, F. Mohamed Atig, Yu-Fang Chen, Diep Phi Bui, Lukáš Holík, Ahmed Rezine, and Philipp Rummer.  Trau : SMT solver for string constraints.  In Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, pages 165–169. FMCAD Inc., 2019.  doi:10.23919/FMCAD.2018.8602997.
  * [2] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, Denghang Hu, Wei-Lun Tsai, Zhilin Wu, and Di-De Yen.  Solving not-substring constraint with flat abstraction.  In Hakjoo Oh, editor, Programming Languages and Systems - 19th Asian Symposium, APLAS 2021, Chicago, IL, USA, October 17-18, 2021, Proceedings, Lecture Notes in Computer Science. Springer, 2021.  doi:10.1007/978-3-030-89051-3\\_17.
  * [3] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukáš Holík, Ahmed Rezine, and Philipp Rümmer.  Flatten and conquer: A framework for efficient analysis of string constraints.  In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, page 602–617, New York, NY, USA, 2017. Association for Computing Machinery.  doi:10.1145/3062341.3062384.
  * [4] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukáš Holík, Ahmed Rezine, and Philipp Rümmer.  Flatten and conquer: A framework for efficient analysis of string constraints.  SIGPLAN Not., 52(6), 2017.  doi:10.1145/3140587.3062384.
  * [5] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, and Jari Stenman.  String constraints for verification.  In Armin Biere and Roderick Bloem, editors, 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, volume 8559 of Lecture Notes in Computer Science, pages 150–166. Springer, 2014.  doi:10.1007/978-3-319-08867-9\\_10.
  * [6] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, and Jari Stenman.  Norn: An SMT solver for string constraints.  In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pages 462–469. Springer, 2015.  doi:10.1007/978-3-319-21690-4\\_29.
  * [7] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Vrunda Dave, and Shankara Narayanan Krishna.  On the separability problem of string constraints.  In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.  doi:10.4230/LIPIcs.CONCUR.2020.16.
  * [8] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bui Phi Diep, Lukás Holík, and Petr Janku.  Chain-free string constraints.  In Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza, editors, Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, volume 11781 of Lecture Notes in Computer Science. Springer, 2019.  doi:10.1007/978-3-030-31784-3\\_16.
  * [9] C. Aiswarya, Soumodev Mal, and Prakash Saivasan.  On the satisfiability of context-free string constraints with subword-ordering.  In Christel Baier and Dana Fisman, editors, LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022. ACM, 2022.  doi:10.1145/3531130.3533329.
  * [10] Roberto Amadini.  A survey on string constraint solving.  ACM Comput. Surv., 55(2):16:1–16:38, 2023.  doi:10.1145/3484198.
  * [11] Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan.  On bounded reachability analysis of shared memory systems.  In Venkatesh Raman and S. P. Suresh, editors, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, December 15-17, 2014, New Delhi, India, volume 29 of LIPIcs, pages 611–623. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014.  URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2014.611, doi:10.4230/LIPICS.FSTTCS.2014.611.
  * [12] Mohamed Faouzi Atig, Ahmed Bouajjani, and Tayssir Touili.  On the reachability analysis of acyclic networks of pushdown systems.  In Franck van Breugel and Marsha Chechik, editors, Concurrency Theory, 19th International Conference, CONCUR 2008, Toronto, Canada, August 19-22, 2008. Proceedings, volume 5201 of Lecture Notes in Computer Science. Springer, 2008.  doi:10.1007/978-3-540-85361-9\\_29.
  * [13] Mohamed Faouzi Atig, Dmitry Chistikov, Piotr Hofman, K. Narayan Kumar, Prakash Saivasan, and Georg Zetzsche.  The complexity of regular abstractions of one-counter languages.  In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016, pages 207–216. ACM, 2016.  doi:10.1145/2933575.2934561.
  * [14] Mohamed Faouzi Atig, K. Narayan Kumar, and Prakash Saivasan.  Adjacent ordered multi-pushdown systems.  In Marie-Pierre Béal and Olivier Carton, editors, Developments in Language Theory - 17th International Conference, DLT 2013, Marne-la-Vallée, France, June 18-21, 2013. Proceedings, volume 7907 of Lecture Notes in Computer Science, pages 58–69. Springer, 2013.  doi:10.1007/978-3-642-38771-5\\_7.
  * [15] Murphy Berzish, Joel D. Day, Vijay Ganesh, Mitja Kulczynski, Florin Manea, Federico Mora, and Dirk Nowotka.  Towards more efficient methods for solving regular-expression heavy string constraints.  Theor. Comput. Sci., 2023.  doi:10.1016/j.tcs.2022.12.009.
  * [16] Murphy Berzish, Vijay Ganesh, and Yunhui Zheng.  Z3str3: A string solver with theory-aware heuristics.  In Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design, FMCAD ’17, Austin, Texas, 2017. FMCAD Inc.  doi:10.23919/FMCAD.2017.8102241.
  * [17] J. Richard Büchi and Steven Senger.  Definability in the existential theory of concatenation and undecidable extensions of this theory.  Math. Log. Q., 34:337–342, 1988.
  * [18] Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu.  What is decidable about string constraints with the replaceall function.  Proc. ACM Program. Lang., 2(POPL):3:1–3:29, 2018.  doi:10.1145/3158091.
  * [19] Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu.  Solving string constraints with regex-dependent functions through transducers with priorities and variables.  Proc. ACM Program. Lang., 6(POPL), 2022.  doi:10.1145/3498707.
  * [20] Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, and Zhilin Wu.  Solving string constraints with regex-dependent functions through transducers with priorities and variables.  CoRR, abs/2111.04298, 2021.
  * [21] Taolue Chen, Matthew Hague, Jinlong He, Denghang Hu, Anthony Widjaja Lin, Philipp Rümmer, and Zhilin Wu.  A decision procedure for path feasibility of string manipulating programs with integer data type.  In Dang Van Hung and Oleg Sokolsky, editors, Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, volume 12302 of Lecture Notes in Computer Science, pages 325–342. Springer, 2020.  doi:10.1007/978-3-030-59152-6\\_18.
  * [22] Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu.  Decision procedures for path feasibility of string-manipulating programs with complex operations.  Proc. ACM Program. Lang., 3(POPL), 2019.  doi:10.1145/3290362.
  * [23] Peter Chini, Jonathan Kolberg, Andreas Krebs, Roland Meyer, and Prakash Saivasan.  On the complexity of bounded context switching.  In Kirk Pruhs and Christian Sohler, editors, 25th Annual European Symposium on Algorithms, ESA 2017, September 4-6, 2017, Vienna, Austria, volume 87 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.  doi:10.4230/LIPIcs.ESA.2017.27.
  * [24] John Corcoran, William Frank, and Michael Maloney.  String theory.  J. Symb. Log., 39(4):625–637, 1974.  doi:10.2307/2272846.
  * [25] Joel D. Day.  Word equations in the context of string solving.  In Volker Diekert and Mikhail V. Volkov, editors, Developments in Language Theory - 26th International Conference, DLT 2022, Tampa, FL, USA, May 9-13, 2022, Proceedings, Lecture Notes in Computer Science. Springer, 2022.  doi:10.1007/978-3-031-05578-2\\_2.
  * [26] Joel D. Day, Vijay Ganesh, Nathan Grewal, and Florin Manea.  On the expressive power of string constraints.  Proc. ACM Program. Lang., 7(POPL):278–308, 2023.  doi:10.1145/3571203.
  * [27] Joel D. Day, Vijay Ganesh, Paul He, Florin Manea, and Dirk Nowotka.  The satisfiability of word equations: Decidable and undecidable theories.  In Igor Potapov and Pierre-Alain Reynier, editors, Reachability Problems, pages 15–29, Cham, 2018. Springer International Publishing.
  * [28] Diego Figueira, Artur Jez, and Anthony W. Lin.  Data path queries over embedded graph databases.  In Leonid Libkin and Pablo Barceló, editors, PODS ’22: International Conference on Management of Data, Philadelphia, PA, USA, June 12 - 17, 2022, pages 189–201. ACM, 2022.  doi:10.1145/3517804.3524159.
  * [29] Vijay Ganesh, Mia Minnes, Armando Solar-Lezama, and Martin C. Rinard.  Word equations with length constraints: What’s decidable?  In Armin Biere, Amir Nahir, and Tanja E. J. Vos, editors, Hardware and Software: Verification and Testing - 8th International Haifa Verification Conference, HVC 2012, Haifa, Israel, November 6-8, 2012. Revised Selected Papers, volume 7857 of Lecture Notes in Computer Science. Springer, 2012.  doi:10.1007/978-3-642-39611-3\\_21.
  * [30] Michael R. Garey and David S. Johnson.  Computers and Intractability; A Guide to the Theory of NP-Completeness.  W. H. Freeman & Co., USA, 1990.
  * [31] Matthew Hague, Anthony Widjaja Lin, and C.-H. Luke Ong.  Detecting redundant CSS rules in HTML5 applications: a tree rewriting approach.  In Jonathan Aldrich and Patrick Eugster, editors, Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA, October 25-30, 2015, pages 1–19. ACM, 2015\.  doi:10.1145/2814270.2814288.
  * [32] Hermes Hans.  Semiotik. eine theorie der zeichengestalten als grundlage für untersuchungen von formalisierten sprachen.  Journal of Philosophy, 36(13):356–357, 1939.  doi:10.2307/2017267.
  * [33] Lukás Holík, Petr Janku, Anthony W. Lin, Philipp Rümmer, and Tomás Vojnar.  String constraints with concatenation and transducers solved efficiently.  Proc. ACM Program. Lang., 2(POPL), 2018.  doi:10.1145/3158092.
  * [34] John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman.  Introduction to Automata Theory, Languages, and Computation (3rd Edition).  Addison-Wesley Longman Publishing Co., Inc., USA, 2006.
  * [35] Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, and Micha Schrader.  Certistr: a certified string solver.  In Andrei Popescu and Steve Zdancewic, editors, CPP ’22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022. ACM, 2022.  doi:10.1145/3497775.3503691.
  * [36] Adam Kiezun, Vijay Ganesh, Shay Artzi, Philip J. Guo, Pieter Hooimeijer, and Michael D. Ernst.  Hampi: A solver for word equations over strings, regular expressions, and context-free grammars.  ACM Trans. Softw. Eng. Methodol., 21(4), feb 2013.
  * [37] Adam Kiezun, Philip J. Guo, Pieter Hooimeijer, Michael D. Ernst, and Vijay Ganesh.  Theory and practice of string solvers (invited talk abstract).  In Dongmei Zhang and Anders Møller, editors, Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2019, Beijing, China, July 15-19, 2019. ACM, 2019.  doi:10.1145/3293882.3338993.
  * [38] Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark Barrett, and Morgan Deters.  An efficient SMT solver for string constraints.  Form. Methods Syst. Des., 48(3), 2016.  doi:10.1007/s10703-016-0247-6.
  * [39] Anthony Widjaja Lin and Pablo Barceló.  String solving with word equations and transducers: towards a logic for analysing mutation XSS.  In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 123–136. ACM, 2016.  doi:10.1145/2837614.2837641.
  * [40] G S Makanin.  The problem of solvability of equations in a free smigroup.  Mathematics of the USSR-Sbornik, 32(2), 1977.  doi:10.1070/SM1977v032n02ABEH002376.
  * [41] Yu. V. Matiyasevich.  A connection between systems of words-and-lengths equations and Hilbert’s tenth problem.  Studies in constructive mathematics and mathematical logic. Part II,Zap. Nauchn. Sem. LOMI, 8, 1968.  doi:10.1070/SM1977v032n02ABEH002376.
  * [42] Wojciech Plandowski.  Satisfiability of word equations with constants is in PSPACE.  In 40th Annual Symposium on Foundations of Computer Science, FOCS ’99, 17-18 October, 1999, New York, NY, USA, pages 495–500. IEEE Computer Society, 1999.  doi:10.1109/SFFCS.1999.814622.
  * [43] W. V. Quine.  Concatenation as a basis for arithmetic.  The Journal of Symbolic Logic, 11, 1946.  doi:10.2307/2268308.
  * [44] Alfred Tarski.  Der wahrheitsbegriff in den formalisierten sprachen.  Studia Philosophica, 1:261–405, 1935.
  * [45] Jean van Heijenoort.  From Frege to Gödel : A Source Book in Mathematical Logic.  Harvard University Press, January 2002.
  * [46] Georg Zetzsche.  The complexity of downward closure comparisons.  In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 123:1–123:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.  doi:10.4230/LIPICS.ICALP.2016.123.