# Is boolean formula equivalence problem for 2-CNFs $\mathsf{coNP}$-hard?

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?

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$$.