> - It not only tells you whether the formula is satisfiable or not, but gives you the satisfying values. Any yes/no NP solver can be turned into one that does

> - It not only tells you whether the formula is satisfiable or not, but gives you the satisfying values. Any yes/no NP solver can be turned into one that does this with polynomial overhead. After finding there is a solution, you ask it the similar problem "does this have solution with the first bit set to true?", then "does this have a solution with the first bit set to <answer to previous question> and the second bit set to true?", and so forth until you've identified all bits.