Introduction:
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 (second edition). 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.
Theoretical Reasoning:
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:
Unzip the contents of incorrect.zip in a directory. 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:
Unzip the contents of
correct.zip in a directory. The same instructions apply here. 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.
SWI-Prolog:
You can obtain a copy of the SWI Prolog system for your specific machine at
http://www.swi-prolog.org/ .
An equivalent approach was adopted in the errata for the textbook.
