next up previous
Next: The Planar Crossover Construction Up: Sokoban is PSPACE-complete Previous: Basic Forbidden Configurations and

The Turing Machine Emulator

The basic form of the TM emulator is shown in figure 6.

 figure263
Figure 6: Cellular Unit of the TM 

The shaded boxes are collections of devices representing particular subsystems of the TM. This figure represents the state control system and tape symbol for one tape cell and for only one entry state. Other states would need copies of this structure, sharing only the Tape Symbol section. These ``other states'' are represented by cloud-like regions.

On entry, the only pass-reset not in the closed position would be one in the Tape Symbol region; that one would represent the symbol currently held at this tape location. In this construction, only `0', `1' and blank (`b') are represented.

The pusher would proceed through the crossover devices to the pass-reset in the Entry State Indicator region, which could then be reset to the open position. Note that to exit this Cellular Unit (to the next or pervious cell) the pusher must pass through this device.

The pusher may then proceed only to the Tape Symbol region, and since only one symbol is represented, only one of these devices will be open. This forces the exit route from the Tape Symbol, and passage through it erases the symbol by closing the pass-reset device. Since only one Entry State Indicator device is open, only one path is open to the pusher. Note that this path is determined by the entry state and the tape symbol, thus ensuring the TM emulation.

On the path from the Tape Symbol region to the Entry State Indicator, the pusher has the opportunity to reset exactly one tape symbol, and to open one device in the Select Next State region. The latter is required, for otherwise the pusher will not be able to exit this Cellular Unit. Note the use of reversers to allow multiple path entries to the Tape Symbol devices and the Select Next State devices while ensuring that the pusher cannot switch to another exit path.

This construction shows that it is possible for the pusher to follow the TM execution. However, to complete our proof we need to consider the following:

  1. If the TM halts and accepts, there may be (an arbitrary number of) unvisited tape cells. In the emulator, these unvisited cells will still have the pass-reset device in the open state, meaning the puzzle has not yet been solved.
  2. While some of these cells may be input characters, the remaining ones may be blanks beyond the end of the input. We cannot meet the linear time bounds if there are too many of these (in particular, if we want an infinite extension).
  3. The TM may visit every cell on a finite tape, but halt without accepting, or not halt due to cycling. In either case, the puzzle may still be solved by the emulator because the pusher may fail to reset the Tape Symbol before exiting the Cellular Unit.

First, we add a Halt-Accept corridor that can only be reached by exiting some Cellular Unit by emulating a transition to a halt accept state. From this corridor, connections to each Tape Symbol region, controlled by a pass-reset device in the Entry State Indicator, will allow closure of all open Tape Symbol devices.

To ensure the linear time emulation, we will use on-the-fly initialization. We add a special end-of-tape symbol that behaves identically to the blank symbol except that it allows the pusher to reset the end-of-tape symbol in the next Tape Symbol region. All Tape Symbol devices beyond the end-of-tape symbol will be closed initially. Thus, even in an infinite version, only a finite number of boxes, representing the input symbols, will be out of storage location initially.

Finally, to prevent false solutions, the Halt-Accept corridor will have one box not in a storage location initially. This means the puzzle can only be solved if the TM halts in the accept state, which allows the pusher to reach this last box. To meet the time bound, this box must be located near the first Cellular Unit.

The Sokoban puzzle will have a solution if and only if the TM being emulated halts in the accept state, and in this case the solution will be tex2html_wrap_inline722 moves (and pushes) long.


next up previous
Next: The Planar Crossover Construction Up: Sokoban is PSPACE-complete Previous: Basic Forbidden Configurations and

& Culberson
Thu Apr 3 11:48:56 MST 1997