patternMinor
Is boolean formula equivalence problem for 2-CNFs $\mathsf{coNP}$-hard?
Viewed 0 times
problemmathsfconpbooleanhardcnfsforformulaequivalence
Problem
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?
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?
Solution
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.
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.
Context
StackExchange Computer Science Q#166961, answer score: 2
Revisions (0)
No revisions yet.