SATs are cool but MILPs are cooler IMO.
Lol I've been trying to train a neural network over a finite field, not the reals and oh my god MILPs are God's gift to us.
If you get sick of MILPs, maybe you could use a representation of your finite field instead of the field itself? That way you could do everything in C^n, and preserve differentiability to use SGD or something like it.