在邏輯學和計算機科學中，布爾可滿足性問題（有時稱為命題可滿足性問題，縮寫為SATISFIABILITY，SAT或B-SAT）是確定是否存在一個滿足給定布爾公式的解釋的問題。換句話說，它問的是，一個給定的布爾公式的變量是否可以持續地被TRUE或FALSE的值取代，從而使公式的值為TRUE。如果是這樣的話，這個公式就被稱為可滿足。另一方面，如果不存在這樣的賦值，那么對于所有可能的變量賦值，該公式所表達的函數都是FALSE，該公式是不可滿足的。例如，公式aANDNOTb是可滿足的，因為我們可以找到a=TRUE和b=FALSE的值，這使得（aANDNOTb）=TRUE。相比之下，aANDNOTa是不可滿足的。SAT是xxx個被證明是NP-complete的問題；見Cook-Levin定理。這意味著復雜度等級NP中的所有問題，包括廣泛的自然決策和優化問題，最多只能像SAT一樣難以解決。沒有已知的算法可以有效地解決每一個SAT問題，人們普遍認為不存在這樣的算法；然而這種信念還沒有得到數學上的證明，解決SAT是否有多項式時間算法的問題相當于P與NP的問題，這是計算理論中一個著名的開放問題。然而，截至2007年，啟發式SAT算法能夠解決涉及數萬個變量和由數百萬個符號組成的公式的問題實例，這對于許多實際的SAT問題，如人工智能、電路設計和自動定理證明來說是足夠了。

一個命題邏輯公式，也叫布爾表達式，是由變量、運算符AND（結合，也用∧表示）、OR（分離，∨）、NOT（否定，?）和括號構成的。如果一個公式可以通過分配適當的邏輯值（即TRUE，FALSE）而變成TRUE，那么它就被認為是可滿足的。布爾可滿足性問題（SAT）是，給定一個公式，檢查它是否可滿足。這個決策問題在計算機科學的許多領域具有核心重要性，包括理論計算機科學、復雜性理論、算法學、密碼學和人工智能。

一個字面是一個變量（在這種情況下，它被稱為正字面）或一個變量的否定（稱為負字面）。一個子句是一個字面的二連詞（或一個單字面）。如果一個子句最多包含一個正字，則稱為角子句。如果一個公式是子句的聯結（或單個子句），則為共軛正常形式（CNF）。例如，x1是一個正字，?x2是一個負字，x1∨?x2是一個子句。公式(x1∨?x2)∧(?x1∨x2∨x3)∧?x1是連接的正常形式；它的xxx個和第三個子句是霍恩子句，但第二個子句不是。通過任意選擇x1=FALSE,x2=FALSE,和x3，這個公式是可滿足的。因為(FALSE∨?FALSE)∧(?FALSE∨FALSE∨x3)∧?FALSE評價為(FALSE∨TRUE)∧(TRUE∨FALSE∨x3)∧TRUE，進而評價為TRUE∧TRUE∧TRUE(即TRUE)。也就是到TRUE）。

相反，CNF公式a∧?a，由一個字面的兩個子句組成，是不可滿足的，因為對于a=TRUE或a=FALSE，它分別求值為TRUE∧?TRUE(即FALSE)或FALSE∧?FALSE(即再次FALSE)。對于某些版本的SAT問題，定義廣義共軛正常形式公式的概念是很有用的，即作為任意多的廣義子句的連接，后者的形式是R(l1,...,ln)，用于一些布爾函數R和(普通)字元li。不同的允許布爾函數集會導致不同的問題版本。

2個變量的n個連接詞的二擇一，后者由n個變量的2n個子句組成。然而，通過使用Tseytin變換，我們可以找到一個長度與原命題邏輯公式大小成線性關系的可滿足的共軛正常形式公式。