Mika Hirvensalo

Etienne Moutot
email: etienne.moutot@ens-lyon.org

Abuzer Yakaryılmaz
email: abuzer@lu.lv

On the computational power of affine automata

Keywords: non-classical models of automata, affine automata, cutpoint languages, bounded error, compact sets, error reduction

 by showing that any affine language can be recognized by an AfA with certain limitation on the entries of affine states and transition matrices. Lastly, we present the first languages shown to be not recognized by AfAs with bounded-error.

Introduction

Finite automata are interesting computational models because of their simplicity, compared to more complex models like pushdown automata or Turing machines. They also represent a very concrete restriction on computation: they only have a finite memory. A lot of different automata models have been studied during the years, such as deterministic [START_REF] Sipser | Introduction to the Theory of Computation, 3rd edition[END_REF], probabilistic [START_REF] Paz | Introduction to Probabilistic Automata[END_REF] and quantum [START_REF] Ambainis | Automata: From Mathematics to Applications, chap[END_REF] ones. All these models share two common features: the state vector set is compact and the acceptance function can be interpreted as linear. The linearity is desirable because of mathematical simplicity, but on the other hand, it may represent a limitation on the computational power.

Jeandel [START_REF] Jeandel | Topological automata[END_REF] demonstrated that in the bounded-error acceptance model the finite automata with compact state set accept only regular languages. Hence the compactness property of the state set may be one very important limiting the computational power, but since most known models have a compact state set, it remains open how much the compactness of the state set actually contributes.

Recently, A. Díaz-Caro and A. Yakaryılmaz introduced a new model, called affine automata [START_REF] Díaz-Caro | Affine computation and affine automaton[END_REF], also investigated in [START_REF] Villagra | Language recognition power and succintness of affine automata[END_REF] and [START_REF] Belovs | Can one quantum bit separate any pair of words with zero-error?[END_REF]. It is a purely theoretical model, which means that it cannot be implemented by a physical device like quantum automata. But it allows us to investigate on the power of interference caused by negatives amplitudes in the computation, like in the quantum case. Moreover, this model allows us to study the effect of state set compactness, since unlike quantum automata, affine ones have an unbounded state set. In addition, the final operation corresponding to quantum measurement cannot be interpreted as linear, but it is analogous to renormalization in Kondacs-Watrous [START_REF] Kondacs | On the power of quantum finite state automata[END_REF] and Latvian [START_REF] Ambainis | Algebraic results on quantum automata[END_REF] quantum automata models.

In this paper, we present some stability results (Section 3): we show how to obtain a new AfA from two AfAs by tensoring and direct sum. Then, we present a simpler proof for how to change the cutpoint for any affine language and an error reduction method in bounded error case.

Any entry of an affine state or a transition matrix can be arbitrarily away from zero. Here, by addressing to the question of [START_REF] Díaz-Caro | Affine computation and affine automaton[END_REF], we show that (Section 4) any affine language can be recognized by an AfA with the restriction that all the entries of transition matrices are in the interval [-1, 1]. We also show that by an additional state we can guarantee that any AfA can start its computation from the first deterministic state.

Finally, we present (Section 5) the first languages shown not to be recognized by any bounded-error AfA.

Preliminaries

We denote the input alphabet Σ and the empty string ε.

Probabilistic automata are a generalization of deterministic finite automata that can make random choices [START_REF] Rabin | Probabilistic automata[END_REF]. Formally, a probabilistic finite automaton (PFA) P is a 5-tuple P = (E, Σ, {M x | x ∈ Σ}, e s , E a ), where E = {e 1 , . . . , e k } is the finite set of states of P , {M x | x ∈ Σ} is the set of stochastic transition matrices (all their coefficients are real numbers in [0, 1] and their columns sums up to 1), v 0 is the initial probabilistic state (the probability distribution on the states), and E a ⊆ E is the set of accepting states. The computation starts in v 0 , and then the given input, say w = w 1 • • • w n ∈ Σ * for some n > 0, is read once from left to right symbol by symbol. For each symbol the corresponding transition matrix is applied:

v f = M w v 0 = M wn • • • M w1 v 0 . Remark that if w = ε, v f = v 0 .
The accepting probability of P on w is given by

f P (w) = pM w v 0 , ( 1
)
where

p = δ 1 • • • δ k and δ i = 1 if e i ∈ E a and 0 if e i / ∈ E a .
Affine automata are a generalization of PFAs allowing negative transition values. Only allowing negative values in the transition matrices does not add any power (generalized probabilistic automata are equivalent to usual ones [START_REF] Turakainen | Generalized automata and stochastic languages[END_REF]), but affine automata introduces also a non-linear behaviour. The automaton acts like usual generalized probabilistic automaton until the last operation, a non-linear operation called weighting.

A vector v ∈ R n is an affine vector if and only if its coordinates sums up to 1. A matrix M is an affine matrix if and only if all its columns are affine vectors. Remark that if M and N are affine matrices , then M N is also an affine matrix. In particular, if v is an affine vector, then M v is also an affine vector.

Formally, an affine finite automaton (AfA) A is a 5-tuple

A = (E, Σ, {M x | x ∈ Σ}, v 0 , E a )
where all components exactly the same as for probabilistic automata by replacing stochastic property with affine one in the initial state and transition matrices.

As in PFAs, after reading a word

w = w 1 • • • w n , the final state of A is v f = M w v 0 like in the probabilistic case, but the function f A : Σ * → [0, 1] computed by A is defined as f A (w) = ei∈Ea |(v f ) i | ei∈E |(v f ) i | , ( 2
)
and referred as the accepting value of A on w. Similar to projective measurements, we can rewrite Eq. ( 2) as given below. First, we define a projection matrix based on E a :

PA = P =     δ1 δ2 . . . δn     , where δ i = 1 if e i ∈ E a 0 otherwise .
Then, we can denote f A (•) as

f A (w) = |P M w v 0 | |M w v 0 | . ( 3
)
Notice that the final value for PFA P (1) is defined as matrix product v f → p.v f , which is a linear operation on v f . On the other hand, computing final value from

v f as in (3) involves nonlinear operations v f → |P v f | |v f |
due to absolute value and normalization of affine states having length greater than 1. Given a function f : Σ * → [0, 1] computed by an automaton (stochastic or affine), there are different ways of defining the language of an automaton. The natural one is as follows: A language L ⊆ Σ * is recognized by an automaton A with cutpoint λ if and only if

L = {w ∈ Σ * | f A (w) > λ}.
These languages are called cutpoint languages. In the case of probabilistic (resp. affine automata), the set of cut-point languages are called stochastic languages (resp. affine languages) and denoted by SL (resp. AfL).

A stronger condition is to impose that accepted and rejected words are separated by a gap: the cutpoint is said to be isolated: A language L is recognized by an automaton A with isolated cutpoint λ if and only if there exist δ > 0 such that ∀w ∈ L, f A (w) ≥ λ + δ, and ∀w / ∈ L, f A (w) ≤ λ -δ.

As we shall see, for affine automata it is always possible to shift the cutpoint λ ∈ (0, 1) to λ = 1 2 , and hence this notion of isolated cutpoint becomes equivalent to the bounded error recognition: Language L ⊆ Σ * is said to be recognized by an automaton A with bounded error if and only if there exists ε > 0 such that ∀w ∈ L, f A (w) ≥ 1 -ε, and ∀w / ∈ L, f A (w) ≤ ε. The set of languages recognized with bounded error (or isolated cutpoint) affine automata is denoted by BAfL.

A classical result by Rabin [START_REF] Rabin | Probabilistic automata[END_REF] shows that isolated cutpoint stochastic languages are regular (denoted REG). Rabin's proof essentially relies on two facts: 1) the function mapping the final vector into [0, 1] is a contraction, and 2) the state vector set is bounded.

By modifying Rabin's proof, it is possible to show that also many quantum variants of stochastic automata obey the same principle [START_REF] Li | Characterizations of one-way general quantum finite automata[END_REF] bounded-error property implies the regularity of the accepted languages. In fact, E. Jeandel generalized Rabin's proof by demonstrating that the compactness of the state vector set together with the continuity of the final function are sufficient to guarantee the regularity of the accepted language if the cutpoint is isolated [START_REF] Jeandel | Topological automata[END_REF].

In the affine case however, the vector states do not lie in a compact set, we cannot prove that BAfL = REG like in the probabilistic (or even quantum) case [START_REF] Jeandel | Topological automata[END_REF]. In fact, it is even the contrary: REG BAfL [START_REF] Díaz-Caro | Affine computation and affine automaton[END_REF].

We close this section by three basic facts. The following three operations on the state sets will be useful, when constructing new automata from the existing ones:

-

E = {e i | e i / ∈ E} the complement of E, -E a × E b = {(e i , e j ) | e i ∈ E a , e j ∈ E b } the Cartesian product of E a and E b , -E a ∪ E b = {e i | e i ∈ E a or e i ∈ E b } the union of E a and E b .
The following lemma shows how to formulate the above operations by using the formalism of projection matrices.

Stability Results

The main results of this section are stability results. The first are about the functions of affine automata. They provide a way to prove an error reduction theorem. We then use this theorem to show the stability of bounded-error affine languages under intersection and union.

Proposition 4. Let f , g be functions computed by affine automata, then there exists an affine automaton C such that f C = f × g.

Proof. The proof is the same as the stochastic case and essentially relies on the property of tensor product of Lemma 3.

It is easy to design a 2-state PFA P such that f P : Σ * → α for α ∈ [0, 1]. Thus:

