[zaxioms]

Rice's theorem is about decidability, not difficulty. But you are right that assuming P != NP there is no algorithm for efficient SAT (and other constraint) solving.