11institutetext:  Department of Computer Science, Loughborough University,
22institutetext: German Aerospace Center (DLR), Helmholtz Association,
33institutetext: Department of Computer Science, Kiel University,

# On Solving Word Equations Using SAT

Joel D. Day 11 Thorsten Ehlers 22 Mitja Kulczynski 33 Florin Manea 33 Dirk
Nowotka and Danny Bøgsted Poulsen 3333

###### Abstract

We present Woorpje, a string solver for bounded word equations (i.e.,
equations where the length of each variable is upper bounded by a given
integer). Our algorithm works by reformulating the satisfiability of bounded
word equations as a reachability problem for nondeterministic finite automata,
and then carefully encoding this as a propositional satisfiability problem,
which we then solve using the well-known Glucose SAT-solver. This approach has
the advantage of allowing for the natural inclusion of additional linear
length constraints. Our solver obtains reliable and competitive results and,
remarkably, discovered several cases where state-of-the-art solvers exhibit a
faulty behaviour.

##  1 Introduction

Over the past twenty years, applications of software verification have scaled
from small academic programs to finding errors in the GNU Coreutils [7]. In
principle, the employed verification strategies involve exploring the control-
flow-graph of the program, gathering constraints over program variables and
passing these constraints to a constraint solver. The primary worker of
software verification is thus the constraint solver, and the scalability of
software verification achieved by improving the efficiency of constraint
solvers. The theories supported by constraint solvers are likewise highly
influenced by the needs of software verification tools (e.g. array theory and
bitvector arithmetic). A recent need of software verification tools is the
ability to cope with equations involving string constraints, i.e. equations
over string variables composing equality between concatenation of strings and
string variables. This need arose from the desire to do sofware verification
of languages with string manipulation as a core part of the language (e.g.
JavaScript and Java) [19, 9]. Accomodating for this need, we have seen the
advent of dedicated string solvers as well as constraint solvers implementing
string solving techniques. As an incomplete list we mention HAMPI [15], CVC4
[4], Ostrich [8], Sloth [11], Norn [1], S3P [20] and Z3str3 [5].

Although the need for string solving only recently surfaced in the software
verification community, the problem is in fact older and known as _Word
Equations_ (a term that we will use from now on). The word equation
satisfiability problem is to determine whether we can unify the two strings,
i.e., transform them into two equal strings containing constant letters only,
by substituting the variables consistently by strings of constants. For
example, consider the equation defined by the two strings $XabY$ and $aXYb$,
denoted $XabY\,\dot{=}\,aXYb$, with variables $X,Y$ and constants $a$ and $b$.
It is satisfiable because $X$ can be substituted by $a$ and $Y$ by $b$, which
produces the equality $aabb=aabb$. In fact, substituting $X$ by an arbitrary
amount of $a$’s and $Y$ by an arbitrary amount of $b$’s unifies the two sides
of the equation.

The word equation problem is decidable [16] and NP-hard. In a series of works,
Jeż [13, 12] showed that word equations can be solved in non-deterministic
linear space. It has been shown by Plandowski [18] that there exists an upper
bound of $2^{2^{O(n^{4})}}$ for the smallest solution to a word equation of
length $n$. Having this in mind, a standard method for solving word equations
is known as _filling the positions_ [14, 17]. In this method a length for each
of the string variables is non-deterministically selected. Having a fixed
length of the variables reduces the problem to lining up the positions of the
two sides of the equation, and filling the unknown positions of the variables
with characters, making the two sides equal.

In this paper we present a new solver for word equation with linear length
constraints, Woorpje. In particular, it guesses the maximal length of
variables and encodes a variation of _filling the positions_ method into an
automata-construction, thereby reducing the search for a solution to a
reachability question of this automata. Preliminary experiments with a pure
automata-reachability-based approach revealed however, that this would not
scale for even small word equations. Woorpje therefore encodes the automata
into SAT and uses the tool Glucose [3] as a backend. Unlike other approaches
based on the filling the positions method (e.g. [6, 19]), Woorpje does not
need an exact bound for each variable, but only an upper bound. Experiments
indicate that Woorpje is not only reliable but also competitive to the more
mature CVC4 and Z3. Results indicate that Woorpje is quicker on pure word
equations (no linear length constraints), and that CVC4 and Z3 mainly have an
edge on word equations with linear constraints. This may be due to our naive
solution for solving linear length constraints.

##  2 Preliminaries

Let $\mathds{N}$ be the set of natural numbers, let $[n]$ be the set
$\Set{0,1,2,\ldots,n-1}$ and $[n]_{0}$ the set $[n]\setminus\Set{0}$. For a
finite set $\Delta$ of symbols, we let $\Delta^{*}$ be the set of all words
over $\Delta$ and $\varepsilon$ be the empty word. For an alphabet $\Delta$
and $a\notin\Delta$, we let $\Delta_{a}$ denote the set $\Delta\cup\Set{a}$ .
For a word we $w=x_{0}x_{1}\dots x_{n-1}$ we let $|w|=n$ refer to its length.
For $i\in\left[|w|\right]$ we denote by $w[i]$ the symbol on the $i$th
position of $w$ i.e. $w[i]=x_{i}$. For $a\in\Delta$ and $w\in\Delta^{*}$ we
let $|w|_{a}$ denote the number of $a$s in $w$. If $w=v_{1}v_{2}$ for some
words $v_{1},v_{2}\in\Delta^{*}$, then $v_{1}$ is called a prefix of $w$ and
$v_{2}$ is a suffix of $w$. In the remainder of the paper, we let
$\Xi=\Sigma\cup\Gamma$ where $\Sigma$ ($\Gamma$) is a set of symbols called
letters (variables) and $\Sigma\cap\Gamma=\emptyset$. We call a word
$w\in\Xi^{*}$ a _pattern_ over $\Xi$. For a pattern $w\in\Xi^{*}$ we let
$\operatorname{var}(w)\subseteq\Gamma$ denote the set of variables from
$\Gamma$ occurring in $w$. A _substitution_ for $\Xi$ is a morphism
$S:\Xi^{*}\to\Sigma^{*}$ with $S(a)=a$ for every $a\in\Sigma$ and
$S(\varepsilon)=\varepsilon$. Note, that to define a substitution $S$, it
suffices to define $S(X)$ for all $X\in\Gamma$.

A _word equation_ over $\Xi$ is a tuple $(u,v)\in\Xi^{*}\times\Xi^{*}$ written
$u\,\dot{=}\,v$. A substitution $S$ over $\Xi$ is a _solution_ to a word
equation $u\,\dot{=}\,v$ (denoted $S\operatorname{\models}u\,\dot{=}\,v$) if
$S(u)=S(v)$. A word equation $u\,\dot{=}\,v$ is _satisfiable_ if there exists
a substitution $S$ such that $S\operatorname{\models}u\,\dot{=}\,v$. A _system
of word equations_ is a set of word equations
$P\subseteq\Xi^{*}\times\Xi^{*}$. A system of word equations $P$ is
satisfiable if there exists a substitution $S$ that is a solution to all word
equations (denoted $S\models E$). Karhumäki et al. [14] showed that for every
system of word equations, a single equation can be constructed which is
satisfiable if and only if the initial formula was satisfiable. The solution
to the constructed word equation can be directly transferred to a solution of
the original word equation system.

##### Bounded Word Equations

A natural sub-problem of solving word equations is that of _Bounded Word
Equations_. In this problem we are not only given a word equation
$u\,\dot{=}\,v$ but also a set of length constraints $\\{\,|X|\leq b_{X}\mid
X\in\Gamma\land b_{X}\in\mathds{N}\,\\}$. The bounded word equation is
satisfiable if there exists a substitution $S$ such
$S\operatorname{\models}u\,\dot{=}\,v$ and $|S(X)|\leq b_{X}$ for each
$X\in\Gamma$. For convenience, we shall sometimes refer to the set of bounds
$b_{X}$ as a function $B:\Gamma\to\mathds{N}$ such that $b_{X}=B(X)$.

##### Word Equations with Linear Constraints

A word equation with linear constraints is a word equation $u\,\dot{=}\,v$
accompanied by a system $\theta$ of linear Diophantine equations, where the
unknowns correspond to the lengths of possible substitutions of the variables
in $\Gamma$. A word equation with linear constraints is satisfiable if there
exists a substitution $S$ such that $S\operatorname{\models}u\,\dot{=}\,v$ and
S satisfies $\theta$. Note that the bounded word equation problem is in fact a
special case of word equations with linear constraints.

##### SAT Solving

