Equivalence of Krom formulas tractable?

Question

Assume I have two Krom formulas $\psi_1, \psi_2$. Krom formulas are propositional formulas in CNF that have 2 literals in every clause. Each literal can be negated or unnegated. In other words, $\psi_1,\psi_2$ are 2-CNF formulas. For instance:

$(x_1 \vee \neg x_2) \land (\neg x_2 \vee x_3 ) \land (x_3 \vee x_4)$

I want to decide whether $\psi_1,\psi_2$ are logically equivalent, i.e., $\psi_1 \leftrightarrow \psi_2$. Equivalently, I want to test whether $F=(\psi_1 \vee \neg\psi_2)\wedge (\neg \psi_1 \vee \psi_2)$ is true for all assignments of $x_1,\dots,x_n$.

Is this problem tractable?

Answer 1

Yes, equivalence can be checked in polynomial time (in fact, in quadratic time).

I will describe how to test whether $\psi_1 \lor \neg \psi_2$ is true for all assignments. You can do the same for $\neg \psi_1 \lor \psi_2$, and use this to test whether $F$ is a tautology, i.e., whether $\psi_1,\psi_2$ are logically equivalent.

I will do this by checking whether $\psi_1 \lor \neg \psi_2$ is false for any assignment, or in other words, whether $\neg(\psi_1 \lor \neg \psi_2)$ is satisfiable. Notice that

$$\neg(\psi_1 \lor \neg \psi_2) = \neg \psi_1 \land \psi_2,$$

so it suffices to test satisfiability of $\neg \psi_1 \land \psi_2$ where $\psi_1,\psi_2$ are Krom (2-CNF) formulas.

Suppose that $\psi_1 = c_1 \land \cdots \land c_k$ where $c_i$ is the $i$th clause in $\psi_1$. Then

$$\neg \psi_1 = (\neg c_1) \lor \cdots \lor (\neg c_k).$$

Therefore

$$\begin{align*} \neg \psi_1 \land \psi_2 &= ((\neg c_1) \lor \cdots \lor (\neg c_k)) \land \psi_2\\ &= (\neg c_1 \land \psi_2) \lor \cdots \lor (\neg c_k \land \psi_2). \end{align*}$$

Now, $\neg \psi_1 \land \psi_2$ is satisfiable iff $\neg c_i \land \psi_2$ is satisfiable for some $i$. So, we can iterate over $i$ and test satisfiability of each $\neg c_i \land \psi_2$; if any of them are satisfiable, then $\neg \psi_1 \lor \psi_2$ is satisfiable and $F$ is not a tautology and $\psi_1,\psi_2$ are not logically equivalent.

How to test satisfiability of $\neg c_i \land \psi_2$? Well, $c_i$ has the form $(\ell_1 \lor \ell_2)$ where $\ell_1,\ell_2$ are two literals, so $\neg c_i \land \psi_2$ has the form $\neg \ell_1 \land \neg \ell_2 \land \psi_2$. This is also a Krom (2-CNF) formula, so you can test its satisfiability using the standard polynomial-time algorithm. You do a linear number of such tests, so the total running time is polynomial. In fact, it is quadratic, as testing satisfiability can be done in linear time.

Answer 2

Recall 2-SAT solution which uses strongly connected components: we build a graph with vertices $x_1,\ldots,x_n, \lnot x_1, \ldots, \lnot x_n$, and we replace each clause $x_i \lor x_j$ with edges $\lnot x_i \to x_j$ and $\lnot x_j \to x_i$. An example from here:

To satisfy the formula, it's necessary and sufficient to assign vertices so that there are no contradictions in the graph (no edge $true \to false$). We'll use these graphs for equivalence checking.

1. We build these graphs $G_1$ and $G_2$ for both formulas $F_1$ and $F_2$.
2. If there is a cycle $x_i \leadsto \lnot x_i \leadsto x_i$ in a graph, then its formula has no solutions. We check that both formulas are solvable/unsolvable.
3. If there exists a path of form $x_i \leadsto \lnot x_i$ (similarly for the case $\lnot x_i \leadsto x_i$), we know that to satisfy the formula we must select $x_i$ to be false (otherwise we have a contradiction). We remember this choice. Using the graph, we can assign values to all vertices reachable from $\lnot x_i$ (they must be true). Again, check that both formulas made exactly the same decisions in the end.
4. Remove all edges to/from all known vertices from the graphs.
5. Now, $F_1$ and $F_2$ are equivalent $\iff$ the remaining graphs are equivalent in the following sense: for any $v_1,v_2$ path $v_1 \leadsto v_2$ exists in $G_1$ iff it exists in $G_2$. This can be checked in at most $O(|V|\cdot|E|)$ time (just run DFS from each vertex and check that it has visited the same vertices for both graphs). Maybe it can be done faster.

Proof:

$\Leftarrow$: evident, since after transitive closure of graphs we'll have the same implications in both formulas.

$\Rightarrow$: By contradiction. Wlog we assume that there exists a path $v_1 \leadsto v_2$ in $G_1$ which doesn't exist in $G_2$. It means that assignment $v_1 := true$, $v_2 := false$ is feasible in $F_2$ (since there is no path $v_1 \leadsto v_2$) but is infeasible in $F_1$.

Namely, the following assignment satisfies $F_2$:

• $true$ for all vertices reachable from $v_1$.
• $false$ from all vertices which can reach $v_2$.
• Remove all known vertices (mentioned above and their complements) from the graph. All remaining vertices create connected components. We color connected components in $true$, and connected components corresponding to their complements - in $false$ (see note below).

This assignment has no contradiction, since there can be no edge $u \to v$ of form $true \to false$:

• If $u$ belongs to a component which was full colored $true$, then such $v$ must also be true.
• Otherwise, it means that $u$ is reachable from $v_1$, and therefore $v$ is also reachable from $v_1$ and must be true. $\blacksquare$

Technical note: for each variable $x_i$ there are two vertices: $v_i$ and $\lnot v_i$ - and one may wonder if it'll lead to some problems with assignments. The answer is that after step 4), $v_i$ and $\lnot v_i$ will lie in two different components (moreover, they are symmetric: $u \to v$ in one component means $\lnot u \to \lnot v$ in another one). Therefore, whatever decision we make for $u$ in one component, we can make the opposite decision for $\lnot u$ in another one.