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.