Complexity of deciding if a formula has exactly 1 satisfying assignment
Your problem is known as the $\text{UNIQUE-SAT}$ problem which is $\mathsf{US}$-complete. The problem is in $\mathsf{D^p}$ but not known to be $\mathsf{D^p}$-hard under deterministic polynomial time reductions, where the class $\mathsf{D^p} = \{ L_1 \cap \overline{L_2} \mid L_1,L_2 \in \mathsf{NP} \}$. 

It was shown by Papadimitriou and Yannakis [1] that the set of uniquely satisfiable formulas is contained in $\mathsf{D^p}$. This follows by the definition of $\mathsf{D^p}$: let $L_1$ be SAT, and let $L_2$ be the set of formulas with $2$ or more satisfying assignments. Regarding $\mathsf{D^p}$-hardness of $\text{UNIQUE-SAT}$, Blass and Gurevich [2] gave a partial answer. For one, they showed a non-relativizing proof technique would be needed to settle the question. However, Valiant and Vazirani [3] gave a randomized polynomial time reduction from $\text{SAT}$ showing $\mathsf{D^p}$-hardness of $\text{UNIQUE-SAT}$ under randomized polynomial time reductions .

When it is known that the problem has at most one assignment or no assignments, the promise problem is called $\text{UNAMBIGUOUS-SAT}$. The Valiant–Vazirani theorem states that if there is a polynomial time algorithm for $\text{UNAMBIGUOUS-SAT}$, then $\mathsf{NP}=\mathsf{RP}$. To prove their theorem they showed that the promise problem $\text{UNAMBIGUOUS-SAT}$ is $\mathsf{NP}$-hard under randomized polynomial time reductions. A corollary that follows from the Valiant–Vazirani theorem is that $\text{UNIQUE-SAT}$ is complete for $\mathsf{D^p}$ under randomized polynomial time reductions.



[1] Papadimitriou, Christos H., and Mihalis Yannakakis. "The complexity of facets (and some facets of complexity)." Proceedings of the fourteenth annual ACM symposium on Theory of computing. ACM, 1982.

[2] Blass, Andreas, and Yuri Gurevich. "On the unique satisfiability problem." Information and Control 55.1 (1982): 80-88.

[3] Valiant, Leslie G., and Vijay V. Vazirani. "NP is as easy as detecting unique solutions." Theoretical Computer Science 47 (1986): 85-93.