Is the set of satisfiable Horn formulas sparse?
A sparse language contains a polynomially bounded number of srings at every length.
No. Fix a $k$, and let $x_1, x_2, ..., x_k$ be the variables in your Horn formula. Then for all $i$ the clause $(x_i)$ is a Horn clause – there is at most one positive literal. Using such clauses, you can construct $2^k - 1$ different Horn formulas: $(x_1)$; $(x_2)$; $(x_1) \wedge (x_2)$; $(x_3)$; etc. Each of these is trivially satisfiable – just set $x_i = 1$ for all $i$. The length of each formula is $O(k \log k)$, assuming any reasonable encoding.
(You can add extra requirements like "all clauses must contain at least one negative literal", "all variables must occur in at least one clause", etc., but this doesn't really change anything; just tweak the above construction slightly.)