  It is a well-known result that bilevel linear optimization is NP-hard. In
many publications, reformulations as mixed-integer linear optimization problems
are proposed, which suggests that the decision version of the problem belongs
to NP. However, to the best of our knowledge, a rigorous proof of membership in
NP has never been published, so we close this gap by reporting a simple but not
entirely trivial proof. A related question is whether a large enough "big M"
for the classical KKT-based reformulation can be computed efficiently, which we
answer in the affirmative. In particular, our big M has polynomial encoding
length in the original problem data.
