Polynomial-Time Solvability of SAT Implies $\mathrm{P}=\mathrm{NP}$