Satisfiable Modulo Theories Solvers

Software tools for efficient and fully automatic analysis of the satisfiability of a formula in predicate logic with theories.

However, the satisfiability of predicate logic is not decidable, meaning not all satisfiability questions can be answered automatically.

Interesting research questions:

1. What theories are useful? (e.g arithmetic, records, lists, bit vectors, etc)
2. How much is decidable? (e.g subsets of predicate logic are decidable such as Presburger arithmetic)
3. How do we combine the methods used for solving problems in different theories?