BRICS RS-00-13 Klíma & Srba: Matching Modulo Associativity and Idempotency is NP-Complete BRICS

Basic Research in Computer Science

Matching Modulo Associativity and Idempotency is NP-Complete

Ondřej Klíma Jiří Srba BRICS Report Series RS-00-13 ISSN 0909-0878 June 2000 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2000, Ondřej Klíma & Jiří Srba.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/00/13/

Matching Modulo Associativity and Idempotency is NP–complete^{⋆}

Ondřej Klíma^{1} and Jiří Srba^{2}

1 Faculty of Science MU, Dept. of Mathematics, Janáčkovo nám. 2a, 662 95 Brno,

                     Czech Republic, klima@math.muni.cz

2 BRICS^{⋆ ⋆ ⋆}, Department of Computer Science, University of Aarhus, Ny Munkegade bld. 540, DK-8000 Aarhus C, Denmark, srba@brics.dk

Abstract. We show that AI–matching (AI denotes the theory of an associative and idempotent function symbol), which is solving matching word equations in free idempotent semigroups, is NP-complete. Note: this is a full version of the paper [9] and a revision of [8].

Keywords: unification, word rewriting, idempotent semigroups, complexity

1 Introduction

Solving equations appears as an interesting topic in several fields of computer science. Many areas such as logic programming and automated theorem proving exploit solving equations, and syntactic (Robinson) unification is a typical example of it. An important role is played also by semantic unification, which allows to use several function symbols with additional algebraic properties (e.g. associativity, commutativity and idempotency). Makanin (see [16]) shows that the question whether an equation in a free monoid has a solution is decidable. It can be generalized in the way that existential first-order theory of equations in a free monoid with additional regular constraints on the variables is decidable [19]. For an overview of unification theory consult e.g. [4].

AI–matching is one example of semantic unification where the considered equational theory is of one associative and idempotent

⋆ The paper is supported by the Grant Agency of the Czech Republic, grant No.

201/97/0456 and by grant FRVŠ 409/1999.

⋆ ⋆ ⋆

Basic Research in Computer Science,

Centre of the Danish National Research Foundation.

function symbol. In this paper we focus on a subclass of word equations which we call pattern equations. Pattern equations are word equations where we have on the left-hand side just variables and on the right-hand side only constants. In the usual interpretation, AI–matching is a AI–unification of systems of equations where all right-hand sides are variable–free. However, we can eliminate constants on the left-hand sides by adding new equations and so pattern equations are as general as AI–matching.

Many practical problems such as speech recognition/synthesis lead to this kind of equations. This work has been inspired by the papers [12] and [13] where the basic approach – syllable-based speech synthesis – is in assigning prosody attributes to a given text and segmentation into syllable segments. We examine the solvability of word equations in the variety of all idempotent semigroups, which we call stuttering equations. Their name comes from practical motivation. For example in speech recognition the speaker sometimes stutters some words and we would like to eliminate this effect and enable the correct variables assignment even in the case of stuttering. Therefore we allow to eliminate multiple occurrences of the same subword into only one occurrence, which can be modelled by the identity x^{2} = x. The decidability of the satisfiability problem (even in the general case) is a consequence of the local finiteness of free idempotent semigroups and an exponential upper bound on the length of a minimal solution can be given ([6]). A polynomial time decision procedure for the word problem in a free idempotent semigroup can be also easily established. Recently it has been proved in [3] that AI–unification remains decidable even if additional uninterpreted function symbols in the equations are allowed.

Unification problems for the AI–theory have been investigated e.g. in [1, 2, 20], however, the complexity questions were not answered. In this paper we prove that there is a polynomial bound on the length of a minimal solution in the case of stuttering pattern equations and thus we show that the satisfiability problem is in NP. The proof exploits the confluent and terminating word rewriting system for idempotent semigroups by Siekmann and Szabo (see [21]). This means that the identity p = q holds in a free idempotent semigroup if and only if the words p and q have the same normal form w.r.t. the rewriting system {xx → x | C(x) ≠ ∅} ∪ {uvw → uw | ∅ ≠ C(v) ⊆ C(u) = C(w)}, where C(y) denotes the set of letters of y.

Showing a reduction from 3–SAT to our problem, we prove its NP–completeness. This is a more general result than Theorem 7 in the paper by Kapur and Narendran [11], where they prove NP– hardness for AI–matching, where additional uninterpreted function symbols are allowed. In our proof we use only one associative and idempotent function symbol. NP–hardness means that the problem is probably difficult. One of the ways how to solve the problem is to use heuristic algorithms. They are the current field of interest in speech recognition.

2 Basic definitions

An idempotent semigroup (also called a band) is a semigroup where the identity x^{2} = x is satisfied. Let C be a finite set. We define a binary relation → ⊆ C^{∗} × C^{∗} such that uvvw → uvw for u, v, w ∈ C^{∗} and let ∼ be its symmetric, reflexive and transitive closure, i.e. ∼ := (→ ∪ →^{−1})^{∗}. Then the identity p = q holds in a free band over C if and only if p ∼ q (completeness of the equational logic).

Let C be a finite set of constants and V be a finite set of variables such that C ∩ V = ∅. A word equation L = R is a pair (L, R) ∈ (C ∪ V)^{∗} ×(C ∪V)^{∗}. A system of word equations is a finite set of equations of the form {L_{1} = R_{1}, …, L_{n} = R_{n}} for n > 0. A solution (in a free idempotent semigroup) of such a system is a homomorphism α : (C ∪ V)^{∗} → C^{∗} which behaves as an identity on the letters from C and equates all the equations of the system, i.e. α(L_{i}) ∼ α(R_{i}) for all 1 ≤ i ≤ n. Such a homomorphism is fully established by a mapping α : V → C^{∗}. A solution is called non-singular, if α(x) ≠ ϵ for all x ∈ V, where ϵ denotes the empty word. Otherwise we will call it singular. We say that a system of word equations (in a free idempotent semigroup) is satisfiable whenever it has a solution. For the introduction into word equations and combinatorics on words you can see [14], [15] and [18]. We refer to word equations in a free idempotent semigroup as stuttering equations.

In what follows we will use a uniform notation. The set C = {a, b, c, … } denotes the alphabet of constants and V = {x, y, z, … } stands for variables (unknowns) with the assumption that C ∩V = ∅.

We will use the same symbol α for the mapping α : V → C^{∗} and its unique extension to a homomorphism α : (C ∪ V)^{∗} → C^{∗}. The empty word will be denoted by ϵ and the length of a word w by |w|.

We exploit the fact that the word problem in a free band is decidable (see [7] and its generalization [10]), which is a consequence of the next lemma. Let w ∈ C^{+}. We define

C(w) – the set of all letters that occur in w,

