Propositional formula minimization is $Σ_2^p$-complete under many-one reductions

Overview & Synopsis

The Minimum Equivalent Expression problem (MEE) asks, given a propositional formula $φ$ and an integer $k$, whether $φ$ is equivalent to a formula with at most $k$ occurrences of propositional variables. While the problem is clearly in $Σ_2^p$, its completeness under polynomial-time many-one reductions has remained open since at least 1979. Buchfuhrer and Umans showed in 2008 that it is $Σ_2^p$-complete under polynomial-time Turing reductions. In this note, we present a proof discovered by GPT-Sol-6.1 which establishes that MEE is $Σ_2^p$-complete also under polynomial-time many-one reductions.