# Transforming searching to SAT(isfiability)

I'm having problems trying to understand a powerpoint our teacher gave us. The topic is on the theory of NP-Completeness. My biggest questions are,
1. How does the author derive all the 8-22 statements simply from 8-21?
2. How does the author change the '&'s and '-->'s to 'v's from 8-22 to 8-23?
3. Why is x(1)=7 and x(2)≠7 alone? What does "input data" mean?

8-21

Transforming searching to SAT

Does there exist a number in { x(1), x(2), …, x(n) }, which is equal to 7? Assume n = 2. nondeterministic algorithm:
i = choice(1,2)
if x(i)=7 then SUCCESS
else FAILURE

8-22

i=1 v i=2
& i=1 → i≠2
& i=2 → i≠1
& x(1)=7 & i=1 → SUCCESS
& x(2)=7 & i=2 → SUCCESS
& x(1)≠7 & i=1 → FAILURE
& x(2)≠7 & i=2 → FAILURE
& FAILURE → -SUCCESS
& SUCCESS (Guarantees a successful termination)
& x(1)=7 (Input Data)
& x(2)≠7

8-23

CNF (conjunctive normal form) :
i=1 v i=2 (1)
i≠1 v i≠2 (2)
x(1)≠7 v i≠1 v SUCCESS (3)
x(2)≠7 v i≠2 v SUCCESS (4)
x(1)=7 v i≠1 v FAILURE (5)
x(2)=7 v i≠2 v FAILURE (6)
-FAILURE v -SUCCESS (7)
SUCCESS (8)
x(1)=7 (9)
x(2)≠7 (10)

-
The second "8-22" is supposed to read "8-23"? – joriki Apr 11 '11 at 14:31
On your question 2: $A\rightarrow B$ is equivalent to $\neg A \lor B$. Applying this yields the same clause labeled (2) twice; that's why there's one fewer clause in 8-23 than in 8-22. Also, applying this when $A$ is a conjunction yields a disjunction via $\neg(C\land D)=(\neg C)\lor(\neg D)$. – joriki Apr 11 '11 at 14:34
Thanks joriki! Now if I only knew what choice meant... – Some Noob Student Apr 12 '11 at 10:42

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

1. 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$.

1. 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.

-