0(w) – the longest prefix of w in card(C(w)) − 1 letters, 1(w) – the longest suffix of w in card(C(w)) − 1 letters.

Let also \overline{0}(w) resp. \overline{1}(w) be the letter that immediately succeeds 0(w) resp. precedes 1(w).

Lemma 1 ([7]). Let p, q ∈ C^{+}. Then p ∼ q if and only if C(p) = C(q), 0(p) ∼ 0(q) and 1(p) ∼ 1(q).

It is obvious that if a stuttering equation system has a solution then it has always infinitely many solutions, which we show in the following lemma.

Lemma 2. Let {L_{1} = R_{1}, …, L_{n} = R_{n}} be a stuttering equation system with a solution α. Then also any β that satisfies α(x) ∼ β(x) for all x ∈ V (we simply write α ∼ β) is a solution.

Proof. Immediate. ⊓ ⊔

This gives an idea that we should look just for the solutions where α(x) is the shortest word in the ∼ class for each variable x. We introduce a size of a solution α as size(α) := max_{x∈V} |α(x)| and say that α is minimal iff for any solution β of the system we have size(α) ≤ size(β). Given a stuttering equation system it is decidable whether the system is satisfiable because of the local finiteness of free idempotent semigroups. The following lemma just gives a precise exponential upper bound on the size of a minimal solution.

Lemma 3 ([6]). Let k = card(C) ≥ 2 and let {L_{1} = R_{1}, …, L_{n} = R_{n}} be a stuttering equation system. If the system is satisfiable then there exists a solution α such that size(α) ≤ 2^{k} + 2^{k−2} − 2.

In general it can be shown that there are stuttering equation systems such that all their solutions are at least exponentially large w.r.t. the cardinality of the set C . Consider the following sequence of equations: x_{1} = a_{1} and x_{i+1} = x_{i}a_{i+1}x_{i} for a sequence of pairwise different constants a_{1}, a_{2}, . . .. For any solution α of the system we have that |α(x_{i})| ≥ 2^{i} − 1.

In this paper we focus on a special kind of word equations which we call pattern equations.

Definition 1. A pattern equation system is a set {X_{1} = A_{1}, …, X_{n} = A_{n}} where X_{i} ∈ V^{∗} and A_{i} ∈ C^{∗} for all 1 ≤ i ≤ n. A solution of a pattern equation system is defined as in the general case.

Remark 1. In the usual interpretation AI–matching allows constants to appear also on the left-hand sides, i.e. the equations are of the type X = A where X ∈ (V ∪ C)^{∗} and A ∈ C^{∗}. However, we can w.l.o.g. consider only pattern equations, since an equation of the type X_{1}aX_{2} = A where a ∈ C can be transformed into X_{1}xX_{2} = A and x = a, where x is a new variable.

Two natural decidability problems (Pattern-Equation and Non-Singular-Pattern-Equation problem) appear in this context and are defined below.

Definition 2. Given a pattern equation system {X_{1} = A_{1}, …, X_{n} = A_{n}} as an instance of the Pattern-Equation problem, the task is to decide whether this system has a solution. If we require the solution to be non-singular we call the problem Non-Singular-Pattern-Equation.

The Pattern-Equation problem for a single stuttering pattern equation X = A is trivial since it is always solvable: α(x) = A for all x ∈ V. On the other hand a system is not always solvable: e.g. {x = a, x = b} has no solution.

We give an example of a pattern equation system and demonstrate its solutions.

Example 1. Let us have the following system where C = {a, b}, V = {x, y, z} and the pattern equations are {yxy = aba, yz = a}. A singular solution exists α(x) = aba, α(y) = ϵ, α(z) = a, however, there is also a non-singular solution β(x) = bab, β(y) = a, β(z) = a since ababa ∼ aba and aa ∼ a. We have also another non-singular solution γ(x) = b, γ(y) = a, γ(z) = a.

Our goal is to show that a minimal solution of a stuttering pattern equation system is of a polynomial length. This implies that the problem of deciding whether a stuttering pattern equation system is satisfiable is in NP.

3 Rewriting system for idempotent semigroups

In this section we summarize several properties of the rewriting system by Siekmann and Szabo in [21] and prove some technical lemmas. First of all we have to give some definitions and results concerning rewriting systems as it can be found e.g. in [5].

A rewriting system R over C is a subset of C^{∗} × C^{∗}. The elements of R will be called rules. Having such a system R we can define a rewrite relation →⊆ C^{∗} × C^{∗} in the following way:

∀p, q ∈ C^{∗} : p → q iff ∃(u, v) ∈ R, s, t ∈ C^{∗} : p = sut, q = svt.

The elements (u, v) of R will be often written as u → v. For a word q ∈ C^{∗} we write q ↛ iff there is no q′ such that q → q′ and we say that q is in a normal form. We define the set of normal forms of p ∈ C^{∗} as ⟨p⟩ = {q | p →^{∗} q ↛}. We say that R (resp. the relation →) is terminating iff there is no infinite sequence p_{1}, p_{2}, p_{3}, … ∈ C^{∗} such that p_{1} → p_{2} → p_{3} → . . .. The system R (resp. the relation →) is confluent iff ∀p, p_{1}, p_{2} ∈ C^{∗}∃q ∈ C^{∗} :

if (p →^{∗} p_{1} and p →^{∗} p_{2}) then (p_{1} →^{∗} q and p_{2} →^{∗} q).

The system R (resp. the relation →) is locally confluent iff ∀p, p_{1}, p_{2} ∈ C^{∗}∃q ∈ C^{∗} :

if (p → p_{1} and p → p_{2}) then (p_{1} →^{∗} q and p_{2} →^{∗} q).

The following lemma shows the relationship between confluence and local confluence.

Lemma 4 ([5]). Let R be a terminating rewriting system. Then R is confluent if and only if R is locally confluent.

It is easy to see that if R is a confluent and terminating rewriting system, then a word p ∈ C^{∗} has exactly one normal form, i.e. ⟨p⟩ = {q} for some q, and in such a case we simply write ⟨p⟩ = q.

Example 2. Let {xx → x | x ∈ C^{∗}, C(x) ≠ ∅} be a rewriting system over C. Then this system is terminating but it is not confluent. For p = ababcbabc we have p = (ab)(ab)cbabc → abcbabc and p = a(babc)(babc) → (ab)(ab)c → abc where abcbabc and abc are in normal form. It is easy to see that ⟨p⟩ = {abc, abcbabc}.

In this paper we will exploit the rewriting system by Siekmann and Szabo in [21].

