There is no general purpose solver available that can symbolically solve 20M equations, and unfortunately, progress in this field has been excruciatingly slow.

It's highly unlikely it's possible, even in theory. Symbolic solvers must explore many known "routes" to expand and simply given equations, without any theoretical guarantees. Even if you found a symbolic solution to your 20M system, it'd have so many terms in it that you'd have to settle for a numerical approximation, just to make sense of them all.

Numerical solvers are of course, a different matter, altogether.

Ahh nuts. I was foolishly optimistic because my experience with SAT solvers has been magical where they can effortlessly chew through huge numbers of constraints. Was thinking that computers are really fast and good at math, surely they can balance a bunch of algebra given some guidance.

Ah well. Will have to resign myself to raw numbers.