MIN-FORMULA $\in$ NP

Question

I am thinking about the following problem: Show that MIN-FORMULA $\in$ NP.

MIN-FORMULA is the set of minimal boolean formulas, i.e. formulas such that there is no shorter formula that computes the same boolean function.

I would like to have an advise whether or not the following approach/idea is ok.

Show by describing a non-deterministic algorithm N that solves the question of elementhood in polytime:

On a given formula $\phi$:

Construct non-deterministically (i.e. simultaneously) all boolean formulas $\psi$ such that

1. $\psi$ is smaller than $\phi$ and
2. $\psi$ contains all variables of $\phi$.

Check all resulting formulas $\psi$ for equivalence with $\phi$. If none is equivalent, ACCEPT, otherwise, REJECT.

Thank you.

Answer 1

The solution proposed seems wrong. Recall that when building a turing machine that uses non-determinism, if any path accepts,

So we cannot ACCEPT if none is equivalent: we can only take ACCEPT decisions from one of the branches of computation, not all of them!

A solution set to the above problem uses that this problem is $\overline{\texttt{NP}}$ : That is, the complement of $\texttt{NP}$, where we can ACCEPT from all branches, and REJECT from one branch.

Answer 2

To the best of our knowledge, the problem MIN-FORMULA is not in NP. The complement of this problem is in NP^SAT, that is a non-deterministic Turing machine with access to a SAT oracle can solve this in polynomial time.

Given input phi, the machine in question would guess a smaller formula psi and then use the SAT oracle to check whether phi and psi are inequivalent (whether there is an assignment on which they disagree). If the outcome of this test is "NO", i.e., they are equivalent, the machine answers "YES" (meaning, the original formula is NOT minimal).

See for instance Sipser's book Example 9.19.