Corollary 5 Let f be a function computed by an AfA and α ∈ [0, 1], then there exists an AfA C such that f C = αf . Proposition 6. Let f , g be functions computed by some AfAs and α, β ≥ 0 such that α + β = 1, then there exists an AfA C such that f C = αf + βg.

Proof. Let A = (E A , Σ, {A x }, v A 0 , E A a ) and B = (E B , Σ, {B x }, v B 0 , E B a ) two automata such that f = f A and g = f B .
The idea here is to make two copies of A ⊗ B working in parallel, one having the final states of A, the other the final states of B. We define

C = (E C , Σ, {C x }, v C 0 , E C a ) by: Cx =        Ax ⊗ Bx 0 0 Ax ⊗ Bx        , v C 0 =        α(v A 0 ⊗ v B 0 ) β(v A 0 ⊗ v B 0 )        , P C =        P A ⊗ In 0 0 I k ⊗ P B       
, with P A , P B and P C be the projections on E A a , E B a and E C a . Thus,

f C (w) = α|(P A ⊗ I n )(A x ⊗ B x )(v A 0 ⊗ v B 0 )| + β|(I k ⊗ P B )(A x ⊗ B x )(v A 0 ⊗ v B 0 )| (α + β)|(A x ⊗ B x )(v A 0 ⊗ v B 0 )| = α |P A A w v A 0 | |A w v A 0 | + β |P B B w v B 0 | |B w v B 0 | = αf (w) + βg(w).
The first consequence of these stability results is a really short proof for shifting the cutpoint of an affine automaton. Although the construction in [START_REF] Díaz-Caro | Affine computation and affine automaton[END_REF] gives a much more compact automata in term of number of states, our construction is simpler, and does not require as many specific cases.

Proposition 7.

Let A be an affine automaton and λ 1 , λ 2 ∈ [0, 1]. There exists an affine automaton B such that

-f A (w) > λ 1 ⇔ f B (w) > λ 2 and -f A (w) = λ 1 ⇔ f B (w) = λ 2 .
Proof. First we suppose λ 1 = 1. Let B the automaton such that

f B = αf A + (1 - α)1, with α = 1-λ2 1-λ1 . Then f A > λ 1 ⇒ f B > (1-λ2)λ1+λ2-λ1 1-λ1 = λ 2 .
And one has the same with = or <.

For λ 1 = 1 it is even simpler, one has just to "resize" the function by taking B such that f B = λ 2 f A . And then, f A = 1 ⇒ f B = λ 2 , and same for <.

Using the same kind of construction we can prove that bounded-error mode, it is always possible to reduce the error. Reducing the error means increasing the gap between accepted and rejected words. The error probability could even be made as close to zero as one wants.

Lemma 8. Let f be a function computed by affine automaton, then there exists an affine automaton B such that

f B = f 2 (3 -2f ). Proof. Let A = (E, Σ, {A x }, v 0 , E a ) such that f = f A .
The automaton B will run 3 copies of A in parallel, and its final states are made to accept if 2 or 3 copies of A accept and reject otherwise (i.e. taking the majority answer). Formally,

B = (E ⊗ E ⊗ E, Σ, {B x }, v 0 , E a ) with B x = A x ⊗ A x ⊗ A x , v 0 = v 0 ⊗ v 0 ⊗ v 0 , E a = (E a × E a × E a ) ∪ E a × E a × E a ∪ E a × E a × E a ∪ E a × E a × E a .
Note that the four sets in parenthesis are all pairwise disjoints. Let P and P be the projections associated to E a and E a . Then, P = P ⊗ P ⊗ P + (I -P ) ⊗ P ⊗ P + P ⊗ (I -P ) ⊗ P + P ⊗ P ⊗ (I -P ).

And by Lemma 1,

f B (w) = |P B w v 0 | |B w v 0 | = |P A w v 0 | 3 + 3|P A w v 0 | (|A w v 0 | -|P A w v 0 |) |A w v 0 | 3 = f (w) 3 + 3f (w) 2 (1 -f (w)) = f (w) 2 (3 -2f (w)).

Proposition 9 (error reduction). Let L ∈ BAfL.

There exists an affine automaton A such that:

-∀w ∈ L, f A (w) ≥ 3 4 -∀w / ∈ L, f A (w) ≤ 1 4
Proof. We do not detail the proof, but the idea is simple: mapping x → x 2 (3-2x) has attracting points at x = 0 and x = 1. Iterating the mapping, any point = 1 2 will tend to 0 or 1.

This technique could be applied to get any constant instead of 1 4 , to have an error bound as small as one wants.

This error reduction theorem also applies to probabilistic automata, but is not very interesting because in the probabilistic case it is known that bounded-error languages are exactly regular languages [START_REF] Jeandel | Topological automata[END_REF], and hence the error probability could always be 0. In our case, bounded-error languages are more complex than regular languages. But thanks to this error reduction, they are stable under union, intersection, and complement, just like regular languages.

Proposition 10. Let L

A , L B ∈ BAfL. Then -L A ∪ L B ∈ BAfL, -L A ∩ L B ∈ BAfL, -L A ∈ BAfL.
Proof. Let A and B be automata recognizing L A and L B with error bound ε at most 1 4 (thanks to Theorem 9). We define C and D such that

f C = 1 2 (f A + f B ) and f D = f A f B . Let w ∈ Σ * .
We study the 4 possible options depending on the membership of w to L A and L B .

- For the complement one has just to make a copy of A with accepting states E a . The resulting function will be 1 -f A , leading to accept the rejected words of A and vice-versa.

w ∈ L A , w ∈ L B (i.e. w ∈ LA ∪ LB, w ∈ LA ∩ LB) ⇒ f C ≥ 3 4 and f D ≥ 9 16 , -w ∈ L A , w / ∈ L B (i.e. w ∈ LA ∪ LB, w / ∈ LA ∩ LB) ⇒ f C ≥ 3 8 and f D ≤ 1 4 , -w / ∈ L A , w ∈ L B (i.e. w ∈ LA ∪ LB, w / ∈ LA ∩ LB) ⇒ f C ≥ 3 8 and f D ≤ 1 4 , -w / ∈ L A , w / ∈ L B (i.e. w / ∈ LA ∪ LB, w / ∈ LA ∩ LB) ⇒ f C ≤

Equivalent Forms of Affine Automata

General affine automata are hard to study because of the lack of structure of their transition matrices and state vectors. We provide here some equivalent forms which have more restrictive properties. These equivalent forms are useful not only because it provides simpler equivalent models but also because they provide a way understand the power of affine computation.

The first result is that assuming the initial affine (probabilistic) state as the first deterministic state does not change the power of AfAs (PFAs).

Proposition 11.

Let A be an affine automaton with n states, there exist B with n + 1 states with the initial state (1, 0, . . . , 0) and such that

f A = f B . Proof. Let A = (E, Σ, {A x }, v 0 , E a ). Then, B = (E ∪{e }, Σ, {B x }, v 0 , E a ), with v 0 = (1, 0, . . . , 0) T and B x =     0 0 • • • 0 A x v 0 A x     . Thus we can deduce f B = f A from B w v 0 = B wn . . . B w2 B w1 v 0 =     0 0 • • • 0 A w v 0 A w          1 0 . . . 0      =     0 A w v 0     .
Then we prove that one could also assume that all state vectors and transition matrices have coefficients only in [-1, 1]. Proof. Let A = (E = {e 1 , . . . , e k }, Σ, {A x }, v 0 = (1, 0, . . . , 0) T , E a ) be an AfA such that w ∈ L ⇔ f A (w) > 1 2 , and C = max x,i,j |(A x ) i,j |. Then, B is as follows:

Proposition 12. Any language in AfL can be recognized by a AfA B with cutpoint

B = (E ∪ {e n+1 , e n+2 }, Σ, {B x }, v 0 , E a ∪ {e n+1 }) with B x = 1 2kC        0 0 2A x . . . . . . 0 0 kC -1 . . . kC -1 2kC 0 kC -1 . . . kC -1 0 2kC        and v 0 = (1, 0, . . . , 0) T . Then, with w = w 1 • • • w n , we can deduce that Bw = Bw n • • • Bw 2 Bw 1 = 1 2(kC) n       0 0 2Aw . . . . . . 0 0 (kC) n -1 . . . (kC) n -1 2(kC) n 0 (kC) n -1 . . . (kC) n -1 0 2(kC) n      
, which gives the final values of the states: [START_REF] Ambainis | Algebraic results on quantum automata[END_REF]: the values of the states are bounded. Now, one has

