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$.
1 Answer
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.
-
$\begingroup$ Thank you for your response. I have some problems understanding you response. What I am looking here is to find a CNF for this problem but you are talking about predicate logic. After some thinking, I changed my solution to $\bigwedge_{i=1}^n (\bigvee_{a \in \Sigma} x_{i,a}$) but again I am not one hundred percent sure $\endgroup$ Commented Oct 29, 2020 at 12:07
-
$\begingroup$ @Mohammadreza - it is only for "readibility". I've used $\text{In}(i,a)$ in place of $x_{i,a}$. $\endgroup$ Commented Oct 29, 2020 at 13:09
-
$\begingroup$ Having said that, the two big conjunctions are ok; but you have to add the condition $a \ne a'$. $\endgroup$ Commented Oct 29, 2020 at 13:09
-
$\begingroup$ But if I add $a \neq a'$, it means that the letter is position $i$ could not be any letter but $a$ which means that in position $i$ we could have something like $aa$. Or maybe my understanding of $a \neq a'$ is wrong? $\endgroup$ Commented Oct 30, 2020 at 12:12
-
$\begingroup$ and this formula says that in every position there is only and only one letter. How could I say that in every position $i$ there is a letter (couldn't I use the same formula or something like this would also work $\bigwedge_{i=1}^n \; (\bigvee_{a \in \Sigma} x_{i,a})$ $\endgroup$ Commented Oct 30, 2020 at 12:16