Second optimization I would apply would be quadtrees. Start with huge squares subdivide them after solving at that level down to your specified tollerence.
If you need even more precision either tiled hexagon automata or subdivide into K instead of four compass orientations.
There is also probably some Pressburger arithmetic formulation treating it as vectors in 2D you could whack with an SMT solver? I'd have to sleep on that. Might be easier to code than all the finite state automata merging.