v f = B w v 0 = 1 (kC) n            . . . v f . . . (kC) n -1 2 (kC) n -1 2            . Since |(v f ) i | ≤ k n-1 C n , it is clear that |(v f ) i | ≤ [-1,
f B = |P A w v 0 | + (kC) n -1 2 |A w v 0 | + (kC) n -1 ,
and so,

w ∈ L ⇔ f A > 1 2 ⇔ |P A w v 0 | > 1 2 |A w v 0 | ⇔ |P A w v 0 | + (kC) n -1 2 > 1 2 (|A w v 0 | + (kC) n -1) ⇔ f B > 1 2 .

The first languages shown to be not in BAfL

This part is dedicated to prove that some languages are not recognizable by affine automata. This is an adaptation of the proof of Turakainen [START_REF] Turakainen | On nonstochastic languages and homomorphic images of stochastic languages[END_REF] for non-stochastic languages. All the difficulty of exhibiting a non-affine language relies in the fact that a large majority of non-stochasticity proof are based on the linearity of the automaton, which is not the case in the affine case. This proof however, is more based on some "regularity" induced by the matrix-based operations, and number theoretic properties of languages like P rime. Hence it was possible to adapt it for the affine case, where the only non-linear operation is the final projection.

Let L ⊆ a * be a unary language. We call lower density of L the limit

dens(L) = lim inf n→∞ {a k ∈ L | k ≤ n} n + 1 . Let (x n ) be a sequence of vectors in R k and I = [a 1 , b 1 ) × • • • × [a k , b k ) be an "interval". We define C(I, n) as C(I, n) = |{x i mod 1 ∈ I | 1 ≤ i ≤ n}|.
We say that (x n ) is uniformly distributed mod 1 if and only if for any I of such type,

lim n→∞ C(I, n) n = (b 1 -a 1 ) • • • (b k -a k ).
Proposition 13. If L ⊆ a * satisfies the following conditions:

1. dens(L) = 0.

2. For all Q ∈ N * , there exist h ∈ N and an infinite sequence (n i ) ∈ N N such that a h+niQ ⊆ L and for any irrational number α, the sequence

((h + n i Q)α) i∈N is uniformly distributed mod 1.
Then L is non-affine (L / ∈ BAfL).

Proof. Let's assume for contradiction that L ∈ BAfL. Then there exists an affine automaton A with s states such that

f A (a n ) = |P M n v| |M n v|
and there exists ε > 0 such that

-∀w ∈ L, f A (w) ≥ 1 -ε, -∀w / ∈ L, f A (w) ≤ ε. Note that |M n v| = s i=1 |(M n v) i | ≥ s i=1 (M n v) i = 1 (triangle inequality).
Hence the denominator of f A is never 0, and so f A is continuous.

Using the Jordan decomposition M = P JP -1 , one has M n = P J n P -1 . So the coordinates v i of M n v have the form

v i = s k=1 p ik (n)λ n k (4)
where λ i are the eigenvalues of M and p ik are polynomials of degree less than the degree of the corresponding eigenvalue. Let λ i = |λ i |e 2iπθi , we assume

|λ 1 | = • • • = |λ s | > |λ s +1 | • • • . Let λ = |λ 1 |
be the largest module of all eigenvalues and r be the maximum degree of all polynomials p ik , where k ≤ s . Then, one can use (4) to write

|M n v| = i∈E |v i | = λ n n r   i∈E s k=1 a ik e 2iπnθ k + g E (n)  
where a ik is the coefficient of degree r of p ik (note that one can have a ik = 0 for some a, k), and g E a function such that lim n→∞ g E (n) = 0. Similarly,

|P M n v| = i∈Ea |v i | = λ n n r   i∈Ea s k=1 a ik e 2iπnθ k + g Ea (n)   . Now let F (n) = f (a n ).
Using the previous equations, one has

F (n) = |P M n v| |M n v| = λ n n r i∈Ea s k=1 a ik e 2iπnθ k + g Ea (n) λ n n r i∈E s k=1 a ik e 2iπnθ k + g E (n) = i∈Ea s k=1 a ik e 2iπnθ k + g Ea (n) i∈E s k=1 a ik e 2iπnθ k + g E (n)
.

We define

G(n) = i∈Ea s k=1 a ik e 2iπnθ k i∈E s k=1 a ik e 2iπnθ k .
As lim n→∞ g Ea (n) = 0 and lim n→∞ g E (n) = 0, one has G(n) ∼ F (n), and so,

lim n→∞ |F (n) -G(n)| = 0. (5)
We define A = {k | 1 ≤ k ≤ s , θ k / ∈ Q} the indices of the "first" eigenvalue angles that are not rational. Let Q, h and the sequence (n i ) be as in the statement. Using the periodic behaviour induced by rational angle of eigenvalues, and by taking a subsequence of the initial one, one can also assume that (n i ) is such that

G(h + n i Q) = i∈Ea k∈A a ik e 2iπ(h+niQ)θ k + c i∈E k∈A a ik e 2iπ(h+niQ)θ k + d with c, d some constants.
By assumption, for all k ∈ A, the sequence ((h + n i Q)θ k ) i is uniformly distributed modulo 1. The consequence is that the values e 2iπ(h+niQ)θ k are dense in the unit circle. If for some n, G(h + nQ) < 1 2 , there exists ε > 0 such that G(h + nQ) ≤ 1 2 -ε. Then, thanks to the density argument, there are arbitrarily large values of i for which G(h

+ n i Q) ≤ 1 2 -ε 2 . Since for i sufficiently large, |F (h + n i Q) -G(h + n i Q)| ≤ ε 2 (using (5)), one has F (h + n i Q) ≤ 1 2
, and so a h+niQ / ∈ L, contradicting condition 2 of the statement.

Therefore, G(h + nQ) ≥ 1 2 for large enough n. Because G is not identically equal to 1 2 (if it is the case, F would be as close to 1 2 as one wants, which is impossible since L ∈ BAfL), again using density, there must be some ε > 0 and

k 0 such that G(h + k 0 Q) ≥ 1 2 + . First if A = ∅, it
means that all the angles of the eigenvalues θ 1 , . . . , θ s are rational. We can then write them as θ k = l k m k . Then G(n) takes a finite number of values, and these values only depend on (n mod m 1 ), . . . , (n mod m s ). Let's call k 1 = h + k 0 Q the number where G is larger than 1 2 : G(n 1 ) > 1 2 . G has the same value for all n ∈ Z = {k 1 + km 1 • • • m s |k ∈ N} (because for n in this set, the values of all (n mod m 1 ), . . . , (n mod m s ) are the same). Then, thanks to (5), one has, for n ∈ Z sufficiently large, Note that G(h + n i Q) = R((e 2iπ(h+niQ)θ k ) k∈A ). Then, because the sequences ((h + n i Q)θ k ) i are uniformly distributed modulo 1, it follows that any value obtained by the function R((e 2iπy k ) k∈A ) can be approximated by some G(h+n i Q) with arbitrary precision. The function R is continuous, therefore there exists an interval I = (x 1 , y 1 , ...) = ((x k , y k )) k∈A on which R((x k )) > 1 2 + ε 2 . So, if n i is large enough and satisfies ((h + n i Q)θ 1 mod 1, . . . ) = ((h + n i Q)θ k mod 1) k∈A ∈ I, then G(h + n i Q) > 1 2 + ε 2 , which implies F (h + n i Q) > 1 2 and hence a h+niQ ∈ L. Now we just have to prove that the sequence (h + n i Q) is "dense enough" to have dens(L) > 0, contradicting again condition 1. Because of uniform distribution imposed by condition 2, one has

F (n) > 1 2 , so {a n | n ∈ Z, n ≥ n 1 } ⊆ L. And because |{a n | n ∈ Z, n ≥ n 1 }| ∼ n m1•••m s
d = lim i→∞ C(I, h + n i Q) h + n i Q = k∈A (y k -x k )
And so for i large enough, C(I,h+niQ) h+niQ ≥ d 2 , with a h+niQ ∈ L, implying dens(L) > 0. We have proved that L cannot be affine.

Turakainen [START_REF] Turakainen | On nonstochastic languages and homomorphic images of stochastic languages[END_REF] proved that P rime = {a p | p is prime} and P oly(q) = {a q(n) | n ∈ N, q(n) ≥ 0} (where q is any polynomial of degree > 2 with nonnegative coefficients) both satisfy the two conditions of Theorem 13. Hence they are not in BAfL .

Corollary 14 P rime /

∈ BAfL and P oly(q) / ∈ BAfL.

Conclusion

In this paper we demonstrated that even if they are strictly more powerful, bounded-error languages of affine automata share stability properties with regular languages (which are bounded-error languages of stochastic automata). We also showed that the computational power of affine automata does not come alone from the unboundedness state vector set: the general model of unbounded state vector set can always be simulated with a bounded state vector set. Hence some of the computational power of affine automata comes from the nonlinear nature of the final projection, at least in the case of unbounded-error computation.

1 2

 1 such that each entry of affine states during the computation is always in [-1, 1].

,

  one has dens(L) > 0, which contradicts condition 1 of the statement.Next, ifA = ∅. Let R((x k ) k∈A ) = i∈Ea k∈A a ik x k + c i∈E k∈A a ik x k + d .

  C and D are deciding L A ∪ L B and L A ∩ L B with bounded error.

	Because 3 8 > 1 4 and 9 16 > 1 4 ,	1 4 and f D ≤ 1 16 .

Partially supported by Väisälä Foundation Partially supported by TUCS COM 3 -project and ANR project CoCoGro (ANR-16-CE40-0005) Partially supported by TUCS COM 3 -project and ERC Advanced Grant MQC


Andreas Fellner
email: andreas.fellner@ait.ac.at

Pascal Fontaine

Bruno Woltzenlogel Paleo

NP-completeness of small conflict set generation for congruence closure

Keywords: Satisfiability Modulo Theories, Decision procedures, Congruence closure, Complexity

The efficiency of Satisfiability Modulo Theories (SMT) solvers is dependent on the capability of theory reasoners to provide small conflict sets, i.e. small unsatisfiable subsets from unsatisfiable sets of literals. Decision procedures for uninterpreted symbols (i.e. congruence closure algorithms) date back from the very early days of SMT. Nevertheless, to the best of our knowledge, the complexity of generating smallest conflict sets for sets of literals with uninterpreted symbols and equalities had not yet been determined, although the corresponding decision problem was believed to be NP-complete. We provide here an NP-completeness proof, using a simple reduction from SAT.

Introduction

Satisfiability Modulo Theory solvers are nowadays based on a cooperation between a propositional satisfiability (SAT) solver and a theory reasoner for the combination of theories supported by the SMT solver. The propositional structure of the problem is handled by the SAT solver, whereas the theory reasoner only has to deal with conjunctions of literals. Very schematically (we refer to [START_REF] Barrett | Satisfiability modulo theories[END_REF] for more details) the Boolean abstraction of the SMT problem is repeatedly refined by adding theory conflict clauses that eliminate spurious models of the abstraction, until either unsatisfiability is reached, or a model of the SMT formula is found. Refinements can be done by refuting models of the propositional abstraction one at a time. It is, however, much more productive to refute all propositional models that are spurious for the same reason at once. A model of the abstraction is spurious if the set of concrete literals corresponding to the abstracted literals satisfied by this model is unsatisfiable modulo the theory. Given such an unsatisfiable set of concrete literals, the disjunction of the negations of any unsatisfiable subset (a.k.a. core) is a suitable conflict clause. By backtracking and asserting the conflict clause, the SATsolver is prevented from generating the spurious model again. The smaller the clause, the stronger it is and the more spurious models it prevents. Therefore, an optimal conflict clause, corresponding to a minimal unsatisfiable subset of literals (i.e. such that all its proper subsets are satisfiable) or even a minimum one (i.e. smallest among the minimals) is desirable. This feature of the theory reasoners to generate small conflict sets (a name adopted in [START_REF] Barrett | Satisfiability modulo theories[END_REF]) from their input is also referred to as proof production [START_REF] Nieuwenhuis | Union-find and congruence closure algorithms that produce proofs[END_REF][START_REF] Nieuwenhuis | Proof-producing congruence closure[END_REF] or explanation generation [START_REF] Nieuwenhuis | Fast congruence closure and extensions[END_REF].

Decision procedures for the theory of uninterpreted symbols and equality can be based on congruence closure [START_REF] Nelson | Fast decision procedures based on congruence closure[END_REF][START_REF] Peter | Variations on the common subexpressions problem[END_REF][START_REF] Nieuwenhuis | Fast congruence closure and extensions[END_REF]. The decision problem is polynomial and even quasi-linear [START_REF] Peter | Variations on the common subexpressions problem[END_REF] with respect to the number of terms and literals in the input set. Producing minimal conflict sets also takes polynomial time. Indeed, testing if a set S remains unsatisfiable after removal of one of its literals is also polynomial. It suffices then to repeatedly test the |S| literals of S to check if they can be removed. The set S pruned of its unnecessary literals is minimal. One could also profit from the incrementality of the decision procedure [START_REF] Fontaine | Using BDDs with combinations of theories[END_REF].

It has also been common knowledge that computing minimum conflict clauses for the theory of uninterpreted symbols and equality is a difficult problem. But, to our best knowledge, the complexity of finding the smallest conflict clause generation for sets of literals with uninterpreted symbols and equalities has never been established. The complexity of the corresponding decision problem (i.e. of whether there exists a conflict clause with size smaller than a given k) is mentioned to be NP-complete in [START_REF] Nieuwenhuis | Fast congruence closure and extensions[END_REF] -with a reference to a private communication with Ashish Tiwari -but neither the authors of [START_REF] Nieuwenhuis | Fast congruence closure and extensions[END_REF] nor Ashish Tiwari published a written proof of this fact1 .

Our interest in this problem arose from our work on Skeptik [START_REF] Boudou | Skeptik: A proof compression system[END_REF], a tool for the compression of proofs generated by SAT and SMT solvers. For the sake of moving beyond the purely propositional level, we have developed an algorithm for compressing congruence closure proofs, which consists of regenerating (possibly smaller) congruence closure conflict clauses while traversing the proof. Congruence closure conflict clauses are typically generated from paths in the congruence graph maintained by the congruence closure algorithm [START_REF] Fontaine | Techniques for verification of concurrent systems with invariants[END_REF][START_REF] Nieuwenhuis | Fast congruence closure and extensions[END_REF][START_REF] Nieuwenhuis | Proof-producing congruence closure[END_REF]. In order to obtain small conflict clauses, and thereby small congruence clo-sure proofs, we (dynamically) assigned weights to the congruence graph and searched for shortest paths in that graph. The weights of input equations would be 1, whereas the weight of a congruence edge would be the size of an explanation of its equation. This raised the question whether we could construct shortest conflict clauses as shortest paths in such weighted congruence graphs, by applying a polynomial time shortest path algorithm to a graph of polynomial size. We answered this question negatively by proving that the problem of deciding whether a shorter conflict clause exists is NP-hard. The goal of this article is to present this proof. The reason why the shortest path method is not able to find shortest conflict clauses is that the weights for congruence edges can not be accurately determined a priori. A preliminary version was presented at the SMT Workshop 2015 [START_REF] Fellner | NPcompleteness of small conflict set generation for congruence closure[END_REF].

Preliminaries

We assume knowledge of propositional logic and quantifier-free first-order logic with equality and uninterpreted symbols, and only enumerate the notions and notations used in this article. A literal is either a propositional variable or the negation of a propositional variable. A clause is a disjunctive set of literals. A propositional variable x appears positively (negatively) in a clause C if x ∈ C (resp. ¬x ∈ C). The notations { 1 , . . . n } and 1 ∨ • • • ∨ n will be used interchangeably. A clause is tautological if and only if it contains a variable both positively and negatively. We shall tacitly assume that clauses are non-tautological, except when explicitly stated otherwise. Clauses being sets, they cannot contain multiple occurrences of the same literal. A formula in conjunctive normal form (CNF for short) is a conjunctive set of clauses. A total (partial) assignment I for a formula in propositional logic assigns a value in { , ⊥} to each (resp. some) propositional variable(s) in the formula. An assignment I for a formula F is a model of F , denoted I |= F , if it makes the formula F true. A formula is satisfiable if it has a model, it is unsatisfiable otherwise. A total or partial assignment is perfectly defined by the set of literals it makes true. By default, an assignment is total unless explicitly said to be partial. A set of formulas E entails a (set of) formula(s) E , denoted

E |= E , if every model of E is a model of E .
We now define the necessary notions for quantifier-free first-order logic. An assignment I on some signature maps each constant to an element in a universe U, and each function symbol to a function of appropriate arity on U. By extension, it assigns an element in U to every term, and a value to every equation s = t, namely if I(s) = I(t) and ⊥ otherwise. Like in propositional logic, an assignment on some signature thus gives a truth value to every formula on this signature.

Definition 2 (Congruence relation) Given a set of terms

T closed under the subterm relation, a relation R ⊆ T × T is a congruence if it is -reflexive: (t, t) ∈ R for each t ∈ T ; -symmetric: (s, t) ∈ R if (t, s) ∈ R; -transitive: (r, t) ∈ R if (r, s) ∈ R and (s, t) ∈ R; -compatible: (g(t 1 , . . . , t n ), g(s 1 , . . . , s n )) ∈ R if g is a n-ary function symbol and (t i , s i ) ∈ R for all i = 1, . . . , n.
A congruence relation is also an equivalence relation, since it is reflexive, transitive and symmetric. Therefore a congruence relation partitions its underlying set of terms T into congruence classes, such that two terms (s, t) belong to the same class if and only if (s, t) ∈ R. The relations {(t, t) : t ∈ T } and T × T are trivial congruence relations. An assignment I on a signature Σ defines a congruence relation on any subset

T ⊆ T Σ , that is, R = {(s, t) | I(s = t) = }.
An equation s = t on terms in a set T can be seen as a singleton relation {(s, t)} ⊆ T ×T . By extension, a set of equations can also be seen as a relation, i.e., the union of the singleton relations. Since congruence relations are closed under intersection, the congruence closure of a set of equations always exists. Also notice that, if (s, t) ∈ E * , then E |= s = t. We say that E is an explanation for s = t.

An algorithm computing the congruence closure of a relation is also a decision procedure for the problem of satisfiability of sets of equalities and disequalities in quantifier-free first-order logic with uninterpreted (predicates and) functions. It suffices indeed to compute the congruence closure of all equalities on the terms and subterms occurring in the literals. Then, the set of literals is satisfiable if and only if there is no disequality with both terms in the same class. A model can be built from the congruence closure, on a universe with cardinality equal to the number of classes in the congruence.

Congruence Closure in Practice

The algorithms we consider in the following take as input a set of literals E. Considering complexity, not only the cardinality of the set is important, but also the number of terms and subterms as well as the number of their occurrences. Congruence closure algorithms in modern SMT solvers typically represent terms with Directed Acyclic Graphs (DAGs) using maximal sharing, and not trees. The number of term and subterm occurrences does not matter, but only the number of distinct (sub)terms. The input is also typically not a set, but successive calls to an assertion function with a literal as argument: every repetition of the same literal then matters for complexity. Let us assume, however, that the input is a set E, terms are DAGs with maximal sharing (i.e. identity of atomic symbols and complex terms can be checked in constant time). Therefore, we characterize complexity results in terms of number of literals, terms and subterms of the input set, i.e. |E| and |T (E)|.

Since congruence relations are basically partitions of equivalent terms that additionally satisfy the compatibility property, it is unsurprising that practical congruence closure algorithms, or decision procedures for ground sets of firstorder logic literals, are based on some kind of union-find data-structure. Terms (and subterms) are put into equivalence classes, according to the equalities in the input. The algorithms furthermore check, every time two classes of the partition are merged, whether any new equality induced by compatibility has to be taken into account. Also, it checks that the congruence is consistent with the set of disequalities. We refer the reader to [START_REF] Nelson | Fast decision procedures based on congruence closure[END_REF][START_REF] Peter | Variations on the common subexpressions problem[END_REF][START_REF] Nieuwenhuis | Fast congruence closure and extensions[END_REF] for more details. The complexity of those algorithms depend on the internal data-structures and on the representation of terms [START_REF] Peter | Variations on the common subexpressions problem[END_REF]. Algorithms typically implemented in SMT solvers have complexity

O(|E| + (|T (E)| • log |T (E)|)
) assuming constant time operations on the hash table being used to detect new equalities induced by compatibility.

The generation of conflict sets or explanations is based on the congruence graph: its nodes are the terms and subterms considered by the algorithm. An edge in the graph is either a full edge, linking two nodes s and t and labeled by an input equation s = t, or a congruence edge (a dotted edge in the figures in this article), linking two terms with the same leading function symbol and labeled by the compatibility-deduced equality between both terms. The graph has a path between two terms if and only if they belong to the same congruence class. The equality between two terms in the same class is a logical consequence of the set of equations labeling the path. To get an explanation for the equality of two terms in the same class, that is, a set of input equations implying the equality of the two terms, it thus suffices to collect the set of equations labeling a path, and recursively replace any compatibility equation

g(t 1 , . . . , t n ) = g(s 1 , . . . , s n ) by the explanations of t 1 = s 1 ,. . . , t n = s n . Example 1 A congruence graph for two input equations a = f (f (f (a))) and a = f (f (f (f (f (a))))
) is given on Figure 1. Labeling equations are omitted for simplicity. There is a path between a and f (a), so both terms are equal if the a f (a)

f (f (a)) f (f (f (a))) f (f (f (f (a)))) f (f (f (f (f (a)))))
Fig. 1 An example congruence graph input equations hold. To compute an explanation for a = f (a), it suffices to collect the equalities on the path, that is, the input equation a = f (f (f (a)))) and the compatibility equation f (a) = f (f (f (a))). This last equation should then be replaced by the equation between the arguments, i.e., a = f (f (a))) which is consequence, by transitivity, of another compatibility equation and of the other input equation a = f (f (f (f (f (a))))). Hence the explanation will contain both equations.

