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