A Boolean formula $\varphi$ with finitely many Boolean variables
$\operatorname{var}(\varphi)=\Set{x_{1},\dots,x_{n}}$ is usually given in
conjunctive normal form. This is a conjunction over a set of disjunctions
(called clauses), i.e. $\varphi=\bigwedge_{i}\bigvee_{j}l_{i,j}$, where
$l_{i,j}\in\bigcup_{i\in[n]}\Set{x_{i},\lnot x_{i}}$ is a literal. A mapping
$\beta:\operatorname{var}(\varphi)\rightarrow\Set{0,1}$ is called an
_assignment_ ; for such an assignment, the literal $l$ evaluates to true if
and only if $l=x_{i}$ and $\beta(x_{i})=1$, or $l=\lnot x_{i}$ and
$\beta(x_{i})=0$. A clause inside a formula in conjunctive normal form is
evaluated to true if at least one of its literals evaluates true. We call a
formula $\varphi$ _satisfied_ (under an assignment) if all clauses are
evaluated to true. If there does not exists a satisfying assignment, $\varphi$
is unsatisfiable.

##  3 Word equation solving

In this section we focus on solving _Bounded Word Equations_ and _Word
Equations with Linear Constraints_. We proceed by first solving bounded word
equations, and secondly, we discuss a minor change, that allows solving word
equations with linear constraints.

###  3.1 Solving Bounded Word Equation

Recall that a bounded word equation consists of a word equation
$u\,\dot{=}\,v$ along with a set of equations $\\{|X|\leq b_{X}\\}$ providing
upper bounds for the solution of each variable $X$s. In our approach we use
these bounds to create a finite automaton which has an accepting run if and
only if the bounded word equation is satisfiable.

Before the actual automata construction, we need some convenient
transformations of the word equation itself. For a variable $X$ with length
bound $b_{X}$, we replace $X$ with a sequence of new ‘filled variables’
$X^{(0)}\cdots X^{(b_{X}-1)}$ which we restrict to only be substituted by
either a single letter or the empty word. A pattern containing only filled
variables, as well as letters, is called a filled pattern. For a pattern
$w\in\Xi^{*}$ we denote its corresponding filled pattern by $w_{\xi}$. In the
following, we refer to the alphabet of filled variables by $\Gamma_{\xi}$ and
by $\Xi_{\xi}=\Sigma\cup\Gamma_{\xi}$ the alphabet of the filled patterns. Let
$S:\Xi^{*}\rightarrow\Sigma^{*}$ be a substitution for $w\in\Xi^{*}$. We can
canonically define the induced substitution for filled patterns as
$S_{\xi}:\left(\Sigma\cup\Gamma_{\xi}\right)\rightarrow\Sigma_{\lambda}$ with
$S_{\xi}(a)=S(a)$ for all $a\in\Sigma$, $S_{\xi}(X^{(i)})=S(X)[i]$ for all
$X^{(i)}\in\Gamma_{\xi}$ and $i<|S(X)|$, and $S_{\xi}(X^{(j)})=\lambda$ for
all $X^{(j)}\in\Gamma_{\xi}$ and $|S(X)|\leq j<b_{X}$. Here, $\lambda$ is a
new symbol ($\lambda\notin\Xi_{\xi}$) to indicate an unused position at the
end of a filled variable. Note that the substitution of a single filled
variable always maps to exactly one character from $\Sigma_{\lambda}$, and, as
soon as we discover $S_{\xi}\left(X^{(j)}\right)=\lambda$ for
$j\in\left[b_{X}\right]$ it also holds that
$S_{\xi}\left(X^{(i)}\right)=\lambda$ for all $j\leq i<b_{X}$. In a sense, the
new element $\lambda$ behaves in the same way as the neutral element of the
word monoid $\Sigma^{*}$, being actually a place holder for this element
$\varepsilon$. In the other direction, if we have found a satisfying filled
substitution to our word equation, the two filled patterns obtained from the
left hand side and the right hand side of an equation, respectively, we can
transform it to a substitution for our original word equation by defining
$S(X)$ as the concatenation $S_{\xi}\left(X^{(0)}\right)\dots
S_{\xi}\left(X^{(i)}\right)$ in which each occurrence of $\lambda$ is replaced
by the empty word $\varepsilon$, for all $X\in\Gamma$ and $i\in[b_{X}]$.

Our goal is now to build an automaton which calculates a suitable substitution
for a given equation. During the calculation there are situations where a
substitution does not form a total function. To extend a partial substitution
$S:\Xi\mathrel{\ooalign{\hfil$\mapstochar$\hfil\cr$\to$\cr}}\Sigma^{*}$ we
define for $X\in\Xi$ and $b\in\Sigma^{*}$ the notation
$S\left[\frac{X}{b}\right]=S\cup\Set{X\mapsto b}$ whenever $S(X)$ is undefined
and otherwise $S\left[\frac{X}{b}\right]=S$. This definition can be naturally
applied to filled substitutions. We define a congruence relation which sets
variables and letters in relation whenever their substitution with respect to
a partial substitution $S_{\xi}$ is equal or undefined. For all
$a,b\in\Xi_{\xi}\cup\\{\lambda\\}$ we define

$a\overset{S_{\xi}}{\sim}b\text{ iff
}S_{\xi}\left(a\right)=S_{\xi}\left(b\right)\text{ or
}S_{\xi}\left(b\right)\notin\Sigma^{*}_{\lambda}\text{ or
}S_{\xi}\left(a\right)\notin\Sigma^{*}_{\lambda}.$

###### Definition 1

For a word equation $u\,\dot{=}\,v$ for $u,v\in\Xi^{*}$ and a mapping
$B:\Gamma\rightarrow\mathds{N}$ defining the bounds $B(X)=b_{X}$, We define
the _equation automaton_ $A(u\,\dot{=}\,v,B)=(Q,\delta,I,F)$ where
$Q=\left([|u_{\xi}|+1]\times[|v_{\xi}|+1]\right)\times\left(\Xi_{\xi_{\lambda}}\mathrel{\ooalign{\hfil$\mapstochar$\hfil\cr$\to$\cr}}\Sigma_{\lambda}\right)$
is a set of states consisting of two integers which indicate the position
inside the two words $u_{\xi}$ and $v_{\xi}$ and a partial substitution, the
transition function $\delta:Q\times\Sigma_{\lambda}\rightarrow Q$ defined by

$\delta\left(\left(\left(i,j\right),S\right),a\right)=\begin{cases}\left(\left(i+1,j+1\right),S\left[\frac{u_{\xi}[i]}{a}\right]\left[\frac{v_{\xi}[j]}{a}\right]\right)&\text{if
$u_{\xi}[i]\overset{S_{\xi}}{\sim}v_{\xi}[j]\overset{S_{\xi}}{\sim}a$,}\\\
\left(\left(i+1,j\right),S\left[\frac{u_{\xi}[i]}{\lambda}\right]\right)&\text{if
$u_{\xi}[i]\overset{S_{\xi}}{\sim}\lambda=a$,}\\\
\left(\left(i,j+1\right),S\left[\frac{v_{\xi}[j]}{\lambda}\right]\right)&\text{if
$v_{\xi}[j]\overset{S_{\xi}}{\sim}\lambda=a$.}\end{cases}$

an initial state $I=\left(\left(0,0\right),\Set{a\mapsto
a}{a\in\Sigma_{\lambda}}\right)$ and the set of final states
$F=\Set{\left(\left(i,j\right),S_{\xi}\right)}{i=|u_{\xi}|,j=|v_{\xi}|}$.

The state space of our automaton is finite since the filled substitution
$S_{\xi}$ maps each input to exactly one character in $\Sigma$. The automaton
is nondeterministic, as the three choices we have for a transition are not
necessarily mutually exclusive.

As an addition to the above definition, we introduce the notion of location as
a pair of integers $(i,j)$ corresponding to two positions inside the two words
$u_{\xi}$ and $v_{\xi}$. A location $(i,j)$ can also be seen as the set of
states of the form $((i,j),S)$ for all possible partial substitutions $S$.

A run of the above nondeterministic automaton constructs a partial
substitution for the given equation which is extended with each change of
state. The equation has a solution if one of the accepting states
$(|u_{\xi}|,|v_{\xi}|,S)$, where $S$ is a total substitution, is reachable,
because the automaton simulates a walk through our input equation left to
right, with all its positions filled in a coherent way.

###### Example 1

