reducing the number of gates by using don't care in the aiger encoding of states
Currently if the winning strategy has n states, we use ⌈log n⌉ latches to binary encode the current state. However if n is not a power of two, some of the states could be encoded with fewer bits, leaving the rest of the bits as "don't care". That's fewer latches to read to decide when we are in those states, and that's more flexibility to decide how to update those latches.
In fact any binary tree with n leaves can be used to encode n states using a number of latches equal to the depth of the tree, so we could also decide to use more latches in order to make certain states very easy to encode.