I have been struggling with the understanding of why this problem is in coNP.


CNF-Equivalence, denoted as C, takes as input a pair of CNF formulas ($\phi, \sigma$) both are defined over the same set of $n$ variables $x = (x_{1}, x_{2}, ... x_{n})$. The goal is to decide whether these two formulas are equivalent, which means they compute the same output for every $x$. Is this problem in P, NP or coNP?


Deciding whether this problem is in NP or coNP. In order to verify the equivalence I have a verifier $V$ which takes as input a certificate $c$ which in our case is an assignment of $x$. The verifier will then run the assignment on both formulas $\phi$ and $\sigma$ and compare the outputs.


In this case we need to check for all certificates for a given $x$


In this case we will be checking for certificates until we find one for which the output is different.

Maybe I got the certificate system wrong, but with such system in place both of the problems seem equally hard to me ...

  • 1
    $\begingroup$ These problems seem equally hard if you are looking for a deterministic machine to solve the problem, but one is easier with a non-deterministic machine. You should look at your definition of NP and coNP again (or provide the definition you have in your post, if you want to have a more detailed explanation). $\endgroup$
    – Rémi
    Commented Dec 13, 2023 at 14:33
  • $\begingroup$ The problem is for sure in co-NP and a certificate is an assignment $x$ for which $\phi(x) \neq \sigma(x)$. It is unknown whether the problem is in $P$ or in $NP$. $\endgroup$
    – Steven
    Commented Dec 13, 2023 at 14:40

2 Answers 2



In this case we will be checking for certificates until we find one for which the output is different.

To show that the formulas are not equivalent, it suffices to show just a single certificate $c$ for which $\phi(X\vert c)\neq\sigma(X\vert c)$. Clearly, checking a single certificate is possible in polynomial time.

On the other hand, it does not seem that there always is some short single certificate to show equivalence, because you'd need to show it for exponentially many possible assignments.

  • $\begingroup$ Ohh I see, thanks for the simple answer :) $\endgroup$
    – Meki21
    Commented Dec 13, 2023 at 14:48

The question is about CNF-equivalence. This answer, however, chiefly is about CNF-not-equivalence, the complement problem of CNF equivalence. Two formulas $(\phi, \sigma)$ are not-equivalent if they differ on at least one assignment (i.e. if they are not equivalent). In this answer, we will see that CNF-not-equivalence is NP-complete (i.e. in NP and NP-hard). Therefore, we will know that CNF-equivalence is co-NP-complete.

So, the rest of this answer focuses on CNF-not-equivalence. We know that SAT is in NP (even NP-complete). We reduce from it to CNF-not-equivalence, and reduce back:

Reducing CNF-not-equivalence to SAT:

Given two formulas $(\phi, \sigma)$, construct the formula $\neg (\phi \iff \sigma)$ as a CNF, using the reduction from SAT for arbitrary formulas to CNF-SAT, also known as the Tseytin transformation. If this formula is SAT, then we found a counterexample and thus the input formulas are not equivalent.

Reducing SAT to CNF-not-equivalence (for NP-hardness):

Given a formula $\sigma$, we compare it to the always-false formula. We then know that $\sigma$ is satisfiable precisely when it is not equal to $\bot$.

Thus CNF-not-equivalence is in NP, since it is solvable by SAT. The backward direction establishes it is NP-hard, thus it even is NP-complete.

  • $\begingroup$ Here is the issue with your answer. The problem, in its full form is formalized as $\forall X:\phi(X)=\sigma(X)$. The formula $\neg(\phi\iff\sigma)$ therefore would be formalized as $\forall X:\neg(\phi(X)\iff\sigma(X))$. That's actually the negation of the original problem, though you could have $\not\exists:\neg(\phi(X)\iff\sigma(X))$ but since there is a negation in the quantifier part of the formula, you can't trivially apply Tseytin transformation. $\endgroup$
    – rus9384
    Commented Dec 13, 2023 at 17:20
  • $\begingroup$ @rus9384 I can't follow. Yes, in my answer, I analyze the problem that is the complement of the one given in the question. I clearly state this in the answer. $\endgroup$ Commented Dec 13, 2023 at 18:18
  • $\begingroup$ When you state $\neg(\phi\iff\sigma)$, that formula actually is translated into English as "Does there exist such an assignment that the two formulas are unequal?" Whereas the original problem asks an opposite statement: "Are the formulas equal on every assignment?" Or, equivalently, "Does there not exist such an assignment that the two formulas are unequal?" $\endgroup$
    – rus9384
    Commented Dec 13, 2023 at 18:20
  • $\begingroup$ Yes. Hence why the original problem from the question is in coNP, while SAT is in NP. That's where the missing negation went--into the "co".. didn't it? $\endgroup$ Commented Dec 13, 2023 at 18:24
  • 2
    $\begingroup$ That's fine now. $\endgroup$
    – rus9384
    Commented Dec 13, 2023 at 18:31

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.