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. 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=N_{0} /\ N_{1} /\ ... /\ N_{p(n)-1}

N_{i} is given on page 433 as

N_{i } = (A_{i0} \/ B_{i0}) /\ (A_{i1}\/B_{i1})
/\ ... /\ (A_{i,p(n)}\/ B_{i,p(n)})

Note that in order for the full expression to be true under an
interpretation, for a given k, either A_{i,k }or B_{i,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 A_{ij
}and B_{ij }are mutually disjoint, they do not form a partition of
all the possibilities that relate variables to one another. B_{ij} says
that the variable X_{ij} 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 ( X_{i,j-1} is a
state OR X_{i,j }is a state OR X_{i,j+1} is a state), * not*
* just *(X_{i,j}
is a state). The other possibilities must also be taken into
consideration.

Correct (but still incomplete) solution:

Changing the definition for N_{i} rectifies the situation. The
correct formula is

N_{i } = (A_{i0} \/ A_{i1}
\/ B_{i0}) /\

(A_{i0}
\/ A_{i1} \/_{ } A_{i2} \/ B_{i1}) /\

...

(A_{i,k-1}
\/ A_{i,k }\/ A_{i,k+1} \/ B_{i,k}) /\

...

( A_{i,p(n)-1}
\/ A_{i,p(n)}\/ B_{i,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 C_{ij }as

C_{ij }= Y_{i,j-1,a} /\ Y_{i,j,f}
/\ Y_{i,j+1,d} /\ Y_{i+1,j-1,a} /\ Y_{i+1,j,f }/\
Y_{i+1,j+1,d}

where **a, d** are members of the alphabet (or blank) and **f** is a
final state. Let us also modify A_{ij} such that it is applicable only
if X_{ij} is a non-final state.

Then the correct formula that handles all possibilities is:

N_{i } = (A_{i0} \/ A_{i1}
\/ C_{i0} \/ C_{i1}\/ B_{i0}) /\

(A_{i0}
\/ A_{i1} \/_{ } A_{i2} \/ C_{i0} \/ C_{i1}
\/_{ } C_{i2 }\/ B_{i1}) /\

...

(A_{i,k-1}
\/ A_{i,k }\/ A_{i,k+1} \/ C_{i,k-1} \/ C_{i,k }\/
C_{i,k+1} \/ B_{i,k}) /\

...

( A_{i,p(n)-1}
\/ A_{i,p(n)} \/ C_{i,p(n)-1} \/ C_{i,p(n)}\/ B_{i,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 A_{ij} incorporates the case where X_{ij}
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.

SWI-Prolog:

You can obtain a copy of the SWI Prolog system for your specific machine at http://www.swi.psy.uva.nl/projects/SWI-Prolog/ .

Feedback:

Please feel free to write to me in case of questions or comments. I am at zeki.bayram@emu.edu.tr . An here is my home page.