No, the GP is correct. If you use SAT to solve Sudoku, you have reduced Sudoku to SAT, not the other way around. That is, you've shown that an oracle that solv

No, the GP is correct. If you use SAT to solve Sudoku, you have reduced Sudoku to SAT, not the other way around. That is, you've shown that an oracle that solves any SAT problem in constant time can solve any Sudoku in polynomial time. The more difficult side is to show that for any SAT instance, you can reduce it to a Sudoku. Really proving that you can use SAT to solve Sudoku is not a great or interesting result; since Sudoku is a decision problem it is very clear that it is in NP. Or see that verifying that a Sudoku solution is correct is achievable in polynomial time.