Practical congruence closure algorithms with explanation build a congruence graph while computing the congruence closure. Every time the decision procedure merges two classes, either because of an input equation or because an equality was deduced due to compatibility, a full-or congruence-edge is added to the graph. Since edges between nodes are only added when their respective congruence classes are merged, the path between two terms in the same class is unique. The explanation that two terms are equal is also unique, but there is no guarantee that this explanation is the smallest one. Indeed, it may happen that the algorithm considers, e.g. equations a = b and b = c before a = c, merging a, b and c before considering the last equation, and thus discarding a = c as redundant: in that case, a = c would have been the smallest proof that a and c are equal, but the congruence graph would only consider the two other equalities. There is not even a guarantee that the explanation is minimal. Again, the congruence closure algorithm can prove that a = f (b) from the input equations b = f (a), f (a) = f (b) and a = b. The redundant equality f (a) = f (b) would be recorded in the congruence graph, and thus be part of the explanation, if it is considered before a = b.

In practice, the congruence closure procedures implemented in SMT solvers produce explanations efficiently: the complexity of the explanation production is quasi-linear with respect to the explanation size, which is at most equal to the size of the input [START_REF] Nieuwenhuis | Fast congruence closure and extensions[END_REF]. But the explanations are not optimal, i.e. they are not always the smallest. In fact, they are not even minimal. It is possible to compute minimal explanations in polynomial time; it suffices for instance to compute again the congruence closure iteratively removing every equation in the explanation, to see if it is redundant or not. One could (naively) hope to conceive a different congruence closure algorithm generating the smallest explanation in polynomial time. For example, one might attempt to modify the iterative removal algorithm; or attempt to modify shortest path algorithms and apply them to congruence graphs enriched with redundant equations as labels. However, such attempts would be futile. As proven in the next section, the corresponding decision problem is NP-hard.

