Search arXiv⌕ Search

arXiv · 2610.34516

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

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.

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Reijo Jaakkola. 2026-10-25. Propositional formula minimization is $Σ_2^p$-complete under many-one reductions. https://arxiv.org/abs/2610.34516

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

Optimal Inapproximability of Satisfiable $k$-LIN over Non-Abelian Groups

A seminal result of Håstad [J. ACM, 48(4):798--859, 2001] shows that it is NP-hard to find an assignment that satisfies $\frac{1}{|G|}+\varepsilon$ fraction of the constraints of a given $k$-LIN instance over an abelian group, even if there is an assignment that satisfies $(1-\varepsilon)$ fraction of the constraints, for any constant $\varepsilon>0$. Engebretsen et al. [Theoretical Computer Science, 312(1):17--45, 2004] later showed that the same hardness result holds for $k$-LIN instances over any finite non-abelian group. Unlike the abelian case, where we can efficiently find a solution if the instance is satisfiable, in the non-abelian case, it is NP-complete to decide if a given system of linear equations is satisfiable or not, as shown by Goldmann and Russell [Information and Computation, 178(1):253--262. 2002]. Surprisingly, for certain non-abelian groups $G$, given a satisfiable $k$-LIN instance over $G$, one can in fact do better than just outputting a random assignment using a simple but clever algorithm. The approximation factor achieved by this algorithm varies with the underlying group. In this paper, we show that this algorithm is {\em optimal} by proving a tight hardness of approximation of satisfiable $k$-LIN instance over {\em any} non-abelian $G$, assuming $P \neq NP$. As a corollary, we also get $3$-query probabilistically checkable proofs with perfect completeness over large alphabets with improved soundness. Our proof crucially uses structural properties captured by Gowers' notion of {\em quasi-randomness} for non-abelian groups [Combinatorics, Probability and Computing, 17(3):363--387, 2008].

cs.CC↗

Polynomial and Hyperplane Avoidance over the Integers with Applications to Integer-Point Counting

We study the \emph{Polynomial Avoidance Problem}: given a finite collection $F \subseteq Z[x_1,\dots,x_n]$ of nonzero polynomials, find a vector $x \in Z^n$ of minimum $\ell_p$-norm such that $f(x)\neq0$ for every $f \in F$. Each polynomial is given sparsely as a list of its nonzero terms. The affine special case is the \emph{Hyperplane Avoidance Problem}. This special case arises in Barvinok-type algorithms for counting integer points in polyhedra, when certain rational generating functions must be evaluated at a removable singularity. Our main results are as follows: 1) Let $D:=\sum_{f\in F} \text{deg} f$. Every instance admits a feasible vector $x$ satisfying \[ \|x\|_1 \leq \min\left\{D,\frac{D+n}{2}\right\}. \] This bound is tight. Such a vector can be found by a deterministic algorithm whose bit complexity is polynomial in $D$ and the sparse encoding length of the input. Our proof uses a new algorithmic variant of the \emph{Combinatorial Nullstellensatz}; 2) In the affine case, with $m$ input polynomials, such a vector can be constructed by a fast deterministic polynomial-time algorithm using $O(nm)$ arithmetic operations. For the homogeneous case, Barvinok's original approach provides only the weaker guarantee $\|x\|_1 = O((nm)^{n-1})$; 3) The problem is NP-hard for every $p\in R_{\geq 1}\cup\{\infty\}$, even for homogeneous linear forms; 4) As an application, we improve the complexity bound for counting integer points in general rational polytopes. We also improve the bound for polyhedra of bounded codimension; this includes the counting version of the \emph{Unbounded Subset-Sum} problem as a special case.

cs.CC↗

Even more properties of parity based bit-counting complexity classes

We investigate several additional properties of parity based bit-counting complexity classes ${\bf B_{|0|\oplus}P}$ and ${\bf B_{|1|\oplus}P}$. We first prove that ${\bf C_=P}={\bf ES}={\bf MNS}\subseteq{\bf P}^{{\bf B_{|1|\oplus}P}}={\bf P}^{{\bf B_{|0|\oplus}P}}$. We then build upon the four consecutive value theorem from \cite{P26b} and develop a bit recovery procedure that reconstructs the binary representation of a ${\bf \#P}$ value one bit at a time by querying appropriately padded and shifted versions of that value. Using this procedure, we prove that ${\bf PP}\subseteq{\bf P}^{{\bf B_{|1|\oplus}P}}$ and ${\bf PP}\subseteq{\bf P}^{{\bf B_{|0|\oplus}P}}$, which consequently yields ${\bf P}^{\bf PP}={\bf P}^{\bf B_{|0|\oplus}P}={\bf P}^{\bf B_{|1|\oplus}P}$. Furthermore, since this procedure recovers the complete numerical output of a ${\bf \#P}$ function, it also establishes the functional containments of ${\bf \#P}\subseteq{\bf FP}^{{\bf B_{|1|\oplus}P}}$ and ${\bf \#P}\subseteq{\bf FP}^{{\bf B_{|0|\oplus}P}}$. We additionally demonstrate that caching repeated oracle queries reduces the number of distinct queries required for the bit recovery procedure from $4n$ to $2n+2$. Finally, we prove that parity based bit-counting hierarchies ${\bf ΣB_{|0|\oplus}H}$, ${\bf ΣB_{|1|\oplus}H}$, ${\bf ΔB_{|0|\oplus}H}$ and ${\bf ΔB_{|1|\oplus}H}$ contain ${\bf CH}$. As a result, these hierarchies coincide with ${\bf CH}$ since the reverse containments were already established in \cite{P26b}.

cs.CC↗