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

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.

• Short answer: the problem of finding a satisfying assignment is computationally as hard as deciding if one exists. The idea is that given an algorithm which decides satisfiability it can be used to efficiently construct a satisfying assignment. Check out en.wikipedia.org/wiki/… Aug 28, 2014 at 20:46
• I thought UNSAT was coNP-complete? Aug 29, 2014 at 14:09

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 $$Φ$$.