Comment Comment by 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. parent zaxioms 1 year ago