Equivalence of Krom formulas tractable?
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.

We build these graphs $G_1$ and $G_2$ for both formulas $F_1$ and $F_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.
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.
Remove all edges to/from all known vertices from the graphs.
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.