Equivalence of Horn formulas tractable?

Question

Assume I have two Horn formulas $\phi_1, \phi_2$. Horn formulas are CNF formulas so that each clause has at most one unnegated literal. For example:

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

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

Is this problem tractable?

Answer 1

Yes, you can check equivalence in polynomial time (in fact, in quadratic time).

By similar logic to my answer to your previous question, it suffices to test satisfiability of $\phi_1 \land \neg c$ where $c$ ranges over the clauses of $\phi_2$. If any of these are satisfiable, then $\phi_1,\phi_2$ are inequivalent. Otherwise, if they're all unsatisfiable, and the same for $\phi_2 \land \neg c'$ where $c'$ ranges over all clauses of $\phi_1$, then $\phi_1,\phi_2$ are equivalent.

So, let's investigate how to test satisfiability of $\phi_1 \land \neg c$ where $c$ is a clause of $\phi_2$. By assumption, $c$ is a Horn clause, so it has the form $\neg x_1 \lor \dots \lor \neg x_k \lor x_{k+1}$. So, $\phi_1 \land \neg c$ has the form

$$\phi_1 \land x_1 \land \dots \land x_k \land \neg x_{k+1}.$$

This turns out to be a Horn formula, so you can its test satisfiability with the standard algorithm for testing satisfiability of Horn formula. This takes linear time per clause, and there are linearly many clauses, so the total running time is quadratic.