SAT解算器在計算機科學和形式化方法中，SAT解算器是一個旨在解決布爾可滿足性問題的計算機程序。在輸入一個布爾變量的公式時，比如（x或y）和（x或不y），SAT求解器會輸出該公式是否可滿足，即x和y有可能使該公式為真，或者不可滿足，即x和y沒有這種值。自從20世紀60年代引入SAT算法以來，現代SAT求解器已經發展成為復雜的軟件產品，涉及到大量的啟發式算法和程序優化，以便高效工作。根據一個被稱為庫克-列文定理的結果，布爾可滿足性一般是一個NP-完全的問題。因此，只有指數級的最壞情況下的復雜度的算法是已知的。盡管如此，高效和可擴展的SAT算法在2000年代被開發出來，并且在我們自動解決涉及數萬個變量和數百萬個約束條件的問題實例的能力方面取得了巨大的進步。SAT求解器通常從將公式轉換為共軛正常形式開始。它們通常基于核心算法，如DPLL算法，但也包括一些擴展和功能。大多數SAT求解器包括超時，所以即使他們不能找到一個輸出為未知的解決方案，他們也會在合理的時間內終止。通常情況下，SAT求解器不只是提供一個答案，而是可以提供進一步的信息，包括在公式可滿足的情況下提供一個賦值的例子（x，y等的值），或者在公式不可滿足的情況下提供最小的不可滿足的條款集。現代SAT求解器對包括軟件驗證、程序分析、約束條件求解、人工智能、電子設計自動化和運籌學等領域產生了重大影響。強大的求解器很容易以免費和開源軟件的形式出現，并且被內置到一些編程語言中，比如在約束邏輯編程中把SAT求解器暴露為約束條件。概述DPLL求解器DPLLSAT求解器采用一個系統的回溯搜索程序來探索變量賦值的（指數大小）空間，尋找滿意的賦值。這個基本的搜索過程是在20世紀60年代初的兩篇開創性的論文中提出的,現在通常被稱為Davis-Putnam-Logemann-Loveland算法（DPLL或DLL）。許多現代的實際SAT解題方法都是從DPLL算法中衍生出來的，并且具有相同的結構。通常他們只提高了某些類別的SAT問題的效率，如工業應用中出現的實例或隨機生成的實例。

理論上，DPLL系列算法的指數下限已經被證明。不屬于DPLL系列的算法包括隨機的局部搜索算法。一個例子是WalkSAT。隨機方法試圖找到一個滿意的解釋，但不能推斷出一個SAT實例是不可滿足的，與完整算法相反，如DPLL。相比之下，隨機算法，如Paturi,Pudlak,Saks和Zane的PPSZ算法，根據一些啟發式方法，例如有界寬度解析，以隨機順序設置變量。如果啟發式方法不能找到正確的設置，變量就會被隨機分配。PPSZ算法的運行時間為為3-SAT。這是這個問題最有名的運行時間，直到2019年，Hansen、Kaplan、Zamir和Zwick發表了該算法的修改，運行時間為對于3-SAT，后者是目前已知的在所有k值下最快的k-SAT算法。后者是目前已知的k-SAT在所有k值下最快的算法。在有許多滿足的賦值的情況下，Sch?ning的隨機算法有更好的約束。

現代SAT求解器（2000年開發）有兩種類型：沖突驅動型和前瞻型。這兩種方法都是由DPLL演變而來。沖突驅動的求解器，比如沖突驅動的子句學習（CDCL），用高效的沖突分析、子句學習、非同步回溯（又稱回跳），以及雙打字單元傳播、自適應分支和隨機重啟來增強基本的DPLL搜索算法。經驗表明，這些基本的系統搜索的附加功能對于處理電子設計自動化（EDA）中出現的大型SAT實例至關重要。著名的實現包括Chaff和GRASP。前瞻性求解器特別加強了還原（超越了單元句傳播）和啟發式求解器，它們在困難實例上通常比沖突驅動的求解器更強（而沖突驅動的求解器在大實例上會好得多，因為這些實例內部實際上有一個簡單的實例）。