Lemma 5 ([21]). The rewriting system {xx → x | x ∈ C^{∗}, C(x) ≠ ∅} ∪ {uvw → uw | u, v, w ∈ C^{∗}, ∅ ≠ C(v) ⊆ C(u) = C(w)} is confluent and terminating. Moreover for p, q ∈ C^{∗} we have p ∼ q if and only if p and q have the same normal form w.r.t. the system.

We will refer the rewriting system {xx → x | C(x) ≠ ∅}∪{uvw → uw | ∅ ≠ C(v) ⊆ C(u) = C(w)} as RS. Since RS contains two different types of rewriting rules we denote RS_{1} the rewriting system {xx → x | C(x) ≠ ∅} and RS_{2} the rewriting system {uvw → uw | ∅ ≠ C(v) ⊆ C(u) = C(w)}. The corresponding rewrite relations are denoted →, →_{1} resp. →_{2} and for a word p ∈ C^{∗} the set of its normal forms is denoted by ⟨p⟩, ⟨p⟩_{1} resp. ⟨p⟩_{2}.

If we want to investigate the complexity issues for stuttering equations, the first question we have to answer is the complexity of checking whether some identity holds in a free band. We will show that the word problem (i.e. the problem whether p ∼ q) can be decided in polynomial time by using the rewriting system RS. If we note that a string of length k contains O(k^{2}) substrings (each substring is identified by its beginning and its length) we get that each reduction of RS can be done in polynomial time. Since every reduction decreases the length of the word, we have a polynomial time decision algorithm for the word problem in a free band.

We know that RS is confluent and terminating. Our goal in this section is to show that RS_{2} is also a confluent and terminating rewriting system and that ⟨p⟩ = ⟨⟨p⟩_{2}⟩_{1}.

We define a rewrite relation →_{2l}⊂→_{2} such that suvwt →_{2l} suwt if and only if |v| = 1 and C(v) ⊆ C(u) = C(w). It is easy to see that →_{2}⊆→_{2l}^{∗} and hence →_{2l}^{∗}=→_{2}^{∗}. The last relation we will use is →_{2m}⊂→_{2}, consisting of all rules that leave out the maximal number of letters in the following sense. Let H(w) resp. T(w) mean the first resp. the last letter of the word w. We write suvwt →_{2m} suwt iff ∅ ≠ C(v) ⊆ C(u) = C(w) and the following conditions hold:

(i) C(s_{0}u) ≠ C(wt_{0}), for any suffix s_{0} of s and any prefix t_{0} of t (including empty s_{0} or t_{0}, but not both)

(ii) u = 0(u)T(u) (iii) w = H(w)1(w).

Note that if suvwt →_{2m} suwt then the last letter of s and the first letter of t (if they exist) are new and different letters^{1}. Also note that T(u) is the only occurrence of this letter in u and we can write it as u = 0(u)\overline{0}(u). Similarly w = \overline{1}(w)1(w).

We remind that whenever →_{2} rewriting applies then so does →_{2m} and →_{2l}. Moreover a word is in normal form w.r.t. →_{2} iff it is in normal form w.r.t. →_{2m} and iff it is in normal form w.r.t. →_{2l}. In what follows, we will use these trivial observations without any explicit reference.

We show that ⟨p⟩_{2m} = ⟨p⟩_{2}. The inclusion ⟨p⟩_{2m} ⊆ ⟨p⟩_{2} is obvious and the rest is the content of the following lemmas. For more transparent proofs we use the notation s\underline{u}v\underline{w}t →_{2} suwt in the sense that suvwt →_{2} suwt where ∅ ≠ C(v) ⊆ C(u) = C(w) (and the same for →_{2l}, →_{2m}). In the following, whenever we say that u is a subword of sut, we always refer to the concrete (and obvious) occurrence of the subword u in sut.

Lemma 6. The relation →_{2m} is confluent and terminating.

Proof. The termination is obvious. Let p be a word and suppose that we can apply two different rules of →_{2m} on p, say p = s_{1}\underline{u_{1}}v_{1}\underline{w_{1}}t_{1} →_{2m} s_{1}u_{1}w_{1}t_{1} and p = s_{2}\underline{u_{2}}v_{2}\underline{w_{2}}t_{2} →_{2m} s_{2}u_{2}w_{2}t_{2}.

Let us suppose that u_{1} is a subword of u_{2}v_{2}w_{2}. Then the whole u_{1}v_{1}w_{1} is a subword of u_{2}v_{2}w_{2}, because u_{2}v_{2}w_{2} is followed by a new letter (if t_{2} is non-empty), which is not contained in u_{1}. If u_{1}v_{1}w_{1} is a subword of u_{2} resp. w_{2} then our two rules commute (i.e. they are independent of the order of their applications). If it is not the case, we will show that v_{1} is a subword of v_{2}. Suppose that the occurrence of \overline{0}(u_{2}) (the last letter of u_{2}) is in u_{1}v_{1}w_{1}, then it is surely in u_{1}.

1 Observe that it doesn’t hold in general that if p →_{2m} q then spt →_{2m} sqt for s, t ∈ C^{∗}. This means that →_{2m} is not a rewriting relation in the previously introduced sense.

Similarly if the occurrence of \overline{1}(w_{2}) is in u_{1}v_{1}w_{1}, then it is in w_{1}. This implies that v_{1} is a subword of v_{2}. Let us define s_{0} as a prefix of u_{2} and t_{0} as a suffix of w_{2} s.t. s_{0}u_{1}v_{1}w_{1}t_{0} = u_{2}v_{2}w_{2}. Observe that C(s_{0}u_{1}) = C(u_{2}) = C(w_{2}) = C(w_{1}t_{0}) and using the condition (i) in the definition of →_{2m} we get that s_{0} = t_{0} = ϵ. So we have that u_{1}v_{1}w_{1} = u_{2}v_{2}w_{2} and v_{1} is a subword of v_{2}, which is a contradiction with the conditions (ii) and (iii).

If u_{1} resp. w_{1} is not a subword of u_{2}v_{2}w_{2}, and u_{2} resp. w_{2} is not a subword of u_{1}v_{1}w_{1}, then our two rules commute. ⊓ ⊔

Remark 2. From the previous proof we can see that two arbitrary applications of →_{2m}, say p = s_{1}\underline{u_{1}}v_{1}\underline{w_{1}}t_{1} →_{2m} s_{1}u_{1}w_{1}t_{1} and p = s_{2}\underline{u_{2}}v_{2}\underline{w_{2}}t_{2} →_{2m} s_{2}u_{2}w_{2}t_{2}, commute and they can be nested exactly in one of the following ways (up to symmetry):

1. w_{1} = w′_{1}q, u_{2} = qu′_{2} and p = s_{1}u_{1}v_{1}w′_{1}qu′_{2}v_{2}w_{2}t_{2}

2. u_{1}v_{1}w_{1} is a subword of u_{2}

