The problem:

Given two boolean formulas in 2-CNF, decide if they are equivalent.

I know that the problem is $\mathsf{coNP}$-hard when at least one formula is in 3-CNF. However, the same proof of $\mathsf{coNP}$-hardness does not apply when both formulas are in 2-CNF.

Conversely, I don't see a straightforward way to show that this problem is in $\mathsf{NP}$.

What is the complexity of the problem? Can this somehow be reduced to (sub)graph isomorphism?


1 Answer 1


I believe the problem is in $P$.

Let $\varphi,\psi$ be the two 2-CNF formulas. The plan of approach will be to test satisfiability of $\varphi \land \neg \psi$ and of $\psi \land \neg \varphi$. If either is satisfiable, then $\varphi,\psi$ are not equivalent; otherwise, they are equivalent.

How do we test satisfiability of $\varphi \land \neg \psi$? Write $\psi = C_1 \land \dots \land C_n$ where $C_i$ are the 2-CNF clauses of $\psi$. $\varphi \land \neg \psi$ is satisfiable iff there exists $i$ such that $\varphi \land \neg C_i$ is satisfiable. Note that $\neg C_i$ is a 2-CNF formula (it is the conjunction of two literals), so $\varphi \land \neg C_i$ is a 2-CNF formula. Therefore, for each $i$, we can test whether $\varphi \land \neg C_i$ is satisfiable, using a standard algorithm to test satisfiability of 2-CNF formulas. If any of those are satisfiable, then so is $\varphi \land \neg \psi$; if not, then $\varphi \land \neg \psi$ is not satisfiable.

Do the same for $\psi \land \neg \varphi$.

The running time is quadratic.

  • $\begingroup$ @rus9384, If you want to know whether it's coNP-hard to prove equivalence of a 2-CNF and 3-CNF formula, I suggest you try to prove that it is coNP-hard (is there a simple reduction from a problem that you already know is coNP-hard?) and try to prove that it is in P (can you adapt the above proof to this case? why or why not?) and see if you can solve it on your own. Actually write down the proof and check each step, don't just guess. If you are still stuck, you can ask a new question and show your work/progress so far. $\endgroup$
    – D.W.
    Mar 8 at 7:14

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.