# Equivalence of Horn formulas tractable?

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?

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