CNF for modilisation of a word

Question

Imagine that we are interested in problem of words. A word is a sequence of letters from a $\Sigma$ alphabet. For encoding a word in SAT we are using variable like $x_{i,a}$ which means that in position $i$ we find the letter $a$.
So now my problem is this: Find a CNF formula which expresses that the variables $x_{i,a}$, with $i$ ranging from 1 to $n$ (the size of the word), encode a word of size $n$. That is for any position $i$, there is exactly one letter of $a \in \Sigma$ that appears in that position.
So far I came up with this but I am not sure if it is true:
$$\bigwedge_{i=1}^n \; \bigwedge_{a \in \Sigma \\ a' \in \Sigma} \neg x_{i,a} \lor \neg x_{i,a'}$$ So this means that we can't have in the same time two letters in position $i$.

Answer 1

Long comment

Quite...

Let start approaching the problem from a different point of view: to say that position $i$ is filled with symbol $a$ can be written in predicate logic as follows:

$\forall s \in \Sigma (\text {In}(i,a) \to \lnot \text {In}(i, s))$,

which is equivalent to: $\forall s \in \Sigma (\lnot \text {In}(i,a) \lor \lnot \text {In}(i, s))$.

Assuming a finite alphabet of symbols $\Sigma$, we may replace the universal quantifier with a finite conjunction.

But we have to take care of the case: $s_k=a$, for some $k$: when "scanning" the symbols of $\Sigma$, at a certain point we will find $a$ itself.

In that case we have that the conjunct: $(\lnot \text {In}(i,a) \lor \lnot \text {In}(i, s_k))$ is false.