NP-Completeness of the Small Conflict Set Problem

The function problem of generating the smallest conflict set corresponds to the decision problem of deciding whether a conflict set with size smaller than a given k exists.

Definition 4 (Small conflict set problem) Given an unsatisfiable set E of literals in quantifier-free first-order logic with equality and k ∈ N, the small conflict set generation problem is the problem of deciding whether there exists an unsatisfiable set E ⊆ E with |E | ≤ k.

If we had a polynomial-time algorithm α capable of generating the smallest conflict set for any unsatisfiable set E, then we could decide in polynomial time any instance of the small conflict set problem by applying α to E and checking whether α(E) has size smaller than k. However, as proven below, the small conflict set problem is NP-complete and, therefore, polynomial time generation of conflict sets with minimum size is not possible (unless P = NP). Our proof reduces the problem of deciding the satisfiability of a propositional logic formula in conjunctive normal form (SAT) to the small explanation problem. Definition 5 (Small explanation problem) Given a set of equations E = {s 1 = t 1 , . . . s n = t n }, k ∈ N and a target equation s = t, the small explanation problem is the problem of answering whether there exists a set E such that E ⊆ E, E |= s = t and |E | ≤ k.

The small explanation problem and the small conflict set problem are closely related: there is a small explanation of size k of s = t from E if and only if there is a small conflict of size k + 1 for E ∪ {s = t}.

In the following we describe a polynomial translation from instances of the propositional satisfiability problem to instances of the small explanation problem. The translation consists of two parts: a translation of propositional formulas, here assumed, without loss of generality, to be in CNF (as shown in Definition 6), and a translation of assignments (as shown in Definition 7).

Definition 6 (CNF congruence translation)

Let C be a set of propositional clauses {C 1 , . . . C n } using variables x 1 , . . . , x m . The congruence translation E C of C is defined as the set of equations

E C = Connect ∪ 1≤i≤n Clause i with Connect = {c i = c i+1 | 1 ≤ i < n} Clause i = {c i = t i (x j ) | x j appears in C i } ∪ {t i ( j ) = c i | x j appears positively in C i } ∪ {t i (⊥ j ) = c i | x j appears negatively in C i }
where c 1 , . . . c n , c 1 , . . . c n , x1 , . . . xm , 1 , . . . m , ⊥ 1 , . . . ⊥ m are distinct constants, and t 1 , . . . t n are distinct unary functions. 2Remark 1 Note that the constants i and ⊥ i (for 1 ≤ i ≤ m)) should not be confused with the Boolean values and ⊥. The intuitive relationship between these constants and the boolean values is established in Definition 7.

The translation of clauses is illustrated by the following example.

Example 2 Consider the set of clauses C

C 1 = x 1 ∨ x 2 ∨ ¬x 3 , C 2 = ¬x 2 ∨ x 3 , C 3 = ¬x 1 ∨ ¬x 2 .
Figure 2 represents the congruence translation of C graphically, an edge between two nodes meaning that the set contains an equation between the terms labeling the two nodes.

c1 t1(x2) t1(x1) t1(x3) c 1 t1( 2)
t1( 1)

t1(⊥3) c2 t2(x2) t2(x3) c 2 t2(⊥2) t2( 3) c3 t3(x1) t3(x2) c 3 t3(⊥1) t3(⊥2)

Definition 7 (Assignment congruence translation)

The assignment congruence translation E I of an assignment I on propositional variables x 1 , . . . , x m is the set of equations

E I = {x j = j | 1 ≤ j ≤ m and I |= x j } ∪ {x j = ⊥ j | 1 ≤ j ≤ m and I |= ¬x j }
For convenience, we also define the set

AssignmentEqs = {x j = j , xj = ⊥ j | 1 ≤ j ≤ m}.
An assignment congruence translation is always a subset of AssignmentEqs. By extension, a subset of AssignmentEqs is said to be an assignment if it is the congruence translation of an assignment, that is, if it does not contain both xj = j and xj = ⊥ j for some j.

E I ∪ E C |= c 1 = c n .
Proof. Let the propositional variables in C be x 1 , . . . , x m .

(⇐) Consider the congruence graph induced by E I ∪ E C . Besides edges directly associated to equalities in the set, the only edges are congruence edges between terms t i (x j ) and either t i ( j ) or t i (⊥ j ). So any path from c 1 to c n would go through such a congruence edge for each i. And such an edge exists for i if and only if the clause i is satisfied by I.

(⇒) If I |= C, then I |= C i for each clause C i ∈ C. Assume I makes true a variable x j , literal of C i (the case of the negation of a variable is handled similarly). Then E I |= t i (x j ) = t i ( j ), and E I ∪ Clause i |= c i = c i . This is true for each i, and thanks to the equations in Connect, one can deduce using transitivity that

E I ∪ E C |= c 1 = c n .

Lemma 2 Consider a (partial or total) assignment I for non-tautological clauses

C = {C 1 , . . . C n } on variables x 1 , . . . , x m . |E I ∪ E C | and |T (E I ∪ E C )| are polynomial in n and m.
Proof. E I contains at most m equations, since for no j both I |= x j and I |= ¬x j . The set Connect contains exactly n -1 equations. For every i, the set Clause i contains at most 2m equations, resulting in 2mn equations for all clauses. In total, we thus have

