<p>Equisatisfiability can be achieved in the following manner (reduction from 2SAT to HornSAT).  So <span class="math-container">$(p \lor q)$</span> can also be reduced to a Horn formula in this manner.  Thanks to Joshua Gorchow for pointing out this reduction.</p>
<p>Input:  A 2-SAT formula <span class="math-container">$\phi$</span>, with clauses <span class="math-container">$C_1,\dots,C_k$</span> on variables <span class="math-container">$x_1,\dots,x_n$</span>.</p>
<p>Construct a Horn formula <span class="math-container">$Q$</span> as follows:</p>
<p>There will be <span class="math-container">$4\binom n2+ 2n + 1$</span> new variables, one for <strong>every possible</strong>
possible 2-cnf clause on the <span class="math-container">$x$</span> variables with at most 2 literals (<strong>Not
only</strong> the <span class="math-container">$C_i$</span> clauses in <span class="math-container">$\phi$</span>) -- this is including unit clauses and the
empty clause. The new variable corresponding to a clause <span class="math-container">$D$</span> will be
denoted by <span class="math-container">$z_D$</span>.</p>
<p>The <span class="math-container">$4\binom n2$</span> comes from the fact that each pair of <span class="math-container">$(x_i, x_j)$</span>
gives rise to four 2-cnf clauses.
The <span class="math-container">$2n$</span> comes from the fact that each <span class="math-container">$x_i$</span> can create 2 unit clauses.
And finally the &quot;one&quot; comes from the empty clause. So the total
number of possible 2-cnf clauses is <span class="math-container">$4\binom n2+ 2n + 1$</span>.</p>
<p>If a 2-cnf clause <span class="math-container">$F$</span> follows from two other 2-cnf clauses <span class="math-container">$D$</span> and <span class="math-container">$E$</span> by a single
resolution step, then we add the Horn clause
<span class="math-container">$(z_D \land z_E \to z_F)$</span>
to <span class="math-container">$Q$</span>...  Again, we do this for all possible 2-cnf clauses -- all <span class="math-container">$4\binom n2+2n+1$</span> of them --  <strong>not just</strong> the <span class="math-container">$C_i$</span>.</p>
<p>Then we add the unit clauses <span class="math-container">$z_{C_i}$</span> to <span class="math-container">$Q$</span>, for each clause <span class="math-container">$C_i$</span>
appearing in the input <span class="math-container">$\phi$</span>...
Finally, we add the unit clause <span class="math-container">$(\neg z_{empty})$</span> to <span class="math-container">$Q$</span>.</p>
<p>The Horn formula <span class="math-container">$Q$</span> is now complete.  Observe that the variables used in <span class="math-container">$Q$</span> are completely different from those used in <span class="math-container">$\phi$</span>.</p>

CC BY-SA 3.0
2015-04-30T01:27:59.193Z
Is anyone aware of an algorithm in the other direction?  Given a Horn formula $\phi_1$, is there a method to obtain an equivalent 2SAT (2CNF) expression $\phi_2$, so that $\phi_1$ is satisfiable if and only if $\phi_2$ is?  Using the same set of variables, or using extra variables, or using a completely different set of variables (as done in the above answer)?  Or a proof that this is impossible?
Martin Seymour
CC BY-SA 4.0
2020-11-12T14:59:25.770Z
If there was one, it'd be a proof of $NL = P$.
rus9384
CC BY-SA 4.0
2022-08-05T12:58:32.660Z
This reduction is not valid, Q will be satisfied when all Z is false, but if all Z is false then all clause in ϕ is false, thus ϕ is not satisfied but Q is satisfied when all Z is false.
LLL
CC BY-SA 4.0
2023-03-01T16:19:48.557Z
@LLL all $z$-clauses cannot be set to FALSE, because all $z_C$ for $C \in \Phi$ are added as unit clauses to $H$; i.e., they must be satisfied. Then, in combination with the $z_D \wedge z_E \to z_F$ clauses, this could imply many more $z$-variables fixed to TRUE, which could eventually lead to an unsat system.
Jasper
CC BY-SA 4.0
2014-11-20T06:22:47.057Z
2022-08-19T18:31:40.110Z
2022-08-19T18:31:40.110Z
Martin Seymour
<p>No.  Conjunctions of Horn clauses admit least Herbrand models, which disjunctions of positive literals don't.  Cf. <a href="http://books.google.com/books/about/Foundations_of_logic_programming.html?id=P10ZAQAAIAAJ">Lloyd, 1987, <em>Foundations of Logic Programming</em></a>.</p>

