Equivalence of Krom formulas tractable?

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.

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.