This page concerns the construction given in the Automata Theory textbook by Hopcroft, Motwani and Ullman for proving the NP-completeness of the satisfiability problem. The presentation is given in section 10.2.3, starting on page 428 of the textbook. You need to refer to the textbook in order to understand the context in which the discussion is made.
The construction presented there is flawed. First I give the theoretical reason, then a piece of software that actually implements the proposed construction. Using the software, you will be able to see precisely what propositional formula is generated, and also test it for satisfiablity. This is followed by a correct construction, as well as the software that implements it.
The expression generated by the construction is the conjunction of starts-right, next-move-is-right and finishes-right. Next-move-is-right is given on page 434 as
N=N0 /\ N1 /\ ... /\ Np(n)-1
Ni is given on page 433 as
Ni = (Ai0 \/ Bi0) /\ (Ai1\/Bi1) /\ ... /\ (Ai,p(n)\/ Bi,p(n))
Note that in order for the full expression to be true under an interpretation, for a given k, either Ai,k or Bi,k must be true. Both of them cannot be false.
With this formula, there are cases where we would expect a given interpretation to satisfy the corresponding propositional formula (because it describes precisely the computation carried out by the turing machine), but in fact it doesn't. The problem is that even though the cases specified by Aij and Bij are mutually disjoint, they do not form a partition of all the possibilities that relate variables to one another. Bij says that the variable Xij is not a state, and that its immediate neighbors are also not states, so that it can be copied directly below to the next line. The opposite of this statement is ( Xi,j-1 is a state OR Xi,j is a state OR Xi,j+1 is a state), not just (Xi,j is a state). The other possibilities must also be taken into consideration.
Correct (but still incomplete) solution:
Changing the definition for Ni rectifies the situation. The correct formula is
Ni = (Ai0 \/ Ai1 \/ Bi0) /\
(Ai0 \/ Ai1 \/ Ai2 \/ Bi1) /\
(Ai,k-1 \/ Ai,k \/ Ai,k+1 \/ Bi,k) /\
( Ai,p(n)-1 \/ Ai,p(n)\/ Bi,p(n))
The above solution is incomplete, because is does not incorporate the case when "a given ID contains a final state, and the ID that follows it should be its copy".
Correct and Complete Solution:
Let us define Cij as
Cij = Yi,j-1,a /\ Yi,j,f /\ Yi,j+1,d /\ Yi+1,j-1,a /\ Yi+1,j,f /\ Yi+1,j+1,d
where a, d are members of the alphabet (or blank) and f is a final state. Let us also modify Aij such that it is applicable only if Xij is a non-final state.
Then the correct formula that handles all possibilities is:
Ni = (Ai0 \/ Ai1 \/ Ci0 \/ Ci1\/ Bi0) /\
(Ai0 \/ Ai1 \/ Ai2 \/ Ci0 \/ Ci1 \/ Ci2 \/ Bi1) /\
(Ai,k-1 \/ Ai,k \/ Ai,k+1 \/ Ci,k-1 \/ Ci,k \/ Ci,k+1 \/ Bi,k) /\
( Ai,p(n)-1 \/ Ai,p(n) \/ Ci,p(n)-1 \/ Ci,p(n)\/ Bi,p(n))
Obviously, we should take care of the non-existent variables also, as specified in the textbook (the case where j=0 and j=p(n)).
Software- implementing the construction in the book:
The software consists of a reducer and a satisfiability checker. It is written and compiled in SWI-Prolog (by me, of course!) You need to provide two files of your own - one that describes a Turing Machine, with its input, another for describing which variables are true (i.e. an Interpretation). A sample file is given for both of these. Note that in this implementation, the definition of Aij incorporates the case where Xij is a final state.
The program that implements the construction in the book is consists of the files main.pl reducer.pl utilities.pl and satisfier.pl . You will also need an input file that describes the Turing Machine (see as an example tm.pl) and an input file that gives an Interpretation (see as an example tv.pl). You are advised to put all these files in one directory before you start. You will be prompted for the names of these files containing the Turing Machine and the Interpretation by the program. readme.txt describes briefly how the program works.
Software- implementing the correct and complete construction:
The same instructions apply here. The files now are main.pl reducer.pl utilities.pl and satisfier.pl . Only the reducer is really different from the other version. Two sets of sample input files: tm.pl (Turing Machine) tv.pl (Interpretation) and tm2.pl (Turing Machine 2) and tv2.pl (Interpretation 2) are provided. Using the same format as these files, you can specify your own Turing Machines and Interpretations. Save all these files in a different directory, and execute the program as specified in the readme.txt file.
You can obtain a copy of the SWI Prolog system for your specific machine at http://www.swi.psy.uva.nl/projects/SWI-Prolog/ .
Please feel free to write to me in case of questions or comments. I am at firstname.lastname@example.org . An here is my home page.