Consider the decision problem:

MIN-EQ-CNF= $\{\langle\phi, k\rangle |\exists \text{CNF formula } \psi \text{ of size }\leq k\text{ that is equivalent to the CNF formula }\phi\}$

CNF is a Boolean formula that is an AND of ORs and we say that two formulas are equivalent if they agree on all possible assignments. This problem is complete for the second level of polynomial hierarchy ${\Sigma^P_2}$.

Now lets consider a similar problem:

MIN-EQ-3-CNF= $\{\langle\phi' , k\rangle | \exists \text{3-CNF formula } \psi' \text{of size }\leq k\text{ that is equivalent to the CNF formula } \phi'\}$. In other words, given a 3SAT instance $\phi'$, is there a 3SAT formula $\psi'$ of size $\leq k$ that is equivalent to $\phi'$?

Query: What is the computational complexity of this restricted MIN-EQ-3-CNF?

Note: I am unclear how the size is defined in MIN-EQ-CNF. Thus, I am assuming the size of the formula is the number of clauses in MIN-EQ-CNF. Please correct this is incorrect. Similarly, in MIN-EQ-3-CNF we define the size as the number of clauses in the formula.

  • $\begingroup$ Thank you. I understand. The limitation of 3 literals per clause is what is bothering me. Is the restricted problem still complete for ${\Sigma^P_2}$ or is it simpler? Most texts talk about the general version. $\endgroup$
    – J.Doe
    Commented Oct 25, 2021 at 18:55
  • $\begingroup$ and what is the formal definition of size: number of clauses or something else? $\endgroup$
    – J.Doe
    Commented Oct 25, 2021 at 18:59
  • 1
    $\begingroup$ A small observation: in P^(NP) we can find a 3cnf G with a maximum number of clauses equivalent to a given F, if any 3cnf is equivalent to F: for each of the O(n^3) possible clauses C, if F is equivalent to (F AND C) then add C to G. This takes O(n^3) calls to SAT (in fact we could ask the queries in parallel). This adds every 3cnf clause consistent with F. (We could test with one more SAT query if F is equivalent to G.) Another consequence is it "suffices" to solve: given a 3cnf G, find a minimum subset of clauses G' equivalent to G. If this is in P^NP then the original problem is in P^NP... $\endgroup$ Commented Oct 26, 2021 at 3:39


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.