Complexity of Double-Horn-SAT?
Double-Horn-SAT is polynomial-time solvable.

Given a set of Horn-clauses $X = \{C_1,C_2,...,C_n\}$ and a solution $x_1=b_1,x_2=b_2,...,x_n=b_n$, $b_i \in \{true,false\}$ we can observe that a second solution must differ in at least one variable $x_i$.
So we can run the Horn-SAT algorithm $n$ times on the augmented set $X_i' = X \cup \{ \lnot x_i \}$ if in the first solution $x_i = true$ or on the augmented set $X_i' = X \cup \{ x_i \}$ if in the first solution $x_i = false$. If we find  a solution for one of the $X_i'$ then it is a valid solution for the original set $X$, too and by construction it differs from the first one; otherwise the original set doesn't have a second solution, as can be easily proved by contradiction.

See also the question "Complexity of finding a second solution given a correct solution to an NP-complete problem" on cstheory and Laurent Juban, Dichotomy theorem for the generalized unique satisfiability problem (1999)