Slaughtering Competition Problems with Quantifier Elimination (2021)

https://grossack.site/2021/12/22/qe-competition.html

by todsacerdoti • 7 months ago

78 3 7 months ago

brantmv• 7 months ago

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

ibobev• 7 months ago

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.

mmaaz• 7 months ago

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.

Slaughtering Competition Problems with Quantifier Elimination (2021)

Related Stories