0
$\begingroup$

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?

$\endgroup$
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.