Consider the equation $u\,\dot{=}\,v$ for $u=aZXb,v=aXaY\in\Xi^{*}$. We choose
the bounds $b_{X}=b_{Y}=b_{Z}=1$. This will give us the words
$u_{\xi}=aZ^{(0)}X^{(0)}b$ and $v_{\xi}=aX^{(0)}aY^{(0)}$. Fig. 1 visualizes
the corresponding automaton.

$a$$Z^{(0)}$$X^{(0)}$$b$$a$$X^{(0)}$$a$$Y^{(0)}$$(0,0)$$S_{i}$$(1,1)$$S_{i}$$(2,1)$$S_{i}\left[\frac{Z^{(0)}}{\lambda}\right]$$(1,2)$$S_{i}\left[\frac{X^{(0)}}{\lambda}\right]$$(2,2)$$S_{i}\left[\frac{Z^{(0)}}{\lambda}\right]\left[\frac{X^{(0)}}{\lambda}\right]$$S_{i}\left[\frac{Z^{(0)}}{a}\right]\left[\frac{X^{(0)}}{a}\right]$$S_{i}\left[\frac{Z^{(0)}}{b}\right]\left[\frac{X^{(0)}}{b}\right]$$(3,2)$$S_{i}\left[\frac{Z^{(0)}}{\lambda}\right]\left[\frac{X^{(0)}}{\lambda}\right]$$(2,3)$$S_{i}\left[\frac{Z^{(0)}}{a}\right]\left[\frac{X^{(0)}}{\lambda}\right]$$(3,3)$$S_{i}\left[\frac{Z^{(0)}}{a}\right]\left[\frac{X^{(0)}}{a}\right]$$S_{i}\left[\frac{Z^{(0)}}{a}\right]\left[\frac{X^{(0)}}{\lambda}\right]$$(4,4)$$S_{i}\left[\frac{Z^{(0)}}{a}\right]\left[\frac{X^{(0)}}{a}\right]\left[\frac{Y^{(0)}}{b}\right]$$S_{i}\left[\frac{Z^{(0)}}{a}\right]\left[\frac{X^{(0)}}{\lambda}\right]\left[\frac{Y^{(0)}}{b}\right]$$a$$\lambda$$\lambda$$\lambda$$a$$b$$a$$\lambda$$a$$\lambda$$b$$b$

Figure 1: Automaton for the word equation $aZXb\,\dot{=}\,aXaY$, with the
states grouped according to their locations. Only reachable states are shown.

A run starting with the initial substitution $S_{i}=\Set{a\mapsto
a}{a\in\Sigma_{\lambda}}$ reaching one of the final states gives us a solution
to the equation. In this example we get the substitutions $Z\mapsto a,X\mapsto
a,Y\mapsto b$ and $Z\mapsto a,X\mapsto\varepsilon,Y\mapsto b$.

###### Theorem 3.1

Given a bounded word equation $u\,\dot{=}\,v$ for $u,v\in\Xi^{*}$,with bounds
$B$, then the automaton $A(u\,\dot{=}\,v,B)$ reaches an accepting state if and
only if there exists $S$ such that $S\operatorname{\models}u\,\dot{=}\,v$ and
$|S(X)|\leq B(X)$ for all $X\in\Gamma$.

#### SAT Encoding

We now encode the solving process into propositional logic. For that we impose
an ordering on the finite alphabets $\Sigma=\Set{a_{0},\dots,a_{n-1}}$ and
$\Gamma=\Set{X_{0},\dots,X_{m-1}}$ for $n,m\in\mathds{N}$. Using the upper
bounds given for all variables $X\in\Gamma$, we create the filled variables
alphabet $\Gamma_{\xi}$. Further, we create the Boolean variables
$\mathsf{K}^{a}_{X^{(i)}}$, for all $X^{(i)}\in\Gamma_{\xi}$,
$a\in\Sigma_{\lambda}$ and $i\in[b_{X}]$. Intuitively, we want to construct
our formula such that an assignment $\beta$ sets $\mathsf{K}^{a}_{X^{(i)}}$ to
$1$, if the solution of the word equation, which corresponds to the assignment
$\beta$, is such that at position $i$ of the variable $X$ an $a$ is found,
meaning $S_{\xi}\left(X^{(i)}\right)=a$. To make sure
$\mathsf{K}^{a}_{X^{(i)}}$ is set to $1$ for exactly one
$a\in\Sigma_{\lambda}$ we define the clause
$\bigvee_{a\in\Sigma_{\lambda}}\mathsf{K}^{a}_{X^{(i)}}$ which needs to be
assigned true, as well the constraints
$\mathsf{K}^{a}_{X^{(i)}}\rightarrow\lnot\mathsf{K}^{b}_{X^{(i)}}$, for all
$a,b\in\Sigma_{\lambda},X\in\Gamma,i\in[b_{X}]$ where $a\neq b$, which also
need to be all true.

To match letters we add the variables $\mathsf{C}_{a,a}\leftrightarrow\top$
and $\mathsf{C}_{a,b}\leftrightarrow\bot$ for all $a,b\in\Sigma_{\lambda}$
with $a\neq b$. As such, the actual encoding of our equation can be defined as
follows: for $w\in\Set{u_{\xi},v_{\xi}}$ and each position $i$ of $w$ and
letter $a\in\Sigma_{\lambda}$ we introduce a variable which is true if and
only if $w[i]$ will correspond to an $a$ in the solution of the word equation.
More precisely, we make a distinction between constant letters and variable
positions and define:
$\mathsf{word}_{w[i]}^{a}\leftrightarrow\mathsf{C}_{w[i],a}$ if
$w[i]\in\Sigma_{\lambda}$ and
$\mathsf{word}_{w[i]}^{a}\leftrightarrow\mathsf{K}^{a}_{w[i]}$ if
$w[i]\in\Gamma_{\xi}$. The equality of two characters, corresponding to
position $i$ in $u$ and, respectively, $j$ in $v$, is encoded by introducing a
Boolean variable
$\mathsf{wm}_{i,j}\leftrightarrow\bigvee_{a\in\Sigma_{\lambda}}\mathsf{word}_{u[i]}^{a}\land\mathsf{word}_{v[j]}^{a}$
for appropriate $i\in[|u_{\xi}|]$, $j\in[|v_{\xi}|]$.

Based on this setup, each location of the automaton is assigned a Boolean
variable. As seen in 1 we process both sides of the equation simultaneously,
from left to right. As such, for a given equation $u\,\dot{=}\,v$ we create
$n\cdot m=\left(|u_{\xi}|+1\right)\cdot\left(|v_{\xi}|+1\right)$ many Boolean
variables $\mathsf{S}_{i,j}$ for $i\in[n]$ and $j\in[m]$. Each variable
corresponds to a location in our automaton. The location $(0,0)$ is our
initial location and $(|u_{\xi}|,|v_{\xi}|)$ our accepting location. The goal
is to find a path between those two locations, or, alternatively, a satisfying
assignment $\beta$, which sets the variables corresponding to these locations
to $1$. Every path between the location $(0,0)$ and another location
corresponds to matching prefixes of $u$ and $v$, under proper substitutions.
We will call locations where an assignment $\beta$ sets a variable
$\mathsf{S}_{i,j}$ to $1$, active locations. Our transitions are now defined
by a set of constraints. We fix $i\in[n]$ and $j\in[m]$ in the following. The
constraints are given as follows: The first constraint (1) ensures that every
active location has at least one active successor. The next three constraints
(2)-(4) ensure the validity of the paths we follow: from a location we can
only proceed to exactly one other location, in order to find a satisfying
assignment; therefore we disallow simultaneous steps in multiple directions.
In (5),(6) we forbid using an $\lambda$-transition whenever there is another
possibility of moving forward. In the same manner we proceed in the case of
two matching $\lambda$ in (7); this part is especially important for finding
substitutions which are smaller than the given bounds. The idea applies in the
same way for matching letters, whose encoding is given in (8). The actual
transitions which are possible from one state to another are encoded in (9) by
using our Boolean variables $\mathsf{wm}_{i,j}$ which are true for matching
positions in the two sides of the equation. This constraint allows us to move
forward in both words if there was a match of two letters in the previous
location. When the transitions are pictured as movements in the plane, this
corresponds to a diagonal move. A horizontal or vertical move corresponds to a
match with the empty word. The last constraint (10) ensures a valid
predecessor. This is supposed to help the solver in deciding the
satisfiability of the obtained formula, i.e., to guide the search in an
efficient way. It can be seen as a local optimization step.

