在計算機科學和數理邏輯中，可滿足性模數理論（SMT）是確定一個數學公式是否可滿足的問題。它將布爾可滿足性問題（SAT）概括為涉及實數、整數和/或各種數據結構（如列表、數組、位向量和字符串）的更復雜的公式。這個名字來源于這樣一個事實，即這些表達式是在一階邏輯的某個形式化理論中以平等（通常不允許量詞）來解釋的（模子）。SMT求解器是旨在解決實際輸入子集的SMT問題的工具。像Z3和cvc5這樣的SMT求解器已經被用作整個計算機科學中廣泛的應用的構件，包括在自動定理證明、程序分析、程序驗證和軟件測試中。由于布爾可滿足性已經是NP-完備的，所以SMT問題通常是NP-困難的，而且對于許多理論來說，它是不可判定的。研究人員研究哪些理論或理論的子集會導致可判定的SMT問題，以及可判定案例的計算復雜性。由此產生的決策程序常常直接在SMT求解器中實現；例如，請看Presburger算術的可解性。SMT可以被認為是一個約束滿足問題，因此是約束編程的某種形式化的方法。

從形式上講，SMT實例是一階邏輯中的一個公式，其中一些函數和謂詞符號有額外的解釋，而SMT是確定這樣一個公式是否可滿足的問題。換句話說，設想一個布爾可滿足性問題（SAT）的實例，其中一些二元變量被合適的非二元變量集上的謂詞所取代。謂詞是一個非二元變量的二元值函數。謂詞的例子包括線性不等式（例如。是兩個參數的一些未指定的函數）。這些謂詞根據各自分配的理論進行分類。例如，實數變量上的線性不等式使用線性實數算術理論的規則進行評估，而涉及未解釋的術語和函數符號的謂詞則使用未解釋的平等函數理論（有時被稱為空理論）的規則進行評估。其他理論包括數組和列表結構的理論（對建模和驗證計算機程序有用），以及位向量的理論（對建模和驗證硬件設計有用）。子理論也是可能的：例如，差分邏輯是線性算術的一個子理論，其中每個不等式被限制為具有以下形式

一個SMT實例是布爾SAT實例的泛化，其中各種變量集被各種基礎理論的謂詞所取代。SMT公式提供了一個比布爾SAT公式更豐富的建模語言。例如，SMT公式允許我們在字級而不是位級上對微處理器的數據通路操作進行建模。相比之下，答案集編程也是基于謂詞（更確切地說，是基于由原子公式創建的原子句）。

與SMT不同，答案集程序沒有量詞，不能輕易地表達諸如線性算術或差分邏輯等約束條件--ASP最多適合于還原為未解釋函數的自由理論的布爾問題。在ASP中把32位整數作為位向量來實現，會受到早期SMT求解器所面臨的大多數問題的影響：諸如x+y=y+x這樣明顯的相同點是很難推導出來的。約束邏輯編程確實提供了對線性算術約束的支持，但是在一個完全不同的理論框架內。SMT求解器也被擴展到解決高階邏輯的公式。

早期解決SMT實例的嘗試是將它們轉化為布爾SAT實例（例如，一個32位的整數變量將由32個具有適當權重的單位變量來編碼，字級操作如"加"將由位上的低級邏輯操作來代替），并將這個公式傳遞給布爾SAT解算器。