[garethrees]

Yes, that's right.

The paper doesn't explain in detail how the gadgets are assembled. But presumably the track is arranged so that from the starting point the car must enter the variable gadget for X1. The "true" branch for X1 then visits each clause gadget containing X1, and the false branch visits each clause gadget containing ¬X1. These two branches must then come together somehow (no gadget is given, but it's easy to see how to make one), and then enter the variable gadget for X2, and so on.

So if the car could steer in mid-air, then it would be able to jump from ¬X3 (say) back to X1, and this would allow it to repeat the track for the X2 and X3 variables, and it could make a different choice on the second run through, thus making its path no longer correspond to a 3SAT solution.

[roundsquare]

Thanks, that's basically how I saw it. I guess that's one way how this proof essentially makes the problem discrete (in addition to assuming perfect driving).