$\displaystyle\mathsf{S}_{i,j}\rightarrow\mathsf{S}_{i+1,j}\lor\mathsf{S}_{i,j+1}\lor\mathsf{S}_{i+1,j+1}$
(1)
$\displaystyle\left(\mathsf{S}_{i,j}\land\mathsf{S}_{i,j+1}\right)\rightarrow\left(\lnot\mathsf{S}_{i+1,j+1}\land\lnot\mathsf{S}_{i+1,j}\right)$
(2)
$\displaystyle\left(\mathsf{S}_{i,j}\land\mathsf{S}_{i+1,j}\right)\rightarrow\left(\lnot\mathsf{S}_{i+1,j+1}\land\lnot\mathsf{S}_{i,j+1}\right)$
(3)
$\displaystyle\left(\mathsf{S}_{i,j}\land\mathsf{S}_{i+1,j+1}\right)\rightarrow\left(\lnot\mathsf{S}_{i,j+1}\land\lnot\mathsf{S}_{i+1,j}\right)$
(4)
$\displaystyle\mathsf{S}_{i,j}\land\lnot\mathsf{word}_{u[i]}^{\lambda}\rightarrow\lnot\mathsf{S}_{i+1,j}\text{
and
}\mathsf{S}_{i,j}\land\mathsf{word}_{u[i]}^{\lambda}\land\lnot\mathsf{word}_{v[j]}^{\lambda}\rightarrow\mathsf{S}_{i+1,j}$
(5)
$\displaystyle\mathsf{S}_{i,j}\land\lnot\mathsf{word}_{v[j]}^{\lambda}\rightarrow\lnot\mathsf{S}_{i,j+1}\text{
and
}\mathsf{S}_{i,j}\land\lnot\mathsf{word}_{u[i]}^{\lambda}\land\mathsf{word}_{v[j]}^{\lambda}\rightarrow\mathsf{S}_{i,j+1}$
(6)
$\displaystyle\mathsf{S}_{i,j}\land\mathsf{word}_{u[i]}^{\lambda}\land\mathsf{word}_{v[j]}^{\lambda}\rightarrow\mathsf{S}_{i+1,j+1}$
(7)
$\displaystyle\mathsf{S}_{i,j}\land\mathsf{S}_{i+1,j+1}\rightarrow\mathsf{wm}_{i,j}$
(8)
$\displaystyle\mathsf{S}_{i,j}\leftrightarrow\left(\mathsf{S}_{i-1,j-1}\land\mathsf{wm}_{i-1,j-1}\right)\lor\left(\mathsf{S}_{i,j-1}\land\lnot\mathsf{wm}_{i,j-1}\right)\lor\left(\mathsf{S}_{i-1,j}\land\lnot\mathsf{wm}_{i-1,j}\right)$
(9)
$\displaystyle\mathsf{S}_{i+1,j+1}\rightarrow\mathsf{S}_{i,j}\lor\mathsf{S}_{i+1,j}\lor\mathsf{S}_{i,j+1}$
(10)

The final formula is the conjunction of all constraints defined above. This
formula is true iff location $(n,m)$ is reachable from location $(0,0)$, and
this

Figure 2: Solver computation on $XaXbYbZ\,\dot{=}\,aXY\\-YbZZbaa$

is true iff the given word equation is satisfiable w.r.t. the given length
bounds.

###### Lemma 1

Let $u\,\dot{=}\,v$ be a word equation, $B$ be the function giving the bounds
for the word equation variable, and $\varphi$ the corresponding formula
consisting of the conjunction (1) - (10) and the earlier defined constraints
in this section, then
$\varphi\land\mathsf{S}_{0,0}\land\mathsf{S}_{|u_{\xi}|,|v_{\xi}|}$ has a
satisfying assignment if and only if $A(u\,\dot{=}\,v,B)$ reaches an accepting
state.

###### Example 2

Consider the word equation $u\,\dot{=}\,v$ where $u=XaXbYbZ$ and
$v=aXYYbZZbaa\in\Xi^{*}$ where $\Sigma=\Set{a}$ and $\Gamma=\Set{X,Y,Z}$.
Using the approach discussed above, we find the solution $S(X)=aaaaaaaa$,
$S(Y)=aaaa$ and $S(Z)=aa$ using the bounds $b_{X}=8$ and $b_{Y}=b_{Z}=6$. We
set up an automaton with $32\cdot 38=1216$ states to solve the equation. In
Fig. 2 we show the computation of the SAT-Solver. Light grey markers indicate
states considered in a run of the automaton. In this case only $261$ states
are needed. The dark grey markers visualize the actual path in the automaton
leading to the substitution. Non-diagonal stretches are $\lambda$ transitions.

###  3.2 Refining Bounds and Guiding the Search

Initial experiments revealed a major inefficiency of our approach: most of the
locations were not used during the search and only increased the encoding
time. The many white markers in Fig. 2 indicating unused locations visualizes
the problem. Since we create all required variables $x\in\Gamma$ and
constraints for every position $i<b_{X}$, we can reduce the automaton size by
lowering these upper bounds. Abstracting a word equation by the length of the
variables gives us a way to refine the bounds $b_{X}$ for some of the
variables $X\in\Gamma$. By only considering length we obtain a Diophantine
equation in the following manner. We assume an ordering on the variable
alphabet $\Gamma=\Set{X_{0},\dots,X_{n-1}}$. We associate to each word
equation variable $X_{j}$ an integer variable $I_{j}$.

###### Definition 2

For a word equation $u\,\dot{=}\,v$ with $\Gamma=\Set{X_{0},\dots,X_{n-1}}$ we
define its _length abstraction_ by
$\sum_{j\in[n]}\left(|u|_{X_{j}}-|v|_{X_{j}}\right)\cdot
I_{j}=\sum_{a\in\Sigma}|v|_{a}-|u|_{a}$ for $j\in[n]$.

If a word equation has a solution $S$, then so does its length abstraction
with variable $I_{j}=|S(X_{j})|$. Our interest is computing upper bounds for
each variable $X_{k}\in\Gamma$ relative to the upper bounds of the bounded
word equation problem. To this end consider the following natural deductions

$\displaystyle\sum_{j\in[n]}\left(|u|_{X_{j}}-|v|_{X_{j}}\right)\cdot
I_{j}=\sum_{a\in\Sigma}\left(|v|_{a}-|u|_{a}\right)$
$\displaystyle\Longleftrightarrow~{}$ $\displaystyle
I_{k}=\frac{\sum_{a\in\Sigma}\left(|v|_{a}-|u|_{a}\right)}{|u|_{X_{k}}-|v|_{X_{k}}}-\frac{\sum_{j\in[n]\setminus
k}\left(|u|_{X_{j}}-|v|_{X_{j}}\right)\cdot I_{j}}{|u|_{X_{k}}-|v|_{X_{k}}}$
$\displaystyle\Longrightarrow~{}$ $\displaystyle
I_{k}\leq\frac{\sum_{a\in\Sigma}|v|_{a}-|u|_{a}}{\left(|u|_{X_{k}}-|v|_{X_{k}}\right)}-\frac{\sum_{j\in\kappa}\left(|u|_{X_{j}}-|v|_{X_{j}}\right)\cdot
b_{X_{j}}}{\left(|u|_{X_{k}}-|v|_{X_{k}}\right)}=b^{\mathsf{S}}_{X_{k}},$

where
$\kappa=\set{m\in[n]\setminus{k}\mid(}{u|_{X_{k}}-|v|_{X_{k}})\cdot(|u|_{X_{m}}-|v|_{X_{m}})<0}$.
Whenever $0<b^{\mathsf{S}}_{X_{k}}<b_{X_{k}}$ holds, we use
$b^{\mathsf{S}}_{X_{k}}$ instead of $b_{x_{k}}$ to prune the search space.

The length abstraction is also useful because it might give information about
the unsatisfiability of an equation: if there is no solution to the
Diophantine equation, there is no solution to the word equation. We use this
acquired knowledge and directly report this fact. Unfortunately whenever
$|u|_{X}-|v|_{X}=0$ holds for a variable $X$ we cannot refine the bounds, as
they are not influenced by the above Diophantine equation.

##### Guiding the Search

The length abstraction used to refine upper bounds can also be used to guide
the search in the automaton. In particular it can restrict allowed length of
one variable based on the length of others. We refer to the coefficient of
variable $I_{j}$ in 2 by
$\mathsf{Co}_{u,v}(X_{j})=\left(|u|_{X_{j}}-|v|_{X_{j}}\right)$.

