In computational complexity theory, Cook's theorem, also known
as the Cook–Levin theorem, states that the Boolean satisfiability
problem is NP-complete. That is, any problem in NP can be reduced
in polynomial time by a deterministic Turing machine to the problem
of determining whether a Boolean formula is satisfiable.