 Satisfiability modulo theories

Satisfiability Modulo Theories (SMT) is a decision problem that extends the concepts of propositional satisfiability (SAT) by incorporating theories about certain data types and structures. In essence, SMT asks whether a given logical formula can be satisfied when the formula is interpreted not only over boolean variables but also over more complex data types defined by theories, such as arithmetic, arrays, bit-vectors, or others.