Why is SAT so important in theoretical computer science?
SAT was the first problem shown to be NP-complete, in Stephen Cook's seminal paper. Even nowadays, when introducing the theory of NP-completeness, the starting point is usually the NP-completeness of SAT.
SAT is also amenable to surprisingly successful heuristic algorithms, implemented by software known as SAT solvers. As a result, there is a lot of practical interest into formulating problems efficiently as instances of SAT.
SAT also shows up in fine-grained complexity, one of whose main assumptions is the strong exponential time hypothesis, which is a conjecture on the computational complexity of SAT.