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?

  • 1
    $\begingroup$ Nice question! You're asking two separate questions here. We prefer that you post them separately, so that if one is answered and the other isn't, the latter gets treated as an unanswered question. I've edited this to ask about the case of Krom formulas. I encourage you to post your question about equivalence of Horn formulas as a separate question. $\endgroup$
    – D.W.
    Jul 16, 2020 at 18:24
  • 1
    $\begingroup$ I created a second question here: cs.stackexchange.com/q/128423/755 $\endgroup$
    – D.W.
    Jul 16, 2020 at 19:14

2 Answers 2


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


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

  • $\begingroup$ Nice answer and also easy to understand! $\endgroup$
    – Pepe
    Jul 16, 2020 at 20:55

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:

enter image description 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.


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

  • 1
    $\begingroup$ Very interesting and clever! Can you provide a more detailed justification of the claim that $v_1 := \text{true}, v_2 := \text{false}$ is feasible in $F_2$? That is not obvious to me. Sure, there is no path $v_1 \leadsto v_2$, but how does that imply that such an assignment is feasible? (You must be relying on the fact that steps 2,3 were done somehow, but I don't see them show up in your argument explicitly, so some steps seem to have been glossed over.) $\endgroup$
    – D.W.
    Jul 16, 2020 at 19:08
  • $\begingroup$ Indeed, very interesting idea since I was also thinking about involving the 2-SAT algorithm that involves graphs but couldn't figure out on how to make it work. It would be great if you can also provide the answer to D.W.'s comment. $\endgroup$
    – Pepe
    Jul 16, 2020 at 20:52
  • $\begingroup$ @D.W., thanks for the comment, I hope it's clearer now. $\endgroup$
    – user114966
    Jul 16, 2020 at 21:47
  • $\begingroup$ Very nice, thank you for the detailed explanation! That makes sense. $\endgroup$
    – D.W.
    Jul 16, 2020 at 22:05
  • $\begingroup$ @D.W., actually, there is a bug in this reasoning, let me fix it $\endgroup$
    – user114966
    Jul 16, 2020 at 22:07

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.