|E I ∪ E C | ≤ n -1 + m + 2mn.
E I ∪ E C contains at most 2n + 3m + 3mn terms: 2n for c i , c i , 3m for xj , j , ⊥ j and 3mn for all possible combinations of t i (x j ), t i ( j ), t i (⊥ j ).

Considering again Example 3, and particularly Figure 5, any transitivity chain from c 1 to c 3 will pass through c 1 , c 2 , c 2 and c 3 . Any acyclic path from c 1 to c 3 will contain 11 edges: 3 congruence edges, 3 * 2 edges in Clause i for i = 1, 2, 3 and 2 edges from Connect.

Since every interpretation I is such that E I ⊂ AssignmentEqs, one can try to relate the propositional satisfiability problem for a set of clauses C = {C 1 , . . . C n } to finding an explanation of c 1 = c n in AssignmentEqs ∪ E C . However, it is necessary that this explanation does not set xj equal both to j and ⊥ j , i.e. at most one of the two equations xj = j and xj = ⊥ j should be in the explanation. By restricting assignments to total ones, i.e. by enforcing that at least one of the two equations xj = j and xj = ⊥ j belongs to the explanation, it is also possible, with a single cardinality condition on the explanation size, to require that at most one of them belong to the explanation.

Lemma 3 A set of non-tautological clauses

C = {C 1 , . . . C n } using vari- ables x 1 , . . . , x m is satisfiable if and only if there is a set E such that E ⊆ AssignmentEqs ∪ E C , E |= c 1 = c n+m and |E | ≤ 3n + 4m -1, where C is C augmented with the tautological clauses C n+i = x i ∨ ¬x i for i = 1, . . . m.
Proof. (⇒) Consider a total model I for C. We show that there is a set E ⊂ E C , such that together with the congruence translation

E I of I it follows E = E ∪ E I |= c 1 = c n+m and |E | ≤ 3n + 4m -1.
The set E I contains m equations, since it is the congruence translation of a total assignment.

For each clause C i (i = 1 . . . n + m), there is a literal in C i that is satisfied by the model I. Let x j be the variable of that literal.

Suppose I |= x j , then the set E contains equations c i = t i (x j ), t i ( j ) = c i of Clause i . These equations are in Clause i , because x j is the satisfying literal of C i , thus surely x j ∈ C i . From compatibility and the fact that xj = j ∈ E I it follows that E ∪ E I |= t i (x j ) = t i ( j ). Finally, from transitivity and the three equations

c i = t i (x j ), t i (x j ) = t i ( j ), t i ( j ) = c i it follows that E ∪ E I |= c i = c i .
The case I |= x j is symmetric, such that via equations

c i = t i (x j ), t i (x j ) = t i (⊥ j ), t i (⊥ j ) = c i , it follows E ∪ E I |= c i = c i .
In addition to 2 equations for each of the (n + m) clauses, the set E contains all n + m -1 equations of Connect, that is

c i = c i+1 for i = 1 . . . n + m -1. From transitivity it follows that E ∪ E I |= c 1 = c n+m .
In total, E contains 2(n + m) of the sets Clause i , n + m -1 equations from Connect and m equations from E I , i.e. |E| = 3n + 4m -1.

(⇐) Suppose there is a set of equations E ⊆ AssignmentEqs ∪ E C such that E |= c 1 = c n+m and |E | ≤ 3n + 4m -1. E has to contain 2(n + m) equations from Clause i (i = 1 . . . n+m), that is one pair of equations c i = t i (.) and t i (.) = c i for every clause, and n + m -1 equations from Connect, since by construction there is no other possibility to deduce c i = c i . Furthermore, thanks to the tautological clauses, E also has to contain at least xj = j or xj = ⊥ j for each j ∈ {1 . . . m}. Therefore, the cardinality condition |E | ≤ 3n+4m-1 and the fact that E contains 3(n + m)-1 equations from Clause i and Connect, requires that the E contains at most one xj = j or xj = ⊥ j for each j ∈ {1 . . . m}. Therefore, we have that E I = E ∩ AssignmentEqs is the congruence translation of an assignment and Lemma 1 guarantees the existence of a model for C , or equivalently for the original set of clauses C.

Example 4

In Lemma 3, the input formula is augmented with tautological clauses. We demonstrate here the necessity of these extra clauses on the unsatisfiable formula ϕ

= (x 1 ∨ x 2 ) ∧ (¬x 1 ∨ x 2 ) ∧ (x 1 ∨ ¬x 2 ) ∧ (¬x 1 ∨ ¬x 2 ).
Figure 6 shows the congruence translation of ϕ together with a subset of AssignmentEqs that yields an explanation for c 1 = c 4 . This explanation picks, besides the necessary equations from the clause and connect parts, two equations from the AssignmentEqs part. However, this explanation maps x 1 to ⊥ and at the same time, and hence cannot correspond to a (consistent) assignment. With the addition of tautological clauses and because the number of equations in the explanation is upper bounded, spurious explanations of this kind are ruled out. This is illustrated in Figure 7, depicting the congruence translation of ϕ conjoined with the tautological clauses (x 1 ∨ ¬x 1 ) and (x 2 ∨ ¬x 2 ), together with the same subset of AssignmentEqs used in Figure 6. As desired, this subset is not an explanation of c 1 = c 6 , since the transitivity chain stops at t 6 (x 2 ), x 2 being unassigned. In fact, in this congruence graph, there is no explanation of c 1 = c 6 with less than 19 equations. This is as expected, since ϕ is unsatisfiable and 3n + 4m -1 = 19 in our example with n = 4 clauses and m = 2 variables.

c1 t1(x2) t1(x1) c 1 t1( 2) t1( 1) c2 t2(x2) t2(x1) c 2 t2( 2) t2(⊥1) c3 t3(x2) t3(x1) c 3 t3(⊥2) t3( 1) c4 t4(x2) t4(x1) c 4 t4(⊥2) t4(⊥1) x1 1 ⊥1
Fig. 6 The congruence translation of ϕ and a spurious short explanation.

c1 t1(x2) t1(x1) c 1 t1( 2) t1( 1) c2 t2(x2) t2(x1) c 2 t2( 2) t2(⊥1) c3 t3(x2) t3(x1) c 3 t3(⊥2) t3( 1) c4 t4(x2) t4(x1) c 4 t4(⊥2) t4(⊥1) c5 t5(x1) c 5 t5(⊥1) t5( 1) c6 t6(x2) c 6 t6(⊥2) t6( 2) x1 1 ⊥1
Fig. 7 The congruence translation of ϕ with tautological clauses.

Corollary 1 (NP-hardness)

The small explanation problem is NP-hard.

Proof. Propositional satisfiability is NP-hard, and can be reduced in polynomial time to the small explanation problem.

Lemma 4 (NP)

The small explanation problem is in NP.

Proof. Let E be a set of equations and s = t be a target equation. A solution to the explanation problem for some k ∈ N is a subset E ⊆ E, such that |E | ≤ k. Let n = |T (E)| + |E| and n = |T (E )| + |E |. We have n ≤ n, since E ⊆ E and every term in E appears also in E. Checking whether E is an explanation of s = t can be done by computing its congruence closure, which is possible in polynomial time in n [START_REF] Nelson | Fast decision procedures based on congruence closure[END_REF] and thereby also in n.

Theorem 1 (Small explanation NP-completeness) The small explanation problem is NP-complete.

Proof. By corollary 1 and lemma 4.

Theorem 2 (Small conflict NP-completeness)

The small conflict set problem is NP-complete.

Proof. The small conflict set problem is at least as hard as the small explanation problem since the small explanation problem has been showed to be reducible to the small conflict set problem. It is also in NP for exactly the same reason that the small explanation problem is.

Conclusion

The conflict set generation feature of congruence algorithms is essential for practical SMT solving. Although one could argue that the important property of the generated conflicts is minimality (i.e. no useless literal is in the conflict), it is also interesting to consider producing the smallest conflict. We have shown that the problem of deciding whether a conflict of a given size exists is NPcomplete. Therefore, it is generally intractable to obtain the smallest conflict.

In [START_REF] Fontaine | Using BDDs with combinations of theories[END_REF][START_REF] Nieuwenhuis | Union-find and congruence closure algorithms that produce proofs[END_REF][START_REF] Nieuwenhuis | Proof-producing congruence closure[END_REF], methods to obtain small conflicts, but not necessarily the smallest, are discussed. In practice, it pays off to prioritize speed of the congruence closure algorithm and conflict generation over succinctness of conflicts. However, other applications sensitive to proof size may benefit from other methods prioritizing small conflict size, at a cost of less efficient solving. Thanks to the NP-completeness, one option could be to iteratively encode the small conflict problem into SAT, and use a SAT-solver to find successively smaller conflicts, until the smallest is found. Perhaps an encoding of the problem can be found that differentiates between hard constraints representing relevant instantiations of the axioms of equality as well as the target equation, and soft constraints representing the inclusion of input equations to an explanation. In that case, Max-SAT solvers could be used to find small explanations, in order to leverage efforts that combine decision procedures and optimization techniques.

Definition 3 (

 3 Congruence closure) The congruence closure E * of a set of equations E on a set of terms T closed under the subterm relation is the smallest congruence relation on T containing E.

Fig. 2

 2 Fig. 2 The congruence translation E C = Connect ∪ 1≤i≤n Clause i of C.

