Slaughtering Competition Problems with Quantifier Elimination (2021)(grossack.site)

78 pointsby todsacerdoti7 months ago3 comments

Slaughtering Competition Problems with Quantifier Elimination (2021)

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

4 comments

mmaaz6 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.

brantmv7 months ago

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

ibobev7 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.

[deleted]7 months ago