1. How does the author derive all the 8-22 statements simply from 8-21?
First, let me explain 8-21. It is written shortly, so it can be a little hard to understand if you don't know what to look for.
Transforming searching to SAT Does there exist a number in { x(1), x(2), …, x(n) }, which is equal to q (given search value)? i = choice(1,2,...,n) #i is the eventual (non-determistic, ie. any) index of x if x(i)=q then SUCCESS #if x(any i) == q, #then q is in x and success. else FAILURE
- How does the author derive all the 8-22 statements simply from 8-21?
Now let's go through them 8-22:
i=1 v i=2
Here $i$ represents the index into $\mathbf{x}$. The presentation is only showing it for $|\mathbf{x}|=2$ (size of $\mathbf{x}$ equal to 2).
It general it would look like:
i=1 v i=2 v ... v i=n
Where $n=|\mathbf{x}|$. This basically says: $i$ is an index of the sequence $\mathbf x$. It can be any value in the range $[1,n]$.
Next:
i=1 → i≠2 i=2 → i≠1
Here we say if $i=1$ then $i\neq 2$. This makes sense, though I am not sure it is necessary, since in SAT or SMT, assigning the values one way would automatically imply they are not equal to other values.
In general, the presentation would do it this way:
i=1 → i≠2 ^ i≠3 ... i≠n i=2 → i≠1 ^ i≠3 ... i≠n ...
Next:
x(1)=7 & i=1 → SUCCESS
Here we are saying: if $x_1=q\text{ (search value) }$ then $q$ (the given search value) exists in $\mathbf x$, and the SUCCESS boolean variable is true.
Next:
x(1)≠7 & i=1 → FAILURE
Here we are saying, that if $i$ is somehow forced to be $1$, and $x_i\neq \text{search value}$, then the search did not succeed. This makes sure that we get the right $i$ when the search value is in $\mathbf x$.
FAILURE → -SUCCESS
This simply connects failure to being unsuccessful, so that we cannot have FAILURE and SUCCESS at the same time.
SUCCESS
Forced the SUCCESS value to be True, since we want to find a satisfiable $i$ where $x_i=q$.
- Why is x(1)=7 and x(2)≠7 alone? What does "input data" mean?
x(1)=7 x(2)≠7
Here the presentation is simply listing input data (filling out $\mathbf x$. I think the 2nd line is unnecessary; simply filling out the correct values for each $x_i$ implies that they do not equal other values.
Generalizing this:
x(1)=1st value in x x(2)=2nd value in x ... x(n)=nth value in x #This is if you add the (unnecessary IMO) counter conditions. x(2)≠1st value in x ... x(2)≠nth value in x
And so on. I think that the ≠ parts are unnecessary, but I could be wrong. This type of logic plays tricks on me.
So in summary to question (2), we make an SAT problem where $i$ is the index into $\mathbf x$, and we restrict $i$ to the index values of $\mathbf x$. We then associate each $i$ with $x_i=q \rightarrow SUCCESS$. and then force SUCCESS to be true. We then ask the SAT solver for a satisfying assignment; the only one should be an $i$ such as that $x_i=q$. If the solver fails, then we know that there is no $i$, such as that $x_i=q$.
2. How does the author change the '&'s and '-->'s to 'v's from 8-22 to 8-23?
So if we have $a \rightarrow b$, the way to write this as a CNF clause is: $(-a \vee b)$. In english: "if $a$ then $b$" is the same as "not $a$, or $b$".
Another type of clause that appears is $(a \wedge b) \rightarrow c$. Now we convert this in the same way as $(a \rightarrow b)$:
$\begin{align} && (a \wedge b) \rightarrow c\\ &=& -(a \wedge b) \vee c && \text{Same rule as }a \rightarrow b\text{ explained above}\\ &=& (-a \vee -b) \vee c && \text{De Morgan's laws}\\ &=& -a \vee -b \vee c\\ \end{align}$ Note we use De Morgan's laws.
Now for 8-23. The left is 8-22, the right is 8-23, with a reason in the #comment reason.
i=1 v i=2 => i=1 v i=2 #copied & i=1 → i≠2 => i≠1 v i≠2 #rule a->b = -a v b & i=2 → i≠1 => i≠2 → i≠1 #ommited, because same as previous line & x(1)=7 & i=1 → SUCCESS => x(1)≠7 v i≠1 v SUCCESS #rule (a ^ b -> c) = -a v -b v -c & x(2)=7 & i=2 → SUCCESS => x(2)≠7 v i≠2 v SUCCESS #rule (a ^ b -> c) = -a v -b v -c #.... So on & FAILURE → -SUCCESS => -FAILURE v -SUCCESS #rule a->b = -a v b & SUCCESS #copied #copy rest.