Example 3 (

 3 Example 2 continued) Consider the model I = {x 1 , ¬x 2 , x 3 } of C. Figure 3 gives a graphical representation of E I , whereas AssignmentEqs is represented in Figure 4. Notice that E C ∪ E I |= c 1 = c 3 , and c 1 and c 3 are connected in the congruence graph of E C ∪ E I (Figure5), the path containing both full edges corresponding to equalities in E C ∪ E I , and dotted edged corresponding to equalities due to the compatibility property of the congruence relation.

3 Fig. 3 3 Fig. 5 Lemma 1

 33351 Fig. 3 Congruence translation of I

Definition 1 (Terms and equations) A signature

  Σ is a finite set of function symbols F equipped with an arity function F → N. A constant is a nullary function. A unary function has arity one. Given a signature Σ, the set of terms T Σ is the smallest set containing all constants in F and all terms of the form g(t 1 , . . . , t n ), where g is a function symbol of arity n in F and t 1 , . . . , t n are terms in T Σ . An equation between two terms s, t in T Σ is denoted by s = t. Boolean combination of equalities between terms; a literal is either an equation or the negation of an equation.The terms t 1 , . . . , t n are direct subterms of g(t 1 , . . . , t n ). The subterm relation is the reflexive and transitive closure of the direct subterm relation. Given a set of equations E, we denote by T (E) the set of terms and subterms occurring in the equations.

	formula is here just a
	Signatures commonly include predicate symbols. Everything extends smoothly
	to signatures with predicates, but to simplify, a quantifier-free first-order logic

We contacted both Ashish Tiwari and the authors of[START_REF] Nieuwenhuis | Fast congruence closure and extensions[END_REF], who confirmed this.

It would be possible to define a translation without the c i constants, but they ease the presentation.

Acknowledgment. We would like to thank Robert Nieuwenhuis and Ashish Tiwari for discussions and some preliminary ideas that led us to this proof. We are grateful to the anonymous reviewers of this paper and of [4] for their comments.

This work has been partially supported by the project ANR-13-IS02-0001 of the Agence Nationale de la Recherche, by the H2020-FETOPEN-2016-2017-CSA project SC 2 (712689), by an ÖAW APART Stipendium, by FWF W1255-N23, by ERC Start Grants Graph Games (279307) and Matryoshka (713999), and by FFG project number 845582 (TRUCONF).


Napaporn Reeveerakul

Ridha Derrouiche

Nopasit Chakpitak

Yacine Ouzrout

Napat Harnpornchai

Abdelaziz Bouras

MONTREAL -CANADA

Keywords: Supply chain management, Foreign Direct Investment, Relocation plant, Knowledge management, Multi-Agent System

The low economic growth and competition among neighbouring countries has caused Foreign Direct Investments (FDIs) to relocate their businesses. In order to prevent further business relocation, this paper proposes an integrated framework based on the supply chain to help analyse decision making for plant situations and enhance manufacturing performance. The context of this perspective is applied to manufacturers located in the industrial estate region of Lumphun province, Thailand. Data collection and review of literature was used to identify the factors that influence industrial investment. The SCOR model was used to define the parameters, which were then used in Arena simulation. The simulation needs to describe factors affected on industrial performance. From this result, an integrated analysis model was built and the importance of supply chain collaboration was identified. A Multi Agent System (MAS) was suggested to enhance of the effective interaction between supply chain' agents. It is in order to mitigate risks among them.

Introduction

Thailand is classified as a developing country. The majority of Thai people work in the agriculture sector but their sectors have accrued faster to more closely link to the international economy, for example; jobs in manufacturing for export or labouring jobs in companies. Those who remained in the domestic economy, such as small scale farmers, generally received fewer benefits, proportionately [START_REF]Socio-economic Situation[END_REF]. In electronics manufacturing, high technology and cost investment, skill requirement, continuous research and development, and intensive labour are needed. Most electronics manufacturers depends on Foreign Direct Invesments (FDIs) with both funding and high technology. At the same time, FDIs are interested in investment in developing countries in order to get the benefits of low labour costs.

Particularly, Lumphun province is the location of a large industrial estate in the northern part of Thailand. Earnings from industrial labor is a key factor driving the province's growth. Sixty-three factories are located in this area, most manufacturing products of which 31.16% are manufacturing electronics. 43,456 persons work in Lumphun province [2], while the workforce in the electronics factories in the Lumphun estate represents 83.33% of the manufacturing workforce in this province [START_REF][END_REF]. However, it has been noted that plant closures have increased to 4.76% during the period 2005 to 2007 [2]. Low local economic growth and competition with neighbouring countries are the main reasons, leading to business relocation to countries with cheaper labour cost. These unwelcome circumstances lead to economic problems in the province, affecting income and finally leading to social problems.

In this context, we are proposing here an analysis of manufacturers' decisions on plant situations. In order to prevent relocation of plants, the model studies three perspectives: finance, supply chain and knowledge skill within companies. However, the main perspective discussed here is the supply chain analysis.

In the next section we summarize the review of literature about the factors influenced decision on plant situation.

In section 3, we introduce a new framework on making a decision on plant situation. The framework helps manufacturer to analyse and make a decision on plant's situation, based on a three perspectives with Finance, Supply chain and Human skill. As an illustration, we apply this framework to case study with supply chain simulation technique in section 4, and we show how this supply chain collaboration important for manufacturers. Finally, we introduce in the section 5, a Multi Agent System (MAS) needs to enhance of the effective interaction between supply chain' agents through an agent communication language.

Context and previous works

Recent studies have proposed some directions to improve the decision making in Supply Chain.

Context of this work: Supply Chain Collaboration

Supply chain collaboration is often defined as two or more enterprises working together to create a competitive advantage and higher profits that cannot be achieved by acting alone [START_REF] Togar | An Integrative Framework for Supply Chain Collaboration[END_REF]. Supply Chain Council, [5] proposes a structure of a supply chain around five distinct management processes as shown in Figure 1. The advent of supply chain collaboration creates the need, at intra-enterprise level (between the different plants and the different processes) and at inter-enterprises level (between the different partners) to pay special attention to the understanding of collaboration in order to prepare the partners to create collaborative efforts successfully [START_REF] Derrouiche | A Dashboard to Analyze Relations in Enterprise Networks[END_REF]. Supply chain collaboration implies that all factors relevant need to be taken into account to produce a good decision.

Review of literature: Factors influencing decisions on plant situation

Chan et al., [START_REF] Chan | Stock Market Reaction to Capital Investment Decisions: Evidence from Business Relocation[END_REF] found that the main reasons for business relocations were cost savings and business expansion, regardless of whether the firm was a plant or a headquarters. Other literature from Qi Chun, Jhon C.S. Tang, [START_REF] Qi Chun | Foreign Direct Investment in Chinese Industries: A Genetics Algorithm Approach[END_REF] proposed a genetic algorithm (GA) as an analytical tool to define fitness function as a variable selection algorithm and analysis of inward Foreign Direct Investment (FDI). They found 24 independent variables that affect FDI in China which the most often selected determinants of FDI flows into industry are productivity, research and development investment, labour investment and educational level. So far as investment in manufacturing is concerned profit which is a key factor for the investor. Minimizing costs while maximizing revenue is undertaken to maximize profit. For financial measurement, net present value (NPV) is one wellknown strategy that ascertains the time value of money invested in a business. Generally, the approach used for optimize decision making. A number of production planning studies have subsequently been evolved with the aim of maximizing the NPV [START_REF] Kersten | An Empirical Approach to Supply Chain Risk Management: Development of a Strategic Framework[END_REF].

In recent years, many companies have observed that beside their "traditional" risks arising from their business activities, new risks emerge from sources that are often related to the close collaboration within their supply chain networks [START_REF] Kersten | An Empirical Approach to Supply Chain Risk Management: Development of a Strategic Framework[END_REF]. Supply-Chain Council (SCC) Risk Management Team & Douglas Kent (December,2007), [START_REF]Supply Chain Risk Measurement[END_REF], argued that today's organizations recognize that "preservation of shareholder value" is highly important in supply chain management. So disruption in the supply chain will impact on the company's overall performance.

Indeed, several authors developed this question under various points of view such as: to make a decision on plant relocation from Europe to China, incorporate management participation method was used by considering return on profitability and soft variables, example of: loyalty skill and local performance [START_REF] Vos | Capturing the Dynamics of Facility Allocation[END_REF]. Besides, N.Viswanadham and Kannan Balaji [START_REF] Viswanadham | Foreign Direct Investment on Outsourcing: A Supply Chain Decision Model[END_REF] proposed quantitative model for optimal decision between FDI and outsourcing with multi-stages. At various stages of supply chain risk due to supply chain, inventory and transportation cost. To investigate the fact of technology transfer by FDI in electronics sector in South Africa, the researchers criticized the need to be integrated from start to acquire capabilities focused on developing knowledge based, security and subcontract existence [START_REF] Mzanda | The Ambivalence of technology transfer through Foreign Direct Investments[END_REF]. The table 1 synthesizes and classifies the various studies according to the attributes used. From a review of literature, it is clear that there are many factors affecting plant relocation. Most researchers are more focused on cost of production, supply chain between supplier and customer, for instance, market demand and supplier lead time or even supply chain risk. However, the consideration on external factors as economic development policy cannot be neglected.

Da

A framework of decision making and prevention of plant relocation: Supply Chain context

