Long and skinny knights tours: the FDR approach.

Don Knuth gave a talk here recently in which he investigated patterns of knight's tours in 3xN boards: finding
what sorts of tours there are and who many of them there are.  Naturally I decided to investigate this with FDR
(though I found it equally possible to handle 4xN).  This has led to

1. A linear-time way of searching for knights tours directly in 3xN and 4xN boards, using inductive compression.
2. The best examples of FDR-driven (non data independent) induction I have ever seen.
3. A completely new technique for getting FDR to ignore pointless states in a search.  [Specifically: given a compressed partial system, how do you get it not to do a lot of work exploring branches where that partial
   system cannot  reach the target "done" event.]
4. A technique for counting and enumerating all the traces of a system with length K or less that end in done.
5. The potentially automatic generation of recurrence relations that govern the number of knight's tours in 3xN and 4xN boards.