[Solved]: 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.