Lemma 7. RS_{2} is a confluent and terminating rewriting system and ⟨p⟩_{2m} = ⟨p⟩_{2} for any p ∈ C^{∗}.

Proof. The termination is clear. If we have u →_{2} v, u →_{2} w then there is v_{1} and w_{1} such that v →_{2}^{∗} v_{1}, w →_{2}^{∗} w_{1}, u →_{2m} v_{1} and u →_{2m} w_{1}. Since →_{2m} is confluent, we have the confluence of RS_{2}. The equality ⟨p⟩_{2m} = ⟨p⟩_{2} is a trivial consequence. ⊓ ⊔

Lemma 8. For any p, q ∈ C^{∗} such that p = ⟨p⟩_{2} and p →_{1} q it holds that ⟨q⟩_{2} = q. In particular for a word p ∈ C^{∗} we have ⟨⟨p⟩_{2}⟩_{1} = ⟨p⟩.

Proof. Assume for the moment that ⟨q⟩_{2} ≠ q, which means that q = suawt where s, u, w, t ∈ C^{∗}, a ∈ C, a ∈ C(u) = C(w), i.e. q = s\underline{u}a\underline{w}t →_{2l} suwt. Then (up to symmetry) p = su_{1}xu_{2}awt where u_{1}, x, u_{2} ∈ C^{∗}, u_{1}u_{2} = u and su_{1} has a suffix x or u_{2}awt has a prefix x. We discuss four different cases:

1) x is a suffix of u_{1}

2) x is a suffix of su_{1} and |x| > |u_{1}|

3) x is a prefix of u_{2}aw

4) x is a prefix of u_{2}awt and |x| > |u_{2}aw|.

In the case 1) we get C(x) ⊆ C(u) = C(w) and we could also use the reduction p = s\underline{u_{1}xu_{2}}a\underline{w}t →_{2l} su_{1}xu_{2}wt since a ∈ C(u_{1}xu_{2}) = C(u) = C(w). In the case 2) we may write x = x_{1}u_{1} and then p = su_{1}x_{1}u_{1}u_{2}awt = su_{1}x_{1}\underline{u}a\underline{w}t →_{2l} su_{1}x_{1}uwt. Cases 3) and 4) are similar and all the four cases lead to a contradiction. ⊓ ⊔

4 Upper bound for the size of the solution

This section aims to prove that the Pattern-Equation problem is in NP by giving a polynomial upper bound on the size of a minimal solution. In the following we assume implicitly that A, B ∈ C^{∗}. Realise that each reduction of RS just leaves out some subword, the case uvw → uw is clear, and in the case xx → x we leave out the right occurrence of x in the square. If we have a word uAv, we can speak about the residual of A in the sense that the residual consists of all letter occurrences of A that were not left out during the sequence of reductions. Moreover if we use two different sequences of reductions by →_{2m}, which give normal form w.r.t. →_{2}, then the residuals are the same after the both reduction sequences, since any two applications of →_{2m} commute by Remark 2.

Lemma 9. Let A and B be in normal form and AB →_{2m} AB′ ↛_{2m} where B′ is the residual of B. Then the word B′ contains at most one square x^{2}. If B′ contains such a square, then x^{2} arises from xvx where v is the word left out by the reduction rule \underline{u}v\underline{w} →_{2m} uw, and x is both a suffix of u and a prefix of w. Moreover in the case when B′ contains a square we have B′ →_{1} ⟨B′⟩.

Proof. Assume that we have used AB = s\underline{u}v\underline{w}t →_{2m} suwt = AB′ and B′ contains a square x^{2}. Since B is in normal form, x^{2} contains “space” of the cancelled v, i.e. xx = u_{1}w_{1} where u_{1} is a suffix of u (u starts in A) and w_{1} is a prefix of wt.

We show that w_{1} is a prefix of w. In the case when |w_{1}| > |w| we can deduce that occurrences of T(u_{1}) and H(t) must lie in the left x since they are the first occurrences of the constants T(u_{1}) and H(t) in B (from the maximality of →_{2m}). It means that x = u_{1}wz where z is a prefix of t. Since C(u_{1}) ⊆ C(u) = C(w) ⊆ C(wz), we can reduce xx = u_{1}\underline{wz}u_{1}\underline{wz} →_{2} u_{1}wzwz and this is a contradiction with B′ ↛_{2}.

So, w_{1} is a prefix of w. The last letter of u_{1} is in the left x and the first letter of w_{1} is in the right x and we see that x^{2} arises from xvx and x is a suffix of u and a prefix of w (i.e. u = u_{0}x, w = xw_{0}).

We have uwt = u_{0}xxw_{0}t →_{1} u_{0}xw_{0}t. Let us denote B′′ as the residual of B′; in fact B′′ = u′′_{0}xw_{0}t where u′′_{0} is a suffix of u_{0}.

It is enough to show that the word B′′ does not contain a square and in such a case we get B′ →_{1} ⟨B′⟩_{1} = B′′. Assume that u′′_{0}xw_{0}t contains a square y^{2}. Recall xw_{0}t = wt is a suffix of B. Thus y^{2} is a subword of u′′_{0}xw_{0} since H(t) ∉ C(u′′_{0}xw_{0}) and because of the similar arguments as in the second paragraph. Since u′′_{0}x and xw_{0} = w are subwords of B then y^{2} contains both T(u′′_{0}) and H(w_{0}). However, T(x) = T(u) is the first occurrence of this letter in u′′_{0}xw_{0} and it must be in the left y and from the same reason H(x) = H(w) is in the right y. This is impossible. So u′′_{0}xw_{0}t contains no square.

If B′ contains two (or more) squares then one is a subword of the other and we get two different residuals of B′. This is a contradiction with B′ →_{1} ⟨B′⟩_{1} = ⟨B′⟩. So B′ contains at most one square. ⊓ ⊔

Remark 3. The same arguments as in the proof of Lemma 9 give the following analogue. If A_{1}, B, A_{2} are in normal form and A_{1}BA_{2} →_{2m} A_{1}B′A_{2} ↛_{2m} and if the residual B′ of B contains a square x^{2}, then B′ →_{1} ⟨B′⟩_{1} and x has the same properties as in Lemma 9.

Proposition 1. Let A and B be in normal form such that ⟨AB⟩_{2} = AB′ where B′ is the residual of B, then |B′| ≤ |⟨B′⟩|^{2}.

