Problem Detail: 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.
Asked By : Jason
Answered By : Kyle Jones
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 all NP-complete problems, and thus all NP 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 $Φ$.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/29482