Some sources state that an algorithm that solves the SAT problem not only needs to decide whether a given existentially-quantified formula is satisfiable or not, but, additionally, in the case where the formula is satisfiable, it does need to provide a satisfying assignment. Is this true or not?
I am bit confused, since I thought the SAT problem would just be an existential question.
The SAT problem is a decision problem. It means that an algorithm that solves SAT must answer true or false, and not necessarily find a satisfying assignment.
However, as many decision problems, there is a functional problem associated to SAT, that asks to find a satisfying assignment when there exists one.
There is a polynomial time reduction from the functional problem to the decision problem. Check here to see what it looks like.
If you have variables x1 to xn, and you decide in polynomial time whether the problem can be satisfied or not, then if it can be satisfied, you set x1 = true and check if it can still be satisfied. If not you set x1 = false, which can be satisfied.
Then you set x2 = true, and if that cannot be satisfied you set x2 = false. And so on, and so on. So if SAT could be solved in polynomial time, you could find a solution in polynomial time quite easily. A similar approach could be used for TSP, for example.