To benefit from the abstraction of the word equation inside our propositional
logic encoding we use Reduced Ordered Multi-Decision Diagrams (MDD) [2]. An
MDD is a directed acyclic graph, with two nodes having no outgoing edges
(called true and false terminal nodes). A Node in the MDD is associated to
exactly one variable $I_{j}$, and has an outgoing edge for each element of
$I_{j}$s domain. In the MDD, a node labelled $I_{j}$ is only connected to
nodes labelled $I_{j+1}$. A row ($\mathsf{r}(I_{j})$) in an MDD is a a subset
of nodes corresponding to a certain variable $I_{j}$.

We create the MDD following 2. The following definition creates the rows of
the MDD recursively. An MDD node is a tuple consisting of a variable $I_{j}$
and an integer corresponding the partial sum which can be obtained using the
coefficients and position information of all previous variables $I_{k}$ for
$k<j$. We introduce a new variable $I_{-1}$ labelling the initial node of the
MDD. The computation is done as follows:

$\displaystyle\mathsf{r}(I_{i})=\\{\;(I_{i},s+k\cdot\mathsf{Co}_{u,v}(X_{i}))\;|\;$
$\displaystyle
s\in\Set{s^{\prime}}{(I_{i-1},s^{\prime})\in\mathsf{r}(I_{i-1})},k\in[b_{X_{i}}]\;\\}$
(11)

