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.