Algorithmic Aspects of Todas Theorem

Toda's Theorem is a fundamental result in computational complexity theory, whose proof is based on a reduction from a QBF problem with a constant number of quantifiers to a model counting problem. The recent progress in model counting tools raises the question of whether this reduction, henceforth c