Proof. By Lemma 7 we have ⟨AB⟩_{2} = ⟨AB⟩_{2m} and we can use the maximal reductions. W.l.o.g. assume that the reductions →_{2m} did not leave out some prefix B_{1} of the word B, otherwise we can start with the words A and B_{2} where B = B_{1}B_{2}. Remark 2 shows how two applications of →_{2m} can be nested. Since A and B are in normal form, we can see that any reduction →_{2m} uses some letters from both A and B. Since A is left untouched, we can write A = s_{n+1}s_{n} … s_{1}, B = u_{1}v_{1}w_{1} … u_{n}v_{n}w_{n}u_{n+1} where s_{i}, u_{i}, v_{i}, w_{i} ∈ C^{∗} for all possible i and we have n reductions of the form

s_{n+1} … \underline{s_{i} … s_{1}u_{1}w_{1} … u_{i}}v_{i}\underline{w_{i}} … u_{n+1} →_{2m}
s_{n+1} … s_{1}u_{1}w_{1} … u_{i}w_{i} … u_{n+1}

where C(v_{i}) ⊆ C(s_{i} … s_{1}u_{1}w_{1} … u_{i}) = C(w_{i}) and B′ is of the form B′ = u_{1}w_{1} … u_{n}w_{n}u_{n+1}.

Since each step of the maximal reduction needs a new letter (the letter that immediately succeeds w_{i}), we get an upper bound for n (the number of steps in →_{2m}^{∗}), n + 1 ≤ card(C(B)). Let us denote B′′ = ⟨B′⟩_{1} = ⟨B′⟩ and w_{0} = ϵ. By induction (where i = 1, …, n) and by Lemma 9 applied on A and ⟨w_{0}u_{1} … w_{i−1}u_{i}⟩v_{i}w_{i}u_{i+1} we can see that |B′′| ≥ max_{i=1}^{n+1}{|w_{i−1}u_{i}|} since after every application xx → x we can find each w_{i−1}u_{i} as a subword in the residual of B. Hence we get |B′′| ≥ max_{i=1}^{n+1}\{|w_{i−1}u_{i}|\} ≥ \frac{1}{n+1} ∑_{i=1}^{n+1} |w_{i−1}u_{i}| = \frac{|B′|}{n+1} and from the fact n+1 ≤ card(C(B)) = card(C(B′′)) we can deduce that |⟨B′⟩|^{2} = |B′′|^{2} ≥ card(C(B′′)) · |B′′| ≥ (n + 1)\frac{|B′|}{n+1} = |B′|. ⊓ ⊔

The previous proposition can be generalized in the following way.

Proposition 2. Let A_{1}, B and A_{2} be in normal form such that ⟨A_{1}BA_{2}⟩_{2} = A′_{1}B′A′_{2} where A′_{1}, B′, A′_{2} are the residuals of A_{1}, B, A_{2}. Then |B′| ≤ 2 · |⟨B′⟩|^{2}.

Proof. We prove the assertion for A′_{1} = A_{1} and A′_{2} = A_{2}, because in the case when we leave out some occurrences of letters in A_{1} and A_{2}, we can reduce A′_{i} →_{1}^{∗} ⟨A′_{i}⟩ and start with these new surroundings ⟨A′_{1}⟩ and ⟨A′_{2}⟩ of the word B, since ⟨⟨A′_{1}⟩B⟨A′_{2}⟩⟩_{2} = ⟨A′_{1}⟩B′⟨A′_{2}⟩. So, ⟨A_{1}BA_{2}⟩_{2} = A_{1}B′A_{2} where B′ is the residual of B.

We will use the maximal reduction again and for an arbitrary word B_{i} ∈ C^{∗} we denote B′_{i} its residual (after the applications of →_{2m}). Three different cases must be discussed.

1) There is a reduction →_{2m} using letters from both A_{1} and A_{2}.

2) There is a letter in B which is not involved in any reduction →_{2m}.

3) Otherwise.

In the case 1) we can write B = B_{1}vB_{2}, A_{1} = su_{1} and A_{2} = w_{2}t where s\underline{u_{1}B_{1}}v\underline{B_{2}w_{2}}t →_{2m} A_{1}B_{1}B_{2}A_{2}. We apply twice Proposition 1 on the words A_{1}B′_{1} and B′_{2}A_{2}. We can deduce |B′| = |B′_{1}B′_{2}| = |B′_{1}| + |B′_{2}| ≤ |⟨B′_{1}⟩|^{2} + |⟨B′_{2}⟩|^{2} ≤ 2 · |⟨B′_{1}B′_{2}⟩|^{2} = 2 · |⟨B′⟩|^{2} where the last inequality holds, because by Remark 3 we have ⟨B′_{1}⟩⟨B′_{2}⟩ →_{1} ⟨B′⟩ (in the case when ⟨B′_{1}⟩⟨B′_{2}⟩ contain a square) and so |⟨B′_{1}B′_{2}⟩| ≥ max{|⟨B′_{1}⟩|, |⟨B′_{2}⟩|}, which implies that 2 · |⟨B′_{1}B′_{2}⟩|^{2} ≥ |⟨B′_{1}⟩|^{2} + |⟨B′_{2}⟩|^{2}.

In the case 2) we can write B = B_{1}B_{2}B_{3} where B_{2} is not involved in any reduction by →_{2m}. Then we have ⟨B′⟩ = ⟨B′_{1}⟩B_{2}⟨B′_{3}⟩ and so by Proposition 1 we get |B′| = |B′_{1}B_{2}B′_{3}| = |B′_{1}| + |B_{2}| + |B′_{3}| ≤ |⟨B′_{1}⟩|^{2} + |B_{2}| + |⟨B′_{3}⟩|^{2} ≤ |⟨B′_{1}⟩B_{2}⟨B′_{3}⟩|^{2} = |⟨B′⟩|^{2}.

In the case 3) we can write B = B_{1}v_{1}B_{2}B_{3}B_{4}v_{2}B_{5}, A_{1} = su_{1}, A_{2} = w_{2}t where

A_{1}BA_{2} = s\underline{u_{1}B_{1}}v_{1}\underline{B_{2}B_{3}}B_{4}v_{2}B_{5}w_{2}t →_{2m} A_{1}B_{1}B_{2}B_{3}B_{4}v_{2}B_{5}A_{2},

A_{1}BA_{2} = su_{1}B_{1}v_{1}B_{2}\underline{B_{3}B_{4}}v_{2}\underline{B_{5}w_{2}}t →_{2m} A_{1}B_{1}v_{1}B_{2}B_{3}B_{4}B_{5}A_{2}

are the unique overlapping reductions (Remark 2). We have B′ = B′_{1}B_{2}B_{3}B_{4}B′_{5} and B_{0} = ⟨B′_{1}B_{2}B_{3}⟩ is a prefix of ⟨B′⟩ = ⟨B_{0}B_{4}B′_{5}⟩, and so |B_{0}| ≤ |⟨B′⟩|. Let us now observe that |B′| = |B′_{1}B_{2}B_{3}B_{4}B′_{5}| = |B′_{1}B_{2}B_{3}| + |B_{4}B′_{5}| ≤ |⟨B′_{1}B_{2}B_{3}⟩|^{2} + |B_{0}B_{4}B′_{5}| ≤ |B_{0}|^{2} + |⟨B_{0}B_{4}B′_{5}⟩|^{2} ≤ 2 · |⟨B′⟩|^{2}. ⊓ ⊔

