Propositional formula minimization problem proven complete for a complex class
Propositional formula minimization is $Σ_2^p$-complete under many-one reductions
Computational ComplexityLogic in Computer Science
Summary
Figuring out the simplest form of a logical expression has been a tough puzzle studied since the 1970s. The problem asks if you can rewrite a logical formula using fewer variable uses but without changing its meaning. Previous work showed this problem is very complex but left some details open about exactly how complex it is. The authors present a new proof that confirms the problem belongs to a particularly challenging complexity class, resolving a long-standing open question.
What this means in practice
- •For logic circuit designers: Understand the inherent computational limits when minimizing logical expressions for hardware optimization.
- •For automated reasoning tool developers: Use the complexity classification to guide the design of heuristics for formula simplification in software verification tools.
A theory result. No direct application yet.
Authors
Reijo Jaakkola
Abstract
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.