>The following does not quite show it can't happen but it does give one pause: an old result of Levin's shows that there is a program you could write NOW such that if P=NP then this program decides SAT except for a finite number of formulas (all of which are NOT in SAT) and can be proven to work in poly time (I will later give three pointers to proofs). The finite number of formulas is why the people above may still be right. But only a finite number- seems like a weak kind of nonconstructive.
So, based on this post, it is actually not known that P=NP implies existence of polynomial time algorithm for deciding SAT. The universal search idea only yields a polynomial time algorithm that decides SAT for all but a finite number of formulas.