First page Back Continue Last page Overview Graphics
Some Details
Finite-state machine encoding must be of size polynomial in the input, but allow for exponentially many flights
- Electronic flight formats permit one to say “Flight X leaves every day at 5pm”
- Encoding size is thus governed only by representation of input and number of transition triples
- Polynomial in input (TM specification and input tape)
- TM specification bounded at a small number if one encodes a Universal TM and writes the program on the tape
- Minimum connection time (MCTs) tables make it easy to encode FSM
- MCTs are per-airport specifications of whether one can connect between two flights with specified flight numbers, and if one can, minimum time that must be allowed
Can simulate non-deterministic TMs because their permitted transitions are just as easily encoded using an FSM as deterministic TMs
Solutions are big
- For EXPSPACE, no limit on size of solution because no limit on # of steps
- If polynomial limit is placed on solution size, then can simulate polynomial-sized tape for polynomial number of steps: NP-hard
- ITA Software's engine can run a TM over a tape of size 10 to 20 for 10 to 20 steps
No need to specify input tape: can let system search over all possible input tapes
Notes:
The flight and fare databases necessary for this query do not depend on how long execution takes, unlike Cook's SAT proof. This is because it is possible in the airlines' electronic flight distribution language to say that a flight leaves every day without specifying each departure separately.
For a fixed Turing Machine the only causes of variation in the size of the encoding are that some flights need to be dedicated to forcing the beginning of the first row of the simulation to match the TM input (thus, the flight network grows linearly with the size of the TM input) and the encoding of tape length using minimum and maximum stay restrictions on fares. As it is possible to encode a duration of 2^n using n bits, general travel planning is at least EXPSPACE-hard.
The proof goes through equally well for non-deterministic TMs. This means that even if solution size is bounded to a polynomial of the length of the TM input, the problem is NP-hard.
As will be understood by those familiar with the undecidability proofs of Post’s Correspondence Problem and CFG intersection, the source of complexity here is the combination of finite state constraints (expressible in many ways: in this proof with the flight network) and long-distance “equality” checks (expressed using round-trip priceable units). Both of these are fundamental to the airline industry, though the trips constructed in this proof are very artificial.
An interesting question is whether there is a way to prevent tape permutations in some way other than with minimum and maximum stay restrictions, since this is the limiting factor in the proof's complexity bound. If one could ensure the same geometric equality conditions no matter how long the tape was, then the air travel planning could simulate a TM for an unbounded number of steps on tapes of unbounded length: the problem of finding a valid ticket for a trip would be unsolvable (undecidable) in the general case. For such a proof one needs a way to restrict the ways that priceable units can be laid out in an answer. The airlines do provide one such mechanism, called the back to back restriction. It is not nearly so fundamental to the industry, and not easy to coerce to a form useful for this proof, but it can be used by slightly restructuring the layout of priceable units in solutions, as is possible using a proof based on Diophantine equations. Unfortunately the details of that proof are considerably more complex and add little to the understanding of the problem.