There is a very classic connection between logic and algebra, which goes back to the origin of modern logic and the work of George Boole. A formula in propositional logic can be interpreted as an element of a Boolean algebra. The logical constants true and false become the algebraic notions of the top and bottom element of a lattice. The logical operations of conjunction, disjunction and negation will become the algebraic operations of meet, join and complementation in the Boolean algebra. This connection is less emphasised in modern treatments of logic, but it is particularly interesting in the context of your question. Algebra allows us to move away from many problem specific details and find generalisations of a problem that will apply to many different situations.
In the specific case of SAT, the algebraic question one may ask is what happens when we interpret formulae in more general lattices than Boolean algebras. On the logical side, you can generalise the satisfiability problem from propositional logic to intuitionistic logic. More generally, you can generalise the propositional satisfiability problem to that of determining if a formula, when interpreted over a bounded lattice (one with top and botto), defines the bottom element of the lattice. This generalisation allows you to treat problems in program analysis as satisfiability problems.
Another generalisation is to quantifier-free first-order logic where you get the question of Satisfiability Modulo a Theory. Meaning, in addition to having Boolean variables, you also have first-order variables and function symbols and you want to know if a formula is satisfiable. At this point you can ask questions about formulae in arithmetic, theories of strings, or arrays, etc. So we get a strict and very useful generalisation of SAT which has lots of applications in systems, computer security, programming languages, program verification, planning, artificial intelligence, etc.