<p>Least Herbrand models have the property that they are in the intersections of all satisfiers.  The Herbrand models for $(a \lor b)$ are $\{\{a\}, \{b\}, \{a,b\}\}$, which doesn't contain its intersection, so as arnab says, $(a \lor b)$ is an example of a formula which can't be expressed as a conjunction of Horn clauses.</p>

<p><em>Incorrect answer overwritten</em></p>

CC BY-SA 4.0
2020-11-12T14:57:47.093Z
Clearly there must be a log space (or an even easier one) reduction from 2SAT to HornSAT. If you allow to inver variables.
rus9384
CC BY-SA 2.5
2010-08-19T10:26:39.180Z
@rgrig: No, I was confused. @Evgenij: Answer fixed.
Charles Stewart
CC BY-SA 2.5
2010-08-18T14:52:07.513Z
Clever, but the clause -a_1 & ... & -a_n -> # is not a Horn clause.
Evgenij Thorstensen
CC BY-SA 2.5
2010-08-18T15:50:52.473Z
@Evgenij: It is.
Radu GRIGore
CC BY-SA 2.5
2010-08-18T16:14:52.600Z
A horn clause is a disjunction of literals with at most one positive literal. Translating the above to a disjunction of literals, we get a_1 v ... v a_n, with all the literals positive. The above clause is dual-Horn, but that doesn't help my interest.
Evgenij Thorstensen
CC BY-SA 3.0
2010-08-18T10:46:55.463Z
2011-11-07T20:08:04.943Z
2011-11-07T20:08:04.943Z
Charles Stewart
<p>Is it possible to translate a boolean formula B into an equivalent conjunction of Horn clauses? The Wikipedia article about <a href="http://en.wikipedia.org/wiki/Horn-satisfiability">HornSAT</a> seems to imply that it is, but I have not been able to chase down any reference. </p>

<p>Note that I do not mean "in polynomial time", but rather "at all".</p>

CC BY-SA 2.5
2010-08-19T03:01:59.767Z
The question is still ambiguous. Can you explain what you mean by "project them out"? Do you mean "assignment A satisfies the SAT instance F iff there is an assignment B to auxiliary variables such that (A,B) satisfies the HornSAT instance F'"? If so, then I think you can do it by simply using the P-completeness of HornSAT.
Ryan Williams
CC BY-SA 2.5
2010-08-18T00:17:28.333Z
What do you mean by "translate"?  It's obvious there are SAT instances that cannot be written as a HornSAT formula.  For instance, the clause (p or q).  But perhaps you mean that you want a reduction such that the input SAT formula is satisfiable iff the output HornSAT formula is satisfiable?  In that case of course, there's the trivial reduction since you don't care for efficiency...
arnab
CC BY-SA 2.5
2010-08-18T01:14:29.670Z
I do not mean equisatisfiable, since that is indeed trivial without restrictions on efficiency. I mean equivalent as in "have the same satisfying assignments" when we consider the variables common to both the SAT instance and the corresponding HornSAT instance (if we had to add some auxiliary variables, we project them out). I agree that it shouldn't be possible, exactly for the example (P v Q), but I do not know how to prove it. Do you have a proof sketch in mind?
Evgenij Thorstensen
<reference-request><lo.logic><sat>
Translating SAT to HornSAT
Evgenij Thorstensen
# Translating SAT to HornSAT

(Asked by: username_0 on 2010-08-17)

