AT checker TM. Develop a TM that can check whether a given set of values satisfies a given SAT instance. Assume that there are three variables, that the alphabet is # 0 1 x y z x' y' z' ( ) # , and...

AT checker TM. Develop a TM that can check whether a given set of values satisfies a given SAT instance. Assume that there are three variables, that the alphabet is # 0 1 x y z x' y' z' ( ) # , and that the initial contents of the tape are the values of x, y, and z to be checked followed by the shortcut form of the SAT instance. For example, the tape for the example given in the text would contain

Solution. See the TM drawn at right. For each variable, it reads a value, substitutes that value for the variable everywhere in the expression during a scan to the right, and then substitutes the complement of that value for the negated symbol for the variable everywhere in the expression during a scan to the left. After making all the substitutions, the five states at the bottom of the TM scan the expression for a pair of parentheses that does not enclose any 1 values. If such a set is found, it enters a Yes state. If not, it enters a No state. This solution easily extends to n variables, but is not a proof that SAT is in NP. A more complicated construction that is independent of n is necessary.