The Minimum Formula Size Problem is (ETH) Hard

A longstanding open question is whether the Minimum Circuit Size Problem (MCSP) is NP-complete. In fact, even determining whether MCSP has a search-to-decision reduction has been open for over twenty years. We show that, under the Exponential Time Hypothesis, the Minimum (DeMorgan) Formula Size Problem, MFSP, is not in P. Building on this, we show that MFSP has a polynomial-time (exact) search-to-decision reduction, a result that does not relativize. Our main technique relates the formula complexity of a partial function with the formula complexity of an associated total function and is proved using the “leaf weighting” technique of Buchfuhrer and Umans.