First-hand information for everyone
What the paper shows in plain terms: a common trick for solving bilevel linear programs (BLPs) is to turn the lower problem into its optimality conditions and add binary switches and big‑M constants to make a single mixed‑integer linear program (MILP). The authors prove that deciding, after the fact, whether the MILP solution is actually optimal for the original bilevel problem is computationally intractable in the worst case. In complexity terms, that decision is coNP‑complete even if only one big‑M parameter might be wrong. They also show related verification tasks remain hard for other reformulations and for min–max special cases without coupling constraints.
What the researchers did and how the reformulation works: the standard route replaces the follower’s linear program by Karush‑Kuhn‑Tucker (KKT) conditions. One resulting condition, complementarity (either a slack is zero or its multiplier is zero), is usually linearized by introducing binary variables and large constants called big‑M values. Those big‑M numbers act as upper bounds that turn logical “either/or” relations into linear inequalities and so yield a MILP that can be fed to standard solvers. The paper studies two questions: (Q1) Given an optimal solution of that MILP, can we efficiently check whether it is bilevel‑optimal? and (Q2) Given an optimal MILP solution, can we efficiently verify that the chosen global big‑M values are correct (that they do not cut off any feasible or optimal follower solutions)?
Main technical findings: the authors prove that Q1 is coNP‑complete — so unless widely believed complexity collapses occur, there is no polynomial‑time algorithm that always verifies bilevel optimality a posteriori. The hardness holds even when the two big‑M constants are equal, and it extends to strong‑duality based reformulations for mixed‑integer bilevel programs and to min–max instances without coupling constraints. For Q2 they show that checking global big‑M correctness remains computationally difficult even when an optimal MILP solution is provided. They also present approximation‑style hardness: even deciding an ε‑approximate optimality is coNP‑hard for any fixed ε in (0,1).
Why this matters: practitioners often pick large big‑M values without formal checks, solve the resulting MILP with off‑the‑shelf solvers, and accept the solution as bilevel‑correct. The paper gives a theoretical explanation why that practice is risky: after solving, it may be computationally infeasible to verify correctness of the solution or of the big‑M choices in general. It also explains a tradeoff: making big‑M values provably safe is possible in polynomial time, but the safe values may be impractically large and slow solvers down.
Important caveats and scope: these are worst‑case, complexity‑theoretic results. They show that no algorithm can always verify correctness quickly in all instances unless major complexity breakthroughs happen. They do not mean every practical instance is unverifiable or that heuristic checks are useless. The results apply to optimistic bilevel linear programs under the KKT (and related) reformulations studied in the paper, and they rely on standard assumptions used to make the bilevel problem well‑posed. The paper provides reductions from known hard problems (integer linear program optimality verification) to establish the formal hardness statements.