Lemma 10. Let sxxt be a word such that ⟨sxxt⟩_{2} = sxxt and sxxt contains another square y^{2} (|y| ≤ |x|) such that one of these occurrences of y lies inside the x^{2}. Then one of the following conditions holds:

1. y is a suffix of s and a prefix of x

2. y is a prefix of t and a suffix of x

3. y^{2} is a subword of x

Proof. Since y is a subword of x^{2}, we have C(y) ⊆ C(x) and let us suppose that conditions 1. and 2. do not hold. If |x| = |y| then we get C(x) = C(y) and we can apply →_{2} (w.l.o.g. \underline{x}v\underline{y} →_{2} xy where v is both a prefix of x and a suffix of y), which is a contradiction. Assume that |y| < |x|. Notice that the first and the last letter of x are unique occurrences of these constants in the word x because in another case we can apply →_{2l} on x^{2}. This implies that y^{2} does not contain the first letter of the right x and y^{2} also does not contain the last letter of the left x, requiring that y^{2} is a subword of x. ⊓ ⊔

Remark 4. The previous lemma shows that for two applications of the rules xx →_{1} x and yy →_{1} y on a word p in normal form w.r.t. →_{2}, one of the following conditions holds (up to symmetry):

1. xx and yy do not overlap 2. yy is a subword of x

3. x = x′z, y = zy′ and xx′zy′y is a subword of p

Lemma 11. If ⟨sxxt⟩_{2} = sxxt and sxt contains a square y^{2} which is not in sxxt then y = s_{1}xt_{1} where |s_{1}|, |t_{1}| ≥ 1.

Proof. Since y^{2} is not in sxxt, we have y^{2} = s_{0}xt_{0} where s_{0} is a suffix of s and t_{0} is a prefix of t. If x is not a subword of y then y = s_{0}x_{1}, y = x_{2}t_{0} where x = x_{1}x_{2}. Hence s_{0}xxt_{0} = \underline{s_{0}x_{1}}x_{2}x_{1}\underline{x_{2}t_{0}} →_{2} s_{0}x_{1}x_{2}t_{0} since C(x_{2}x_{1}) ⊆ C(y) = C(s_{0}x_{1}) = C(x_{2}t_{0}). The case when x_{1} or x_{2} is an empty word (i.e. x is a prefix or a suffix of y) is also included and we can conclude that y = s_{1}xt_{1} and |s_{1}|, |t_{1}| ≥ 1. ⊓ ⊔

Proposition 3. Let A and B be in normal form, card(C(AB)) ≥ 2 and ⟨AB⟩_{2} = AB. Then |AB| ≤ |⟨AB⟩|^{2}.

Proof. We denote k the length of ⟨AB⟩_{1} = ⟨AB⟩. The case k = 2 is trivial: there is no word (in normal form w.r.t. →_{2}) over a 2–letter alphabet of length greater than 4. Now we assume that k ≥ 3.

At first we have a look at the squares in AB. Since A and B are in normal form, each square has got some letters from A and some from B. By Remark 4 we have that AB contains at most two squares because the cases 1. and 2. of Remark 4 are impossible.

By Lemma 8, anytime during any reduction sequence by →_{1} the residuals of A and B remain in normal form and their concatenations are in normal form w.r.t. →_{2}. So by the previous arguments there are at most two squares and by Lemma 11, if the reduction →_{1} introduces a new square then it is larger at least by two letters than the previous one. We use the sequence of reductions which in each step reduces the smallest square. Then the last reduction in this sequence reduces a square x^{2} with the property |x| ≤ k. The previous reduction reduces a square y^{2} with the property |y| ≤ k − 1 (the case |y| = |x| = k = |⟨AB⟩| is a contradiction with AB is in normal form w.r.t. →_{2}). Thus we can see that for the length of AB we have an upper bound k + k + (k − 1) + (k − 2) + … ≤ k^{2}. ⊓ ⊔

Proposition 4. There is a polynomial p : IN → IN, such that for an arbitrary A_{1}, B, A_{2} ∈ C^{∗} in normal form and ⟨A_{1}BA_{2}⟩_{2} = A′_{1}B′A′_{2} where A′_{i}, 1 ≤ i ≤ 2, is the residual of A_{i} and B′ is the residual of B, we have |B′| ≤ p(|⟨A_{1}BA_{2}⟩|).

Proof. We may assume that card(C(B)) ≥ 2 and by Proposition 2 we know that |B′| ≤ 2 · |⟨B′⟩|^{2}, which is of course less or equal to 2·|⟨A′_{1}⟩⟨B′⟩|^{2}. Since ⟨⟨A′_{1}⟩⟨B′⟩⟩_{2} = ⟨A′_{1}⟩⟨B′⟩ by Lemma 8, we can use Proposition 3 and we get that 2 · |⟨A′_{1}⟩⟨B′⟩|^{2} ≤ 2 · |⟨A′_{1}B′⟩|^{4}, which is again less or equal to 2 · |⟨A′_{1}B′⟩⟨A′_{2}⟩|^{4}. Analogously we have that 2·|⟨A′_{1}B′⟩⟨A′_{2}⟩|^{4} ≤ 2·|⟨A′_{1}B′A′_{2}⟩|^{8}. Thus we have |B′| ≤ p(|⟨A_{1}BA_{2}⟩|) for the polynomial p(n) = 2 · n^{8}. ⊓ ⊔

Proposition 5. Let p be a polynomial that satisfies the condition from Proposition 4. If a stuttering pattern equation system {X_{1} = A_{1}, …, X_{n} = A_{n}} is satisfiable then there exists a solution α with size(α) ≤ ∑_{i=1}^{n} |X_{i}|· p(|A_{i}|).

Proof. Of course, we can assume that all A_{i}’s are in normal form. Let α be a solution of the stuttering pattern equation system {X_{1} = A_{1}, …, X_{n} = A_{n}} which minimizes both size(α) and the number of variables x such that |α(x)| = size(α). Assume for the moment that there is some x such that size(α) = |α(x)| > ∑_{i=1}^{n} |X_{i}|p(|A_{i}|). We may assume that α(x) is in normal form, otherwise we have a smaller solution.

