Slaughtering Competition Problems with Quantifier Elimination (2021)

To provide some additional context: the algorithm being used by QEPCAD is cylindrical algebraic decomposition, which has a time complexity 2^2^n (yes, doubly exponential). So, while in theory many problems could be solved by tossing them into CAD, this is often not tractable. This isn’t a knock against CAD: imo it is one of the most fundamental and under-appreciated algorithms and I devoted a big chunk of my PhD thesis to it.

By the way, to my knowledge QEPCAD is essentially the only complete open-source implementation of it. Mathematica also implements it. I wrote one of the few open-source implementations of it, although it does not do quantifier elimination; it only returns the truth of a given statement. https://github.com/mmaaz-git/cad.

For anyone wondering, "mse" probably means "math Stack Exchange".

More interesting to me is the actual algorithm that the software uses and whether it is practical to apply it with pen and paper in an actual competition, if the number of steps is not too high, of course. Unfortunately, the article didn't go into that depth.