and $\mathsf{r}(I_{-1})=\Set{(I_{-1},0)}$. Since $I_{j}$ is associated to word
equation $X_{j}$, we let $\mathsf{r}(X_{j})=\mathsf{r}(I_{j})$. The whole set
of nodes in the MDD we denote by
$M^{C}=\bigcup_{X\in\Gamma\cup\Set{X_{-1}}}\mathsf{r}(X)$. The $\mathtt{true}$
node of the MDD is $(I_{n-1},\mathsf{s_{\\#}})$, where
$\mathsf{s_{\\#}}=\sum_{a\in\Sigma}|v|_{a}-|u|_{a}$. If the initial creation
of nodes did not add this node, the given equation (2) is not satisfiable
hence the word equation has no solution given the set bounds. Furthermore
there is no need to encode the full MDD, when only a subset of its nodes can
reach $(I_{n-1},\mathsf{s_{\\#}})$. For reducing the MDD nodes to this subset,
we calculate all predecessors of a given node $(I_{i},s)\in M^{C}$ as follows

$\mathsf{pred}((I_{i},s))=\Set{(I_{i-1},s^{\prime})}{s^{\prime}=s-k\cdot\mathsf{Co}_{u,v}(X_{i-1}),k\in[b_{X_{i-1}}]}.$

The minimized set $M=F(T)$ of reachable nodes starting at the only accepting
node $T=\Set{(I_{n},\mathsf{s_{\\#}})}$ is afterwards defined through a fixed
point by

$\displaystyle T\subseteq F(T)\land\left(\forall\;p\in
F(T):q\in\mathsf{pred}(p)\land q\in M^{C}\Rightarrow q\in F(T)\right)$ (12)

We continue by encoding this into a Boolean formula. For that we need
information on the actual length of a possible substitution. We reuse the
Boolean variables of our filled variables $X\in\Gamma_{\xi}$. The idea is to
introduce $b_{X}+1$ many Boolean variables
$(\mathsf{OH}_{i}(0)\dots\mathsf{OH}_{i}(b_{X}+1))$ for each $X_{i}\in\Gamma$,
where $\mathsf{OH}_{i}(j)$ is true if and only if $X_{i}$ has length $j$ in
the acutal substitution. To achieve this we add a constraint forcing
substitutions to have all $\lambda$ in the end. We force our solver to adapt
to this by adding clauses
$\mathsf{K}^{\lambda}_{X^{(j)}}\rightarrow\mathsf{K}^{\lambda}_{X^{(j+1)}}$
for all $j\in[b_{X_{i}}-1]$ and $X_{i}^{(j)}\in\Gamma_{\xi}$. The actual
encoding is done by adding the constraints
$\mathsf{OH}_{i}(0)\leftrightarrow\mathsf{K}^{\lambda}{X_{i}^{(0)}}$ and
$\mathsf{OH}_{i}(b_{X_{i}})\leftrightarrow\lnot\mathsf{K}^{\lambda}_{X^{(b_{X_{i}}-1)}}$,
which fixes the edge cases for the substitution by the empty word and no
$\lambda$ inside it. For all $j\in[b_{X_{i}}]_{0}$, we add the constraints
$\mathsf{OH}_{i}(j)\leftrightarrow\mathsf{K}^{\lambda}_{X_{i}^{(j)}}\land\lnot\mathsf{K}^{\lambda}_{X_{i}^{(j-1)}}$,
which marks the first occurrence of $\lambda$.

The encoding of the MDD is done nodewise by associating a Boolean variable
$\mathsf{M}_{i,j}$ for each $i\in[|\Gamma|]$, where $(I_{i},j)\in M$. Our goal
is now to find a path inside the MDD from node $(I_{-1},0)$ to
$(I_{n-1},\mathsf{s_{\\#}})$. Therefore we enforce a true assignment for the
corresponding variables $\mathsf{M}_{-1,0}$ and
$\mathsf{M}_{{n-1},\mathsf{s_{\\#}}}$. A valid path is encoded by the
constraint
$\mathsf{M}_{i-1,j}\land\mathsf{OH}_{i}(k)\rightarrow\mathsf{M}_{i,s}$ for
each variable $X_{i}\in\Gamma$, $k\in[b_{X_{i}}]_{0}$, where
$s=j+k\cdot\mathsf{Co}_{u,v}(X_{i})$ and $(I_{i},s)\in M$. This encodes the
fact that whenever we are at a node $(I_{i-1},s)\in M$ and the substitution
for a variable $X_{i}$ has length $k$ ($|S(X_{i})|=k$), we move on to the next
node, which corresponds to $X_{i}$ and an integer obtained by taking the
coefficient of the variable $X_{i}$, multiplying it by the substitution
length,

$(X_{-1},0)$$(X_{1},0)$$(X_{2},-1)$$(X_{2},0)$$(X_{2},-2)$$(X_{3},0)$
$0+0\cdot 0$ $0+1\cdot 0$ $0+2\cdot 0$
$0+0\cdot-1$$0+1\cdot-1$$0+2\cdot-1$$0+0\cdot 1$$-1+1\cdot 1$$-2+2\cdot 1$

Figure 3: The MDD for $aX_{1}aX_{2}\,\dot{=}\,aX_{3}X_{1}b$

and adding it to the previous partial sum $s$. Whenever there is only one
successor to a node $(I_{i},j)$ within our MDD, we directly force its
corresponding one hot encoding to be true by adding
$\mathsf{M}_{i-1,j}\rightarrow\mathsf{OH}_{i}(j)$. This reduces the amount of
guesses on variables.

###### Example 3

Consider the equation $u\,\dot{=}\,v$ for
$u=aX_{1}aX_{2},v=aX_{3}X_{1}b\in\Xi^{*}$, where $\Sigma=\Set{a,b}$ and
$\Gamma=\Set{X_{1},X_{2},X_{3}}$. The corresponding linear equation therefore
has the form $0\cdot I_{1}-I_{2}+I_{3}=0$ which gives us the coefficients
$\mathsf{Co}_{u,v}(X_{1})=0$, $\mathsf{Co}_{u,v}(X_{2})=-1$ and
$\mathsf{Co}_{u,v}(X_{3})=1$. For given bounds
$b_{X_{1}}=b_{X_{2}}=b_{X_{3}}=2$ the reduced MDD has the form shown in Fig.
3. We only draw transitions which are transitively connected to the true
terminal node. The solver returns the substitution $S(X_{1})=\varepsilon$,
$S(X_{2})=b$ and $S(X_{3})=a$. Therefore it took the path marked in dark grey
inside the MDD.

##### Adding Linear Length Constraints

Until now we have only concerned ourselves with bounded word equations. As
mentioned in the introduction however, bounded equations with linear
constraints are of interest as well. In particular, without loss of generality
we restrict to linear constraints of the form [2]
$c_{0}I_{0}+\cdots+c_{n-1}I_{n-1}\leq c$ where $c,c_{i}\in\mathds{Z}$ are
integer coefficents and $I_{i}$ are integer variables with a domain
$D_{i}=\Set{m\in\mathds{Z}}{-d_{i}\leq m\leq d_{i}}$ and a corresponding
$d_{i}\in\mathds{Z}$. Each $I_{i}$ corresponds to the length of a substitution
to a variable of the given word equation.

Notice that the structure of the linear length constraint is similar to that
of 2. For handling linear constraints we can adapt the generation of MDD nodes
to keep track the partial sum of the linear constraint, and define the
accepting node of the MDD to one where all rows have been visited and the
inequality is true. We simply extend the set $T$ which was used in the fix
point iteration in (12) to the set $T=\Set{(I_{n},s)}{(I_{n},s)\in M^{C}\land
s\leq\mathsf{s_{\\#}}}$.

##  4 Experiments

Preprocessing Encoding SAT-Solver InputModelWoorpjeunsatsatsatunsatunknown

Figure 4: Architecture of Woorpje

The approach described in the previous sections has been implemented in the
tool Woorpje. The inner workings of Woorpje is visualised in Fig. 4. Woorpje
first has a preprocessing step where obviously satisfiable/unsatisfiable word
equations are immediately reported. After the preprocessing step, Woorpje
iteratively encodes the word equation into a propositional logic formula and
solves it with Glucose [3] for increasing maximal variable lengths ($i^{2}$,
where $i$ is the current iteration). If a solution is found, it is reported.
The maximal value of $i$ is user definable, and by default set to $2^{n}$
where $n$ is the length of the given equation. If Woorpje reaches the given
bound without a verdict, it returns unknown.

We have run Woorpje and state of the art word equation solvers (CVC4 1.6, Norn
1.0.1, Sloth 1.0, Z3 4.8.4) on several word equation benchmarks with linear
length constraints. The benchmarks range from theoretically-interesting cases
to variations of the real-world application set Kaluza [19]. All tests were
performed on Ubuntu Linux 18.04 with an Intel Xeon E5-2698 v4 @ 2.20GHz CPU
and 512GB of memory with a timeout of 30 seconds.

We used five different kind of benchmarks. The first track (I) was produced by
generating random strings, and replacing factors with variables at random, in
a coherent fashion. This guarantees the existence of a solution. The generated
word equations have at most 15 variables, 10 letters, and length 300. The
second track (II) is based on the idea in Proposition 1 of [10], where the
equation $X_{n}aX_{n}bX_{n-1}bX_{n-2}\cdots bX_{1}\doteq
aX_{n}X_{n-1}X_{n-1}bX_{n-2}X_{n-2}b\cdots bX_{1}X_{1}baa$ is shown to have a
minimal solution of exponential length w.r.t. the length of the equation. The
third track (III) is based on the second track, but each letter $b$ is
replaced by the left hand side or the right hand side of some randomly
generated word equation (e.g., with the methods from track (I)). In the fourth
track (IV) each benchmark consists of a system of 100 small random word
equations with at most 6 letters, 10 variables and length 60. The hard aspect
of this track is solving multiple equations at the same time. Within the fifth
track (V) each benchmark enriches a system of 30 word equations by suitable
linear constraints, as presented in this paper. This track is inspired by the
Kaluza benchmark set in terms of having many small equations enriched by
linear length constraints. All tracks, except track II which holds 9
instances, consist of 200 benchmarks. The full benchmark set is available at
https://www.informatik.uni-kiel.de/~mku/woorpje.

| Track I |  | Track II |  | Track III |  | Track IV |  | Track V
---|---|---|---|---|---|---|---|---|---
|  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |
woorpje | 200 | 0 | 0 | 0 | 8.10 |  | 5 | 0 | 4 | 0 | 123.85 |  | 189 | 0 | 11 | 0 | 341.74 |  | 196 | 2 | 2 | 0 | 136.20 |  | 178 | 9 | 13 | 0 | 399.22
cvc4 | 182 | 0 | 17 | 0 | 543.32 |  | 1 | 0 | 8 | 0 | 240.03 |  | 165 | 0 | 35 | 0 | 1055.24 |  | 172 | 0 | 28 | 0 | 925.13 |  | 179 | 0 | 21 | 0 | 635.97
z3str3 | 197 | 1 | 2 | 0 | 105.07 |  | 0 | 9 | 0 | 0 | 0.33 |  | 93 | 43 | 58 | 6 | 2089.92 |  | 175 | 10 | 12 | 3 | 490.23 |  | 198 | 1 | 1 | 0 | 41.52
z3seq | 183 | 0 | 17 | 0 | 545.24 |  | 9 | 0 | 0 | 0 | 1.81 |  | 126 | 0 | 73 | 1 | 2199.99 |  | 193 | 0 | 6 | 1 | 200.09 |  | 193 | 0 | 7 | 0 | 217.35
norn | 176 | 0 | 20 | 4 | 1037.63 |  | 0 | 0 | 9 | 0 | 270.00 |  | 71 | 0 | 128 | 1 | 4038.83 |  | 60 | 0 | 72 | 68 | 3216.95 |  | 112 | 0 | 9 | 79 | 742.34
sloth | 101 | 0 | 99 | 0 | 3658.34 |  | 7 | 0 | 2 | 0 | 124.56 |  | 121 | 0 | 67 | 12 | 2808.48 |  | 16 | 0 | 184 | 0 | 5615.81 |  | 9 | 2 | 187 | 2 | 5750.79

Table 1: Benchmark results (: correct classified, : reported unknown, : timed
out after 30 seconds, : incorrectly classified, : total Time in seconds)

Table 1 is read as follows: is the count of instances classified as correctly,
where marks the incorrect classified cases. For instances marked with the
solver returned no answer but terminated before the timeout of 30 seconds was
reached, where in marked cases the solver was killed after 30 seconds. The row
marked by states the overall solving time. The produced substitutions were
checked regarding their correctness afterwards. The classification of was done
by ad-hoc case inspection whenever not all solvers agreed on a result. In the
cases one solver produced a valid solution, and others did not, we validated
the substitutions manually. For the cases where one solver determined an
equation is unsatisfied and all others timed out, we treated the unsat result
as correct. This means that we only report errors if a solver reports unsat
and we know the equation was satisfiable. During our evaluation of track I
CVC4 crashed with a null-pointer exception regarding the word equation
$dbebgddbecfcbbAadeeaecAgebegee\\-caf\\-egebdbagddaadbddcaeeebfabfef\\-abfacdgAgaabgegagf\,\dot{=}\,dbebgddbeA\\-fcbbAaIegeeAaD\\-e\\-gagf$,
where lowercase symbols are letters and uppercase symbols are variables. Worth
mentioning is the reporting of 14 satisfiable benchmarks by the tool Sloth
without being able to produce a valid model, while at least two other tools
classified them as unsatisfiable. We treated this as an erroneous behaviour.

The result shows that Woorpje produces reliable results (0 errors) in
competitive time. It outperforms the competitors in track I,III and IV and
sticks relatively tight to the leaders Z3str3, Z3Seq and CVC4 on track V. On
track II Woorpje trails CVC4 and Z3Str3. The major inefficiency of Woorpje is
related to multiple equations with large alphabets and linear length
constraints.

It is worth emphasising, that the benchmarks developed here seem of intrinsic
interest, as they challenge even established solvers.

##  5 Conclusion

In this paper we present a method for solving word equations by using a SAT-
Solver. The method is implemented in our new tool Woorpje and experiments show
it is competitive with state-of-the-art string solvers. Woorpje solves word
equations instances that other solvers fail to solve. This indicates that our
technique can complement existing in a portfolio approach.

In the future, aim to extend our approach to include regular constraints. As
our approach rely on automata theory, it is expected that this could be
achievable. Another step is the enrichment of our linear constraint solving.
We currently do a basic analysis by using the MDDS. There are a few refinement
steps described in [2] which seem applicable. A next major step is to develop
a more efficient encoding of the alphabet of constants. Currently the state
space explodes due to the massive branching caused by the usage of large
alphabets.

## References

  * Abdulla et al. [2015] Abdulla, P.A., Atig, M.F., Chen, Y.F., Holík, L., Rezine, A., Rümmer, P., Stenman, J.: Norn: An SMT solver for string constraints.  In: Kroening, D., Păsăreanu, C.S. (eds.) Computer Aided Verification. pp. 462–469. Springer International Publishing, Cham (2015)
  * Abío and Stuckey [2014] Abío, I., Stuckey, P.J.: Encoding linear constraints into SAT.  In: International Conference on Principles and Practice of Constraint Programming. pp. 75–91. Springer (2014)
  * Audemard and Simon [2018] Audemard, G., Simon, L.: On the glucose SAT solver.  International Journal on Artificial Intelligence Tools 27(01), 1840001 (2018)
  * Barrett et al. [2011] Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4.  In: International Conference on Computer Aided Verification. pp. 171–177. Springer (2011)
  * Berzish et al. [2017] Berzish, M., Ganesh, V., Zheng, Y.: Z3str3: A string solver with theory-aware heuristics.  In: 2017 Formal Methods in Computer Aided Design (FMCAD). pp. 55–59 (Oct 2017)
  * Bjørner et al. [2009] Bjørner, N., Tillmann, N., Voronkov, A.: Path feasibility analysis for string-manipulating programs.  In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 307–321. Springer (2009)
  * Cadar et al. [2008] Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs.  In: Draves, R., van Renesse, R. (eds.) 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings. pp. 209–224. USENIX Association (2008), http://www.usenix.org/events/osdi08/tech/full_papers/cadar/cadar.pdf
  * Chen et al. [2019] Chen, T., Hague, M., Lin, A.W., Rümmer, P., Wu, Z.: Decision procedures for path feasibility of string-manipulating programs with complex operations.  Proceedings of the ACM on Programming Languages 3(POPL), 49 (2019)
  * Cordeiro et al. [2018] Cordeiro, L.C., Kesseli, P., Kroening, D., Schrammel, P., Trtík, M.: JBMC: A bounded model checking tool for verifying java bytecode.  In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10981, pp. 183–190. Springer (2018), https://doi.org/10.1007/978-3-319-96145-3_10
  * Day et al. [2017] Day, J.D., Manea, F., Nowotka, D.: The hardness of solving simple word equations.  In: Proc. MFCS 2017. LIPIcs, vol. 83, pp. 18:1–18:14 (2017)
  * Holík et al. [2017] Holík, L., Janků, P., Lin, A.W., Rümmer, P., Vojnar, T.: String constraints with concatenation and transducers solved efficiently.  Proceedings of the ACM on Programming Languages 2(POPL), 4 (2017)
  * Jeż [2013] Jeż, A.: Recompression: a simple and powerful technique for word equations.  In: 30th International Symposium on Theoretical Aspects of Computer Science, STACS 2013, February 27 - March 2, 2013, Kiel, Germany. pp. 233–244 (2013), https://doi.org/10.4230/LIPIcs.STACS.2013.233
  * Jeż [2017] Jeż, A.: Word equations in nondeterministic linear space.  In: Proc. ICALP 2017. LIPIcs, vol. 80, pp. 95:1–95:13. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)
  * Karhumäki et al. [2000] Karhumäki, J., Mignosi, F., Plandowski, W.: The expressibility of languages and relations by word equations.  Journal of the ACM (JACM) 47(3), 483–505 (2000)
  * Kiezun et al. [2009] Kiezun, A., Ganesh, V., Guo, P.J., Hooimeijer, P., Ernst, M.D.: Hampi: a solver for string constraints.  In: Proceedings of the eighteenth international symposium on Software testing and analysis. pp. 105–116. ACM (2009)
  * Makanin [1977] Makanin, G.S.: The problem of solvability of equations in a free semigroup.  Sbornik: Mathematics 32(2), 129–198 (1977)
  * Plandowski and Rytter [1998] Plandowski, W., Rytter, W.: Application of Lempel-Ziv encodings to the solution of words equations.  In: Proc. 25th International Colloquium on Automata, Languages and Programming, ICALP’98. Lecture Notes in Computer Science, vol. 1443, pp. 731–742. Springer (1998)
  * Plandowski [1999] Plandowski, W.: Satisfiability of word equations with constants is in pspace.  In: Foundations of Computer Science, 1999. 40th Annual Symposium on. pp. 495–500. IEEE (1999)
  * Saxena et al. [2010] Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: A symbolic execution framework for javascript.  In: 2010 IEEE Symposium on Security and Privacy. pp. 513–528. IEEE (2010)
  * Trinh et al. [2016] Trinh, M.T., Chu, D.H., Jaffar, J.: Progressive reasoning over recursively-defined strings.  In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification. pp. 218–240. Springer International Publishing, Cham (2016)

##  Appendix 0.A Artifacts for this paper

You can download our artifacts at http://informatik.uni-
kiel.de/~mku/woorpje/rp19.tar.gz. This package contains:

  1. 1.

A README.txt including a guide to use our artifacts.

  2. 2.

Download script for all used tools

  3. 3.

Benchmark suite

  4. 4.

Woorpje source code

##  Appendix 0.B Preprocessing algorithms

###  0.B.1 Prefix reducer

For a word $w\in\Xi^{*}$ we define the prefix of length $i\in[|w|]$ by
$w[i:]=w[1]\dots w[i]$. This algorithm is used analogously for suffices.

⬇

1$\mathsf{Input:}$ $u\,\dot{=}\,v$ # input word equation

2$\mathsf{Output:}$ $u^{\prime}\,\dot{=}\,v^{\prime}$ # reduced word equation

2commonPrefixIndex = 0

3for $i\in\min\Set{}{v|,|u|}$

4 if $v[i]\neq u[i]$

5 commonPrefixIndex = i

6 break

7return $u[commonPrefixIndex:]\,\dot{=}\,v[commonPrefixIndex:]$

Listing 1: Prefix reducer

###### Example 4

Consider the word equation $aaX\,\dot{=}\,aabY$ where capital letters are
variables and lower case letters are constants. The above algorithm reduces
the equation to $X\,\dot{=}\,bY$.

####  0.B.1.1 Prefix mismatch

This algorithm is used analogously for suffices.

⬇

1$\mathsf{Input:}$ $u\,\dot{=}\,v$ # input word equation

2$\mathsf{Output:}$ $x\in\Set{\texttt{UNSAT},\texttt{UNKNOWN}}$

2for $i\in\min\Set{}{v|,|u|}$

3 if $v[i],u[i]\in\Gamma$:

4 break

5 if $v[i]\neq u[i]\land v[i],u[i]\in\Sigma$:

6 return UNSAT

7return UNKNOWN

Listing 2: Prefix mismatch

###### Example 5

Consider the word equation $abX\,\dot{=}\,aabY$ where capital letters are
variables and lower case letters are constants. The above algorithm returns
UNSAT due to the mismatch of the second characters.

###  0.B.2 Constant sequence mismatch

Within the following algorithm we use the set of factors of a word
$w\in\Xi^{*}$ which is defined by
$\mathsf{factor}(w)=\Set{v\in\Xi}{\exists\;u_{1},u_{2}\in\Xi^{*}:w=u_{1}vu_{2}}$.
For a given equation $u\,\dot{=}\,v$ this algorithm assumes $u\in\Sigma^{*}$
and $v\in\Xi^{*}$.

⬇

1$\mathsf{Input:}$ $u\,\dot{=}\,v$ # input word equation

2$\mathsf{Output:}$ $x\in\Set{\texttt{UNSAT},\texttt{UNKNOWN}}$

2for
$w\in\Set{x\in\Sigma^{*}}{x\in\mathsf{factor}(v)\land\forall\,y\in\mathsf{factor}(v):y\in\mathsf{factor}(x)\Rightarrow|x|\geq|y|}$

3 if $w\notin\mathsf{factor}(u)$

4 return UNSAT

5return UNKNOWN

Listing 3: Constant sequence mismatch

###### Example 6

Consider the word equation $ababab\,\dot{=}\,XaabY$ where capital letters are
variables and lower case letters are constants. The above algorithm returns
UNSAT because $aab\notin\mathsf{factor}(ababab)$.

###  0.B.3 Parikh matrix mismatch

This algorithm is used analogously for suffices. It uses the Parikh matrix
which for a word $w\in\Xi^{*}$ is defined for each $a\in\Xi$ and $i\in[|w|]$
by $M_{w}[i][a]=|w[:i]|_{a}$.

⬇

1$\mathsf{Input:}$ $u\,\dot{=}\,v$ # input word equation

2$\mathsf{Output:}$ $x\in\Set{\texttt{UNSAT},\texttt{UNKNOWN}}$

2for $i\in\min\Set{}{v|,|u|}$

3 variablesAlign = true

4 terminalsAlign = true

5 for $a\in\Xi$

6 if $M_{v}[i][a]\neq M_{v}[i][a]$:

7 if $a\in\Gamma$

8 variablesAlign = false

9 else

10 terminalsAlign = false

11 if variablesAlign and not terminalsAlign

12 return UNSAT

13return UNKNOWN

Listing 4: Parikh matrix mismatch

###### Example 7

Consider the word equation $aX\,\dot{=}\,Xb$ where capital letters are
variables and lower case letters are constants. The above algorithm returns
UNSAT due to a Parikh matrix mismatch within index 2 regarding character $a$
(and $b$). The matrices look as following:

$\bordermatrix{&{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}\text{\tiny$1$}}&{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}\text{\tiny$2$}}\cr{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}\text{\tiny$a$}}&1&1\cr{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}\text{\tiny$b$}}&0&0\cr{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color<EMAIL_ADDRESS>28.45274pt\text{and}\hskip
28.45274pt\bordermatrix{&{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}\text{\tiny$1$}}&{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}\text{\tiny$2$}}\cr{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}\text{\tiny$a$}}&0&0\cr{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}\text{\tiny$b$}}&0&1\cr{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color<EMAIL_ADDRESS>
###  0.B.4 Substitution reasoning

For a system of word equations $E$ this algorithm assumes that all equations
$u\,\dot{=}\,v\in E$ are minimized with our algorithm given in 1.

⬇

1$\mathsf{Input:}$ $E$ # a System of word equations

2$\mathsf{Output:}$ $(E,x)$ # $E$ - a system of equations,
$x\in\Set{\text{SAT},\texttt{UNSAT},\texttt{UNKNOWN}}$

2E’ = $\Set{u\,\dot{=}\,v}{u\in\Gamma\land
v\in\Sigma^{*}\land\left(u\,\dot{=}\,v\in E\lor v\,\dot{=}\,u\in E\right)}$

3

4if E’ = $\emptyset$

5 return ($\emptyset$,UNKNOWN)

6

7for $u\,\dot{=}\,v\in E$

8 for $A\,\dot{=}\,w\in E^{\prime}$

9 $v^{\prime}$ = $S(u)[A\mapsto w]$

10 $u^{\prime}$ = $S(v)[A\mapsto w]$

11 if $u\neq u^{\prime}\lor v\neq v^{\prime}$

12 if v $\neq$ u

13 if applyOtherUNSATalgorithms($u\,\dot{=}\,v$) = UNSAT

14 return ($\emptyset$,UNSAT)

15 v = v’

16 u = u’

17 else

18 $E$ = $E\setminus u\,\dot{=}\,v$

19

20if E = $\emptyset$

21 return (E’,SAT)

22return(E’,UNKNOWN)

Listing 5: Substitution reasoning

###### Example 8

Consider the word equations $X\,\dot{=}\,aab$,$Y\,\dot{=}\,a$ and $aX=Yaab$
where capital letters are variables and lower case letters are constants. The
above algorithm returns SAT and the set of equations
$X\,\dot{=}\,aab$,$Y\,\dot{=}\,a$, which gives us the substitutions $S(X)=aab$
and $S(Y)=a$.

##  Appendix 0.C More detailed benchmark results

$0$$50$$100$$150$$200$$0$$10$$20$$30$$40$$50$Solved instancesTime
(seconds)Track Iwoorpjecvc4z3str3z3seqnornsloth

$2$$4$$6$$8$$0$$2$$4$$6$Solved instancesTime (seconds)Track
IIwoorpjecvc4z3str3z3seq

$0$$50$$100$$150$$200$$0$$10$$20$$30$$40$$50$Solved instancesTime
(seconds)Track IIIwoorpjecvc4z3str3z3seqnornsloth

$0$$50$$100$$150$$200$$0$$20$$40$$60$Solved instancesTime (seconds)Track
IVwoorpjecvc4z3str3z3seqnornsloth

$0$$50$$100$$150$$200$$0$$10$$20$$30$$40$$50$Solved instancesTime
(seconds)Track Vwoorpjecvc4z3str3z3seqnornsloth

Figure 5: Cactus plots for all Tracks

| Woorpje |  | CVC4 |  | z3Str3 |  | z3Seq |  | Norn |  | Sloth |
---|---|---|---|---|---|---|---|---|---|---|---|---
| I | II | III | IV | V |  | I | II | III | IV | V |  | I | II | III | IV | V |  | I | II | III | IV | V |  | I | II | III | IV | V |  | I | II | III | IV | V |
sat | 200 | 5 | 147 | 104 | 164 |  | 182 | 1 | 121 | 76 | 156 |  | 197 | 0 | 51 | 79 | 175 |  | 183 | 9 | 82 | 97 | 170 |  | 176 | 0 | 60 | 16 | 88 |  | 101 | 7 | 126 | 15 | 11 |
unsat | 0 | 0 | 42 | 92 | 14 |  | 0 | 0 | 44 | 96 | 23 |  | 0 | 0 | 48 | 99 | 23 |  | 0 | 0 | 45 | 97 | 23 |  | 4 | 0 | 12 | 112 | 103 |  | 0 | 0 | 7 | 1 | 0 |
unknown | 0 | 0 | 0 | 2 | 9 |  | 0 | 0 | 0 | 0 | 0 |  | 1 | 9 | 43 | 10 | 1 |  | 0 | 0 | 0 | 0 | 0 |  | 0 | 0 | 0 | 0 | 0 |  | 0 | 0 | 0 | 0 | 2 |
timeout | 0 | 4 | 11 | 2 | 13 |  | 17 | 8 | 35 | 28 | 21 |  | 2 | 0 | 58 | 12 | 1 |  | 17 | 0 | 73 | 6 | 7 |  | 20 | 9 | 128 | 72 | 9 |  | 99 | 2 | 67 | 184 | 187 |
error | 0 | 0 | 0 | 0 | 0 |  | 0 | 0 | 0 | 0 | 0 |  | 0 | 0 | 6 | 3 | 0 |  | 0 | 0 | 1 | 1 | 0 |  | 4 | 0 | 1 | 68 | 79 |  | 0 | 0 | 12 | 0 | 2 |
Time (s) | 8.10 | 123.85 | 341.74 | 136.20 | 399.22 |  | 543.32 | 240.03 | 1055.24 | 925.13 | 635.97 |  | 105.07 | 0.33 | 2089.92 | 490.23 | 41.52 |  | 545.24 | 1.81 | 2199.99 | 200.09 | 217.35 |  | 1037.63 | 270.00 | 4038.83 | 3216.95 | 742.34 |  | 3658.34 | 124.56 | 2808.48 | 5615.81 | 5750.79 |
Time w/o timeouts (s) | 8.10 | 3.85 | 11.74 | 76.20 | 9.22 |  | 3.32 | 0.03 | 5.24 | 85.13 | 5.97 |  | 45.07 | 0.33 | 349.92 | 130.23 | 11.52 |  | 35.24 | 1.81 | 9.99 | 20.09 | 7.35 |  | 437.63 | 0.00 | 198.83 | 1056.95 | 472.34 |  | 688.34 | 64.56 | 798.48 | 95.81 | 140.79 |

Table 2: Benchmark results

Table 2 is read as follows: sat is the count of instances classified as
satisfiable, where unsat marks the unsatisfiable cases. For instances marked
as unknown the solver returned no answer but terminated before the timeout was
reached, where in timeout cases the solver was killed after 30 seconds. The
row error lists the count of incorrectly classified instances. The row which
states the time lists the overall solving time with and without timeout cases.
The produced substitutions were checked regarding their correctness
afterwards. The classification of an error was done by ad-hoc case inspection
whenever not all solvers agreed on a result. In the cases one solver produced
a valid solution, and others did not, we validated the substitutions manually.
For the cases where one solver determined an equation is unsatisfied and all
others timed out, we treated the unsat result as correct. This means that we
only report errors if a solver reports unsat and we know the equation was
satisfiable. The table lists only 199 benchmarks on Track I for CVC4, since
the program crashed with a null-pointer exception regarding the equation
$dbebgddbecfcbbAadeeaecAgebegeecafegebdbagddaadbddcaeeeb\\-fabfefabfacdgAgaabgegagf\,\dot{=}\,dbebgddbeAfcbbAaIegeeAaDegagf$,
where lowercase symbols are letters and uppercase letters are variables. This
word equation is stored as benchmark 111 in Track I.

The erroneous behavior of Sloth was detected within the following benchmarks:
Track III; Benchmarks 10,11,14,15,16,17,18,21,23,24,4,43 and Track V; 192,53.

| Woorpje
---|---
| I | II | III | IV | V
sat | 200 | 5 | 147 | 104 | 162
unsat | 0 | 0 | 0 | 0 | 0
unknown | 0 | 0 | 6 | 63 | 9
timeout | 0 | 4 | 47 | 33 | 29
error | 0 | 0 | 0 | 0 | 0
Time (s) | 8.10 | 123.62 | 1423.06 | 1162.00 | 885.18
Time w/o timeouts (s) | 8.10 | 3.62 | 13.06 | 172.00 | 15.18
Table 3: Benchmark results without preprocessing

Table 3 shows the results Woorpje produces without using preprocessing
techniques. It is read in exactly the same way as the previous table.
Comparing the times shows that preprocessing not only speeds up the solving
time, but also helps to classify a few more positive instances.