Satisfierbarhet modulo teorier (SMT) är en formaliserad utökning av logiska formler inom datavetenskap och matematisk logik. Ett SMT-problem uppkommer genom att man kombinerar första ordningens logik och likhet med relationer mellan symboler, där tolkningen av både relationerna och symbolerna är godtyckliga och definieras av den logiska teori de tillhör. Exempel på teorier som ofta används inom datavetenskap är teorierna om reella tal och om heltal, som kan användas till exempel för att uttrycka ekvationer över tal med okända variabler (). Själva problemet SMT handlar om att ge en tilldelning till dessa symboler så att alla villkor är uppfyllda. På det sättet kan SMT beskrivas som en av flera formaliseringar av villkorsprogrammering.
Mer specialiserade teorier är de om olika datastrukturer såsom listor, matriser, bitvektorer, strängar och så vidare.