SAT checker simulation. Make a text file giving a tabular representation for the universal DFA TM from Exercise 5.5.38, download TuringMachine.java and Tape.java from the booksite, modify them as described in Exercise 5.2.7 and Exercise 5.2.8, and produce this trace of the machine running with the specified input.
Solution.
Exercise 5.5.38
SAT 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
# 0 1 1 ( x' + z ) ( x + y' + z ) ( x + y ) ( x' + y' ) #
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.
Exercise 5.2.7
Add code to Tape to implement its toString() method. To match the output of Program 5.2.2, suppress the metasymbol #
Program 5.2.2
Exercise 5.2.8
Add code to Turing Machine to print a line with the state name, position of the tape head, and the tape contents, each time that the machine changes state. Modify the toString() method in Tape to leave in the met symbol # and mark the position of the tape head by printing matching square brackets before and after the symbol under the tape head.