We now reduce α(X_{i}) →_{2m}^{∗} ⟨α(X_{i})⟩_{2}. If we look at an arbitrary residual B′ of an occurrence of α(x) in ⟨α(X_{i})⟩_{2}, we see that |B′| ≤ p(|A_{i}|) by Proposition 4. This means that there are at most ∑_{i=1}^{n} |X_{i}|p(|A_{i}|) letter’s occurrences in the residuals of all occurrences of α(x) in all ⟨α(X_{i})⟩_{2}.

By the assumption |α(x)| > ∑_{i=1}^{n} |X_{i}|p(|A_{i}|) we get that there is an occurrence of a letter a in α(x), i.e. α(x) = u_{1}au_{2}, that has been left out from all the occurrences of α(x) by the rule →_{2m}. We can erase this occurrence of the letter a from α(x) and we get a smaller solution β s.t. β(y) = α(y) for y ≠ x and β(x) = u_{1}u_{2}. The homomorphism β is indeed a solution since α(X_{i}) →_{2l}^{∗} β(X_{i}). This is a contradiction because we have found a smaller solution. ⊓ ⊔

The previous considerations lead to the following corollary. Corollary 1. The Pattern-Equation problem is in NP.

Proof. We can guess a solution α and by Proposition 5, if the system is satisfiable then there is a solution of a polynomial length. Checking whether α solves all the equations takes also polynomial time and so the problem is in NP. ⊓ ⊔

5 NP–hardness of the Pattern-Equation problem

In this section we show that the Pattern-Equation problem in a free idempotent semigroup is NP–hard. We use a reduction from the NP–complete problem 3–SAT (see [17]).

Proposition 6. The Pattern-Equation problem is NP–hard.

Proof. Suppose we have an instance of 3–SAT, i.e.

C ≡ C_{1} ∧ C_{2} ∧ … ∧ C_{n}

is a conjunction of clauses and each clause C_{i}, 1 ≤ i ≤ n, is of the form

l_{1} ∨ l_{2} ∨ l_{3}

where l_{j}, 1 ≤ j ≤ 3, is a literal (l_{j} is a variable from the set Var, possibly negated – we call it positive resp. negative literal). A valuation is a mapping v : Var → {T, F }. This valuation extends naturally to C and we say that C is satisfiable if and only if there exists a valuation v such that v(C) = T.

We construct a stuttering pattern equation system such that the system is satisfiable if and only if C is satisfiable. The system will consist of the following sets of equations (1) – (6) and C = {a, b, c}, V = \{x, s_{1}^{x}, t_{1}^{x}, s_{2}^{x}, t_{2}^{x} | x ∈ Var ∪ \overline{Var}\} ∪ \{y_{a}, y_{b}, y_{c}\} where \overline{Var} = \{\overline{x} | x ∈ Var} is a disjoint copy of Var. For the constants a, b and c there are three equations

y_{a} = a, y_{b} = b, y_{c} = c.  (1)

We define x̃ = x if x is a positive literal, ˜¬x = \overline{x} if ¬x is a negative literal and for all clauses C_{i} ≡ l_{1} ∨ l_{2} ∨ l_{3} we have the equation

y_{a}l̃_{1}l̃_{2}l̃_{3}y_{a} = aba  (2)

for each x ∈ Var we add the equations

y_{b}x\overline{x}y_{b} = bab  (3)
y_{a}x\overline{x}y_{a} = aba  (4)

and finally for each x ∈ Var ∪ \overline{Var} we have the following equations:

s_{1}^{x}xt_{1}^{x} = acb, s_{1}^{x}y_{c} = ac  (5)
s_{2}^{x}xt_{2}^{x} = bca, s_{2}^{x}y_{c} = bc.  (6)

The intuition behind the construction is following. If a variable x is true then x = b and if x is false then x = a. The second equation ensures that at least one literal in each clause is true and the other equations imply consistency, i.e. a literal and its negation cannot be both true (false). In particular, the equation (3) means that at least one of x and \overline{x} contains a. Similarly for b and (4). The last two equations make sure that a variable x ∈ Var ∪ \overline{Var} cannot contain both a and b.

Suppose that C is satisfiable, i.e. there is a valuation v such that v(C) = T. Then we show that α defined below is a solution of our system. Let us state

α(y_{a}) = a, α(y_{b}) = b, α(y_{c}) = c

and for all x ∈ Var such that v(x) = T let

α(x) = b, α(\overline{x}) = a

α(s_{1}^{x}) = ac, α(t_{1}^{x}) = b, α(s\overline{x} ; 1) = a, α(t\overline{x} ; 1) = cb

α(s_{2}^{x}) = b, α(t_{2}^{x}) = ca, α(s\overline{x} ; 2) = bc, α(t\overline{x} ; 2) = a

and if v(x) = F then

α(x) = a, α(\overline{x}) = b

α(s_{1}^{x}) = a, α(t_{1}^{x}) = cb, α(s\overline{x} ; 1) = ac, α(t\overline{x} ; 1) = b

α(s_{2}^{x}) = bc, α(t_{2}^{x}) = a, α(s\overline{x} ; 2) = b, α(t\overline{x} ; 2) = ca.

Checking that α is a solution (even non-singular) is a routine. The only interesting equation is (2). This equation is also satisfied by α since we have the assumption that under the valuation v there is at least one true literal in each clause.

Let us suppose that α is an arbitrary solution of our system and we find a valuation that satisfies C. The equation (3) implies that C(α(x)) ⊆ \{a, b\} for all x ∈ Var ∪ \overline{Var}. We will conclude that it is not possible that C(α(x)) = {a, b}.

Suppose that it is the case and using the equations (5) we get that α(x) does not begin with the constant a. For the moment assume that α(x) begins with a. We have ac = 0(acb) ∼ 0(α(s_{1}^{x}xt_{1}^{x})) and from (1) and (5) we get that a ∈ C(α(s_{1}^{x})) ⊆ {a, c}. If C(α(s_{1}^{x})) = {a} then C(0(α(s_{1}^{x}xt_{1}^{x}))) = {a, b} whereas C(0(acb)) = {a, c}, which is a contradiction. Otherwise we have C(α(s_{1}^{x})) = {a, c} and we get 0(α(s_{1}^{x}xt_{1}^{x})) ∼ aca ≁ ac = 0(acb).

By the similar arguments and using the equations (6) we get that α(x) does not begin with the constant b. This yields that there are just three possibilities for α(x), namely α(x) ∼ a, α(x) ∼ b or α(x) = ϵ.

By the equations (3) and (1) we know that for all x ∈ Var at least α(x) ∼ a or α(\overline{x}) ∼ a. The equation (4) implies that either α(x) ∼ b or α(\overline{x}) ∼ b. Similarly for each clause, the equation (2) with (1) gives that there is j, 1 ≤ j ≤ 3, such that α(l̃_{j}) ∼ b. Let us finally define the valuation v as v(x) = T if α(x) ∼ b and v(x) = F if α(x) ∼ a for each x ∈ Var. The valuation is consistent and it holds that v(C) = T.

