Long and skinny knights tours: the FDR approach.
Bill Roscoe ( OUCL )
- 11:30 23rd February 2011 ( week 6, Hilary Term 2011 )Room 147, Oxford University Computing Laboratory
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
- A linear-time way of searching for knights tours directly in 3xN and 4xN boards, using inductive compression.
- The best examples of FDR-driven (non data independent) induction I have ever seen.
- 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.]
- A technique for counting and enumerating all the traces of a system with length K or less that end in done.
- The potentially automatic generation of recurrence relations that govern the number of knight's tours in 3xN and 4xN boards.