Verifying unique solutions of SAT Consider the following problem: given a CNF formula and an assignment that satisfies this formula, is there another satisfying assignment for this formula ?

What is the complexity of this problem ? (It most surely is in NP, but is it also NP-hard ?)

What if you are not given the assignment and you just want do decide whether the formula has a unique satisfying assignment ?

Thanks.
The problem of deciding whether a given CNF formula has a satisfying assignment other than a given one is easily shown to be NP-complete by transforming a CNF formula to add one trivial solution.  This problem is called the “Another Solution Problem (ASP) of SAT” in [YS03], where it is used to give a systematic proof that (the decision versions of) the ASPs of many other problems are also NP-complete.

The problem of deciding whether a given CNF formula has a unique satisfying assignment or not (so you have to answer “no” if the formula has no satisfying assignments or more than one satisfying assignment) is US-complete.  US contains both UP and coNP.

References

[YS03] Takayuki Yato and Takahiro Seta. Complexity and completeness of finding another solution and its application to puzzles. IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, E86-A(5):1052–1060, May 2003.

Edit: An earlier version (revision 1) of this answer contained a confusion between the decision version and the search version.  It has been fixed.