This is enough to demonstrate that the Pattern-Equation problem is NP–hard since the reduction can be done effectively in polynomial time. ⊓ ⊔

It is not difficult to see that the same reduction as above would also work for the Non-Singular-Pattern-Equation problem, which is consequently also NP–hard. We can now formulate the main result of this paper.

Theorem 1. Pattern-Equation and Non-Singular-Pattern-Equation problems are NP–complete.

As an immediate corollary of this theorem (using Remark 1), we get the following result.

Corollary 2. AI-matching with only one associative and idempotent function symbol is NP–complete.

Acknowledgements We would like to thank Ivana Černá and Michal Kunc for their comments and suggestions.

References

[1] Baader F.: The Theory of Idempotent Semigroups is of Unification Type Zero, J. of Automated Reasoning 2 (1986) 283–286.

[2] Baader F.: Unification in Varieties of Idempotent Semigroups, Semigroup Forum 36 (1987) 127–145.

[3] Baader F., Schulz K.U.: Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures, J. Symbolic Computation 21 (1996) 211–243.

[4] Baader F., Siekmann J.H.: Unification Theory, Handbook of Logic in Artificial Intelligence and Logic Programming (1993) Oxford University Press.

[5] Book R., Otto F.: String-Rewriting Systems (1993) Springer–Verlag.

[6] Černá I., Klíma O., Srba J.: Pattern Equations and Equations with Stuttering, In Proceedings of SOFSEM’99, the 26th Seminar on Current Trends in Theory and Practice of Informatics (1999) 369-378, Springer–Verlag.

[7] Green J.A., Rees D.: On semigroups in which x^{r} = x, Proc. Camb. Phil. Soc. 48 (1952) 35–40.

[8] Klíma O., Srba J.: Complexity Issues of the Pattern Equations in Idempotent Semigroups, Technical report FIMU-RS-99-02, Faculty of Informatics MU (1999).

[9] Klíma O., Srba J.: Matching Modulo Associativity and Idempotency is NP– complete, In Proceedings of MFCS’00, the 25rd International Symposium on Mathematical Foundations of Computer Science (2000) To appear.

[10] Kaďourek J., Polák L.: On free semigroups satisfying x^{r} = x , Simon Stevin 64, No.1 (1990) 3–19.

[11] Kapur D., Narendran P.: NP–completeness of the Set Unification and Matching Problems, In Proceedings of CADE’86, Springer LNCS volume 230 (1986) 489– 495, Springer–Verlag.

[12] Kopeček I.: Automatic Segmentation into Syllable Segments, Proceedings of First International Conference on Language Resources and Evaluation (1998) 1275– 1279.

[13] Kopeček I., Pala K.: Prosody Modelling for Syllable-Based Speech Synthesis, Proceedings of the IASTED International Conference on Artificial Intelligence and Soft Computing, Cancun (1998) 134–137.

[14] Lothaire M.: Algebraic Combinatorics on Words, Preliminary version available

at http://www-igm.univ-mlv.fr/∼berstel/Lothaire/index.html

[15] Lothaire, M.: Combinatorics on Words, Volume 17 of Encyclopedia of Mathematics and its Applications (1983) Addison-Wesley.

[16] Makanin, G. S.: The Problem of Solvability of Equations in a Free Semigroup, Mat. Sbornik. 103(2) (1977) 147–236. (In Russian) English translation in: Math. USSR Sbornik 32 (1977) 129–198.

[17] Papadimitriou, C.H.: Computational Complexity, Addison-Wesley Publishing Company (1994), Reading, Mass.

[18] Perrin D.: Equations in Words, In H. Ait-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, Vol. 2 (1989) 275–298, Academic Press.

[19] Schulz, K. U.: Makanin’s Algorithm for Word Equations: Two Improvements and a Generalization, In Schulz, K.–U. (Ed.), Proceedings of Word Equations and Related Topics, 1st International Workshop, IWW-ERT’90, Tübingen, Germany, Vol. 572 of LNCS (1992) 85–150, Berlin-Heidelberg-New York, Springer–Verlag.

[20] Schmidt-Schauss M.: Unification under Associativity and Idempotence is of Type Nullary, J. of Automated Reasoning 2 (1986) 277–281.

[21] Siekmann J., Szabó P.: A Noetherian and Confluent Rewrite System for Idempotent Semigroups, Semigroup Forum 25 (1982).

Recent BRICS Report Series Publications

RS-00-13 Ondřej Klíma and Jiří Srba. Matching Modulo Associativity and Idempotency is NP-Complete. June 2000. 19 pp. To appear in Mathematical Foundations of Computer Science: 25 th International Symposium, MFCS ’00 Proceedings, LNCS, 2000.

RS-00-12 Ulrich Kohlenbach. Intuitionistic Choice and Restricted Classical Logic. May 2000. 9 pp.

RS-00-11 Jakob Pagter. On Ajtai’s Lower Bound Technique for R-way Branching Programs and the Hamming Distance Problem. May 2000. 18 pp.

RS-00-10 Stefan Dantchev and Søren Riis. A Tough Nut for Tree Resolution. May 2000. 13 pp.

RS-00-9 Ulrich Kohlenbach. Effective Uniform Bounds on the Krasnoselski-Mann Iteration. May 2000. 34 pp.

RS-00-8 Nabil H. Mustafa and Aleksandar Pekeč. Democratic Consensus and the Local Majority Rule. May 2000. 38 pp.

RS-00-7 Lars Arge and Jakob Pagter. I/O-Space Trade-Offs. April 2000. To appear in 7th Scandinavian Workshop on Algorithm Theory, SWAT ’98 Proceedings, LNCS, 2000.

RS-00-6 Ivan B. Damgård and Jesper Buus Nielsen. Improved Non-Committing Encryption Schemes based on a General Complexity Assumption. March 2000. 24 pp.

RS-00-5 Ivan B. Damgård and Mads J. Jurik. Efficient Protocols based on Probabilistic Encryption using Composite Degree Residue Classes. March 2000. 19 pp.

RS-00-4 Rasmus Pagh. A New Trade-off for Deterministic Dictionaries. February 2000.

RS-00-3 Fredrik Larsson, Paul Pettersson, and Wang Yi. On Memory-Block Traversal Problems in Model Checking Timed Systems. January 2000. 15 pp. Appears in Graf and Schwartzbach, editors, Tools and Algorithms for The Construction and Analysis of Systems: 6th International Conference, TACAS ’00 Proceedings, LNCS 1785, 2000, pages 127–141.

RS-00-2 Igor Walukiewicz. Local Logics for Traces. January 2000. 30 pp.