According to the previous analysis, a framework for making decisions on plant situations was introduced. The framework helps the manufacturer to analyse and make a decision on a plant's situation. Figure .3 shows the framework explanation based on three perspectives. Fig. 3. The Framework decision on plant situation and system performance improvement On supply chain management, in order to improve manufacturing performance, it is very necessary for firms to enhance effectiveness on collaboration, the integration of supply chain, mitigate risk and, provide more benefits to achieve customer satisfaction. Moreover, manufactures can keep and extend their operational life. To avoid human failure, skill and performance improvements are needed to develop manufacturing systems. Knowledge sharing among knowledge workers and asset transferring are useful approaches to eventually extend a factory's operation. Besides, according to investment in manufacturing, the consideration on financial aspect is implemented by s-curve analysis. The maximum expectation on return on investment is an objective function for investors.

Focussing on the three perspectives, the investor is interested in maximum return on investment (ROI). Factory objective is to mitigate supply chain risks. Meanwhile, enhanced skill and worker performance helps to reduce human error in the working area. Figure .3 describes the explanation of the objective to be successful and the strategic decision on plant situation and system performance improvement. As shown in the framework, to prevent unwelcome situations, alternative strategies on supply chain management by enhancing system performance and their collaboration are adopted. So this paper aims at supply chain perspective. Nowadays, companies face many critical challenges with regards to supply chain management. One of the main challenges arises out of trends associated with lean management. Strongly synchronized interfaces and the reduction of inventory cause a greater dependence on the supply chain partners. Close co-operation between supply chain partners exacerbates the risk exposure of companies in a supply chain [START_REF] Kersten | An Empirical Approach to Supply Chain Risk Management: Development of a Strategic Framework[END_REF]. To improve manufacturing industry, the integration of supply chain and risk analysis is necessary. Besides, supply chain analysis is used to identify the impact of changes in the location and/or capacity of facilities on supply, manufacturing and distribution activities. This impact can be measured by determining the required input quantities (materials, labour, capital and energy) and the respective unit prices for alternative locations and capacity level. In addition, factors in the international environment like taxes, barriers to trade and exchange rate, will affect allocation strategies [START_REF] Vos | Capturing the Dynamics of Facility Allocation[END_REF].

As mentioned above, most arguments are explained in qualitative aspects. Then the practical data is used for an implementation in quantitative aspect. The application on simulation model based on SCOR (Supply Chain Operations Reference) model analysis was used.

Therefore model with SCOR on level 1 related to scope of processes (Plan, Source, Make, Delivery and Return) and processes categories, process element information inputs, outputs and activities which defines the ability to compete operations strategy. To describe unambiguously and communicate the process, a framework of relationships among the standard processes in supply chain was explained with the SCOR-model. The SCORmodel captures the Supply Chain Council's consensus view of supply chain management. While much of the underlying content of the model has been used by the practitioner for many years, the SCOR-model provides a unique framework that links business process, metrics, best practices and technology features into an effective supply chain management and related supply chain improvement activities [5]. SCOR-Model used for performance attributes on supply chain simulation as shown in Table 2. A commonplace situation in manufacturing is one supply source providing material to manufacturer, one distributor receiving finished goods and requesting order. Goods are made and products are made at customer request. Turnover rate on worker recruitment and inventory level was also considered before releasing work order to production line, in which 10 workers used for production. In order to describe the interaction between relevant parameters and define critical factors affected to system performance, simulation technique using Arena software is implemented. As mentioned above, according to simple flow, in which complies with SCOR-model as shown leads to supply chain simulation. The illustration on Arena model is presented. The simulation was run by using assigned variables as the system's performance. The simulation required comparison on system performance such as output productivity, cycle time, while variables were adjusted. The adjustment is applied as an approach, in order to describe the most effect on supply chain and system performance. The results represent sensitivity analysis. It has been noted that increase in turnover was distinctly affected by cycle time and waiting time in process. Meanwhile, time between process and amount of work in process are directly alternated according to demand fluctuation rate. Moreover, comparing with other criteria, rejected parts or loses in production directly result from human error and skill deficit. For example, increasing turnover rate by 32 % impacts the cycle time with a 3.57% increase. Moreover, demand interruption in every UNIF [START_REF]Supply Chain Risk Measurement[END_REF][START_REF] Sarker | A Multi-agent Simulation Study for Supply Chain Operation[END_REF] days, caused a 31.31% increase in worker utilization. While work in process (WIP) quantity and waiting time in process are also obviously increased. More results were explained as presented in table 3. As shown in table 3, on an inbound supply chain, the change in high percentage of turnover, lack of workers' skill and effectiveness impact distinctly on cycle time expansion and losing time in production. On the other hand, an outbound supply chain with variation on demand and supplier lead time affected in processing time and quantities in process. This can be assured that the important of management and collaboration in supply chain helps to enhance manufacturing performance and need for business expansion.

Toward a Multi-Agent System Model

A Multi Agents System (MAS) is the system in which a number of intelligent agents interact with each other. Each agent has their own parameters, indicators and decisions to express their status [START_REF] Sarker | A Multi-agent Simulation Study for Supply Chain Operation[END_REF]. As shown in Figure .5, a simple supply chain agent comprises supplier, manufacturer, distributor and customer. Consequently, supply chain analysis will be applied to decision's model framework. The analysis on collaboration among each partner in supply chain network is mainly focused. For further research, in order to enhance of the effective interaction between supply chain' agents through an agent communication language, a Multi Agents System approach will be used. Certainly, it is beneficial for a firm to develop risk mitigation strategies proactively to handle potential disruptions before risk occur [START_REF] Blackhurst | Supplier Risk Assessment and Monitoring for the Automotive Industry[END_REF].

Conclusion

To support a decision to prevent plant relocation, a proposed framework on manufacturers' decisions on plant situations was introduced, focusing on three perspectives on the situation: Finance, Supply chain and Human factors. The recent study focused on Suppy Chain. In this context, qualitative and quantitative analysis by survey using questionnaires and a model on Arena simulation were implemented. The survey showed factors that influenced investment in three areas: the need for a calibration centre, transportation and worker skill. The strongly impacting factor leading to relocation related to infrastructure and cost, while lack of working skill and abilities caused plant closure situation. Besides, simulation based on SCOR-model supported results on inbound and outbound supply chain, are important on management and collaborate in chain networking. This helps to enhance performance and expand their businesses.

Fig. 1 .

 1 Fig.1. Supply chain structure according to SCOR-M[5]

4

  Application of the framework: Case of Lumphun industrial estate, ThailandTo specify the supply chain system in a manufacturing company, a flow diagram helps to illustrate the system [Figure.4]. The flows are used to model the relation between variables in a continuous system.

Fig. 4 .

 4 Fig. 4. Flow diagram on manufacturing simulation model

Fig. 5 .

 5 Fig. 5. Supply chain decision on plant situation

Table 1

 1 Factor analysis on plant allocation and investment decision from review of literature Factor

analysis on plant allocation/investment decision

		[3]	[8]	[11]	[12]	[13]	[14]	[17] Total
	1. Supply chain cost	x		X	x			3
	2. Production quality		x					1
	3. Market demand			X	x		x	3
	4. Logistics cost				x			1
	5. Employee skills			x		X		2
	6. Expatriate management			x				1
	7. Technological support	X						1
	8. Loyalty to the employer			x				1
	9. Labour productivity			x				1
	10. Close to supplier (Lead time)	X			x		x	3
	11.Economic development policy	x			x		x	3
	12. In-bounded lead time				x			1
	13. Supply chain risk				x		x	x	3
	14. No. of project in R&D	x						x	2
	15. Total investment in R&D		x					1
	16. Return on asset		x					1
	17. Internal culture						x	1
	18. Competition	x					x	2
	1 9 . F i r m s i z e							x	1
	20. Capital to Labour		x					1
	21. Total sales values		x					1
	22. Export sales values		x					1
	23. No. of high educated employee		x					1
	24. Wages of domestic employees		x					1
	25. Security					X		1
	26. Subcontractors existence

X 1

Table 2

 2 Performance attributes and metrics used for the simulation model

	Performance attribute	Metric
	Reliability	Delivery performance
		Fill rate
		Perfect order fulfilment
	Responsiveness	Order fulfilment lead time
	Flexible	Demand chain response time
		Delivery flexibility
	Cost	SC management cost
		Cost of goods sold
		Value added productivity
	Asset	Cash to Cash cycle time
		Inventory days of supply
		Asset Turns

Table 3

 3

	Analysis result by factors affected on system performance
	SCOR Card	Issue			Measurement
	Performance	SCOR Level 1		Cycle	Worker	Waiting	No. WIP Rejected
	attribute	Metrics		time	utilization	time in		part in
						process		prod.
	Asset	Resource turns	Turnover	+3.57%	Not	+0.0766	Not	N/A
			(32% increased)		changed	%	changed
	Supply	Fill rate	Demand	N/A	+31.31%	+30.96% +22.76%	N/A
	chain		fluctuation rate
	reliability		(Interruption 20
			units every
			UNIF
			( 10 , 15) days )
	Cost:	Value added	Human error	+4.82%	+4.3%	+0.256%	Not	+102.94
		employee	(Increased 5%				changed	%
		productivity
	Responsive-	Order		+1.16% -0.1243%	Not	+2.414%	N/A
	ness	fulfillment lead	Supplier lead			changed
		time	time
	Flexible	Supply chain	(1day to 7 days)
		response time

The introduction of Multi Agent System (MAS) is used to simulate the collaboration in supply chain network. In future work an integrated analysis on finance with supply chain risk will lead to making a decision on plant's situation. Nevertheless, enhancing skill and system performance, and knowledge management cannot be abandoned.