Is it possible to translate a boolean formula B into an equivalent conjunction of Horn clauses? The Wikipedia article about [HornSAT](http://en.wikipedia.org/wiki/Horn-satisfiability) seems to imply that it is, but I have not been able to chase down any reference.

Note that I do not mean "in polynomial time", but rather "at all".

**Tags:** reference-request, lo.logic, sat

> **Comments:**
> **username_2**: What do you mean by "translate"?  It's obvious there are SAT instances that cannot be written as a HornSAT formula.  For instance, the clause (p or q).  But perhaps you mean that you want a reduction such that the input SAT formula is satisfiable iff the output HornSAT formula is satisfiable?  In that case of course, there's the trivial reduction since you don't care for efficiency...  
> **username_0**: I do not mean equisatisfiable, since that is indeed trivial without restrictions on efficiency. I mean equivalent as in "have the same satisfying assignments" when we consider the variables common to both the SAT instance and the corresponding HornSAT instance (if we had to add some auxiliary variables, we project them out). I agree that it shouldn't be possible, exactly for the example (P v Q), but I do not know how to prove it. Do you have a proof sketch in mind?  
> **username_1**: The question is still ambiguous. Can you explain what you mean by "project them out"? Do you mean "assignment A satisfies the SAT instance F iff there is an assignment B to auxiliary variables such that (A,B) satisfies the HornSAT instance F'"? If so, then I think you can do it by simply using the P-completeness of HornSAT.  

---

## 2 answers

### Answer by username_7 on 2010-08-18. Score: 28 | Accepted answer

No. Conjunctions of Horn clauses admit least Herbrand models, which disjunctions of positive literals don't. Cf. [Lloyd, 1987, *Foundations of Logic Programming*](http://books.google.com/books/about/Foundations_of_logic_programming.html?id=P10ZAQAAIAAJ).

Least Herbrand models have the property that they are in the intersections of all satisfiers. The Herbrand models for $(a \lor b)$ are $\{\{a\}, \{b\}, \{a,b\}\}$, which doesn't contain its intersection, so as username_2 says, $(a \lor b)$ is an example of a formula which can't be expressed as a conjunction of Horn clauses.

*Incorrect answer overwritten*

> **Comments:**
> **username_0**: Clever, but the clause -a_1 & ... & -a_n -> # is not a Horn clause.  
> **username_8**: @Evgenij: It is.  
> **username_0**: A horn clause is a disjunction of literals with at most one positive literal. Translating the above to a disjunction of literals, we get a_1 v ... v a_n, with all the literals positive. The above clause is dual-Horn, but that doesn't help my interest.  
> **username_7**: @rgrig: No, I was confused. @Evgenij: Answer fixed.  
> **username_4**: Clearly there must be a log space (or an even easier one) reduction from 2SAT to HornSAT. If you allow to inver variables.  

---

### Answer by username_3 on 2014-11-20. Score: 10

Equisatisfiability can be achieved in the following manner (reduction from 2SAT to HornSAT). So $(p \lor q)$ can also be reduced to a Horn formula in this manner. Thanks to Joshua Gorchow for pointing out this reduction.

Input: A 2-SAT formula $\phi$, with clauses $C\_1,\dots,C\_k$ on variables $x\_1,\dots,x\_n$.

Construct a Horn formula $Q$ as follows:

There will be $4\binom n2+ 2n + 1$ new variables, one for **every possible**
possible 2-cnf clause on the $x$ variables with at most 2 literals (**Not
only** the $C\_i$ clauses in $\phi$) -- this is including unit clauses and the
empty clause. The new variable corresponding to a clause $D$ will be
denoted by $z\_D$.

The $4\binom n2$ comes from the fact that each pair of $(x\_i, x\_j)$
gives rise to four 2-cnf clauses.
The $2n$ comes from the fact that each $x\_i$ can create 2 unit clauses.
And finally the "one" comes from the empty clause. So the total
number of possible 2-cnf clauses is $4\binom n2+ 2n + 1$.

If a 2-cnf clause $F$ follows from two other 2-cnf clauses $D$ and $E$ by a single
resolution step, then we add the Horn clause
$(z\_D \land z\_E \to z\_F)$
to $Q$... Again, we do this for all possible 2-cnf clauses -- all $4\binom n2+2n+1$ of them -- **not just** the $C\_i$.

Then we add the unit clauses $z\_{C\_i}$ to $Q$, for each clause $C\_i$
appearing in the input $\phi$...
Finally, we add the unit clause $(\neg z\_{empty})$ to $Q$.

The Horn formula $Q$ is now complete. Observe that the variables used in $Q$ are completely different from those used in $\phi$.

> **Comments:**
> **username_3**: Is anyone aware of an algorithm in the other direction?  Given a Horn formula $\phi_1$, is there a method to obtain an equivalent 2SAT (2CNF) expression $\phi_2$, so that $\phi_1$ is satisfiable if and only if $\phi_2$ is?  Using the same set of variables, or using extra variables, or using a completely different set of variables (as done in the above answer)?  Or a proof that this is impossible?  
> **username_4**: If there was one, it'd be a proof of $NL = P$.  
> **username_5**: This reduction is not valid, Q will be satisfied when all Z is false, but if all Z is false then all clause in ϕ is false, thus ϕ is not satisfied but Q is satisfied when all Z is false.  
> **username_6**: @username_5 all $z$-clauses cannot be set to FALSE, because all $z_C$ for $C \in \Phi$ are added as unit clauses to $H$; i.e., they must be satisfied. Then, in combination with the $z_D \wedge z_E \to z_F$ clauses, this could imply many more $z$-variables fixed to TRUE, which could eventually lead to an unsat system.  

---

