[SloopJon]

I got the solution with a straightforward set of assertions in Z3. It was a lot of typing, and I wonder if there's a more succinct way to do this than the following:

    (declare-const blitzen Int)
    (declare-const comet Int)
    ...
    (assert
      (and
        ; lower bound for readability (1 is front)
        (> blitzen 0)
        (> comet 0)
        ...
        ; upper bound for readability (9 is rear)
        (< blitzen 10)
        (< comet 10)
        ...
        ; clues from the puzzle
        (> vixen rudolph)
        ...
        (< dasher vixen)))