Is finding a solution of a satisfiability problem harder than deciding satisfiability?

Question

Is the problem of determining whether or not a given Boolean expression is satisfiable computationally distinct from actually finding a solution to the expression?

In other words, is there another way of finding that a given expression is satisfiable without explicitly determining the 'right settings' for the Boolean variables? Or do all possible proofs reduce in polynomial time to the 'right settings'?

Forgive my ignorance, I am only an engineering student. Wikipedia seems to imply that the act of just finding SAT or UNSAT is NP-complete.

Answer 1

As mentioned in a comment, any method of determining satisfiability of a Boolean formula can be easily converted into a method for finding the satisfying variable assignment. This is because Boolean satisfiability problems are downward self-reducible.

From Wikipedia:

Self-reducibility

The SAT problem is self-reducible, that is, each algorithm which correctly answers if an instance of SAT is solvable can be used to find a satisfying assignment. First, the question is asked on the given formula $Φ$. If the answer is "no", the formula is unsatisfiable. Otherwise, the question is asked on the partly instantiated formula $Φ$$\{x_1=TRUE\}$, i.e. $Φ$ with the first variable $x_1$ replaced by $TRUE$, and simplified accordingly. If the answer is "yes", then $x_1=TRUE$, otherwise $x_1=FALSE$. Values of other variables can be found subsequently in the same way. In total, $n+1$ runs of the algorithm are required, where $n$ is the number of distinct variables in $Φ$.

Answer 2

The correct answer is that the determining if a solution exists and determining a solution are computationally distinct. Not all methods for determining if a solution exists can produce a solution. There exists a solution to the Hamiltonian Path problem that can determine if a path exists but cannot produce any such path. That said the question is made moot by arxiv.org/abs/cs/0205064.