And indeed I think the reduction of NP problems to SAT is pretty intuitively understandable, at least at a hand-wavy level. If a decision problem is in NP, then

And indeed I think the reduction of NP problems to SAT is pretty intuitively understandable, at least at a hand-wavy level. If a decision problem is in NP, then given some candidate solution to the problem we can verify it in polynomial time. If you imagine a computer implementing this decision algorithm, and you squint your eyes, you can imagine it as a huge boolean satisfiability problem. The program takes some input (as bits aka boolean variables) and the program is run in the circuitry of the computer which at the bottom is effectively doing boolean algebra with logic gates and such. And so if you can solve SAT in polynomial time, then you can run it on this instance of SAT (the instantiation of the verifier for this NP problem) and find out if there's any input to that NP problem that satisfies it. Obviously there's a lot more work to make it formal.