# Does exist any horn formula that is equisatisfiable to the clause that is disjunction of two literals? Does also exist equivalent?

I just and simply want to know if whether or not exist any horn formula that is equisatisfiable to $(p\lor q)$. I would also be interested to know if there also exists equivalent.

• What do you mean by $p \lor q$? Are $p,q$ variables? Are they something else? As you can see below, this has caused some confusion in the answers. Can you edit your question to clarify? – D.W. Jan 2 '18 at 0:23
• – xskxzr Mar 3 '18 at 3:29

The answer is no: this is not possible. I assume a horn formula is a CNF formula with at most one positive literal (=nonnegated variable) in each clause. Now, for the sake of contradiction, suppose we have a horn formula $\phi$ that is equisatisfiable to $p\vee q$. Since $\phi$ is a horn formula, each clause in it contains a negative literal OR there is a clause consisting of only one (positive) variable. If the latter is the case, that positive variable must be a helper variable, since if it were p, it would mean that p must be necessarily true for satisfaction, which is not the case in "$p\vee q$" (same argument for q). So in this case, we derive an equisatisfiable formula by replacing that variable with true. In this new formula, we have one less clause that contains only a positive variable. We repeat this process until this is no longer the case, until we have a formula that has a negative literal in each clause. But such a formula is satisfiable by setting every variable to false. However, that's not the case in $p\vee q$, hence the contradiction.

A simpler argument is the following:

Any horn formula $H$ has a minimal model $\mathcal{A}$, i.e. a model for $H$ such that for any other model $\mathcal{A}'$ of $H$ and any atomic formula $A$ we have $\mathcal{A}(A) \leq \mathcal{A}'(A)$ (where for any model $\mathcal{B}$ we define $\mathcal{B}(A) = 0$ iff $\mathcal{B}(A)$ is false and $\mathcal{B}(A) = 1$ iff $\mathcal{B}(A)$ is true and of course $0 < 1$). This fact follows immediately from the usual linear time algorithm for the satisfiability of horn clauses, since this algorithm computes such a model.

Now, the formula $\varphi = A \lor B$ has three models, $(A = 1, B = 1)$, $(A = 1, B = 0)$ and $(A = 0,B= 1)$. None of this models is minimal. Hence the formula $\varphi$ cannot be a horn clause (or equisatisfiable to a horn clause)

If $p,q$ are atomic then the answer is trivial. I'll assume otherwise below.

Any Horn formula is satisfiable: $a_1 \land \cdots \land a_n \rightarrow b$ can be satisfied letting $b$ to be true.

$p\lor q$ is not necessarily satisfiable, so no Horn clause can be equisatisfiable with it, in general.

• I think p and q are supposed to be atomic and how is that trivial? Didn't you misread "satisfiable" for "equisatisfiable"? – Albert Hendriks Jan 1 '18 at 13:09
• @AlbertHendriks If $p,q$ are atomic, then $p\lor q$ is satisfiable (take $p$ to be true), so it is equisatisfiable with $true$, or the Horn formula $p \rightarrow p$, or any tautology which is a Horn formula. Isn't that trivial? – chi Jan 1 '18 at 13:20
• Well, technically that's true. I guess OP needs to word his question better. I assume there are other clauses in his original formula that may contain p and or q and he only wants to replace the mentioned part with equisatisfiable horn clauses without affecting the satisfiability of the whole formula. – Albert Hendriks Jan 1 '18 at 13:34
• @AlbertHendriks That would completely change the question. The OP asked about an equisatisfiable with $p\lor q$, not $F(p\lor q)$, and I think my answer covers why that can not be in Horn form, in general. – chi Jan 1 '18 at 13:54