Is it possible to translate a boolean formula B into an equivalent conjunction of Horn clauses? The Wikipedia article about HornSAT 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".

  • 2
    $\begingroup$ 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... $\endgroup$
    – arnab
    Aug 18, 2010 at 0:17
  • $\begingroup$ 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? $\endgroup$ Aug 18, 2010 at 1:14
  • 3
    $\begingroup$ 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. $\endgroup$ Aug 19, 2010 at 3:01

3 Answers 3


No. Conjunctions of Horn clauses admit least Herbrand models, which disjunctions of positive literals don't. Cf. Lloyd, 1987, Foundations of Logic Programming.

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.

Incorrect answer overwritten

  • $\begingroup$ Clever, but the clause -a_1 & ... & -a_n -> # is not a Horn clause. $\endgroup$ Aug 18, 2010 at 14:52
  • $\begingroup$ @Evgenij: It is. $\endgroup$ Aug 18, 2010 at 15:50
  • 5
    $\begingroup$ 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. $\endgroup$ Aug 18, 2010 at 16:14
  • $\begingroup$ @rgrig: No, I was confused. @Evgenij: Answer fixed. $\endgroup$ Aug 19, 2010 at 10:26
  • $\begingroup$ Clearly there must be a log space (or an even easier one) reduction from 2SAT to HornSAT. If you allow to inver variables. $\endgroup$
    – rus9384
    Nov 12, 2020 at 14:57

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

  • $\begingroup$ 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? $\endgroup$ Apr 30, 2015 at 1:27
  • 1
    $\begingroup$ If there was one, it'd be a proof of $NL = P$. $\endgroup$
    – rus9384
    Nov 12, 2020 at 14:59
  • $\begingroup$ 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. $\endgroup$
    – LLL
    Aug 5, 2022 at 12:58
  • $\begingroup$ @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. $\endgroup$
    – Jasper
    Mar 1, 2023 at 16:19

I don't think it's possible. There's no way, for example, to write $\phi = (X_1 \vee X_2 \vee \neg X_3 \vee \neg X_4)$ as a conjunction of horn clauses since $\phi$ only outlaws a single truth assignment, namely 0011. Any horn clause with less than 4 literals would outlaw more than 1 truth assignment, and horn clauses with 4 literals can only outlaw truth assignments with at most one 0.

Edit: oops didn't notice this was answered already


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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