One rather serious problem with our rule-based approach to the module enrollment problem is that it’s possible inadvertently to create a set of rules which can’t be satisfied by any set of modules a student might choose.
It’s possible to prove that a set of rules can be satisfied by exhibiting a module selection which satisfies them. It’s possible to prove that they can’t be satisfied by checking all possible module selections. This works in theory because the set of modules, and hence the set of sets of modules, is finite.
For any university with a realistic number of modules checking all possible module selections would never work from a practical point of view. Nevertheless we say the satisfiability problem in this context is decidable, because we could construct a Turing machine which would eventually answer the question. For more complicated languages the satisfiability problem is often undecidable even in theory.
Since our language is essentially that of zeroeth order logic we can borrow satisfiability checking algorithms from there. These methods are faster in practice than checking all possibilities but their theoretical worst case complexity is poorly understood.
I’ve just described satisfiability as a property of a statement in a language, but this isn’t quite correct. It’s a property of the statement, language and interpretation. Without the interpretation we wouldn’t be able to determine when the statement is true.