布林可滿足性（boolean satisfiability, SAT）
/ SAT = sat /
想像一整面牆的電燈開關，每個非開即關，經過一團 AND、OR、NOT 邏輯的纏繞接到一盞燈。SAT 問的就只是：「有沒有任何一種」撥動開關的方式能把燈點亮？等價地說，給定一個由真／假變數構成的邏輯公式，我們能否給每個變數指派真或假，使整個公式為真？若能，這公式「可滿足」；若沒有任何設定行得通，它就「不可滿足」。聽起來無害，它卻是計算機科學最初的困難問題。
精確地說，SAT 的一個實例是一個建立在變數 x1, ..., xn 上的布林公式，通常寫成合取範式（CNF）：許多子句的 AND，其中每個子句是若干文字的 OR，而文字是一個變數或其否定，如 (x1 OR not x3 OR x4)。若一組真值指派使每個子句都至少有一個為真的文字（於是每個 OR 為真，使整個 AND 為真），公式就被滿足。SAT 問這樣的指派是否存在。檢查一組提議的指派既瑣碎又快——代入求值即可——這就是為什麼 SAT 屬於 NP，那組指派本身就是憑證。麻煩在於「找出」一組：n 個變數有 2^n 種可能指派，最壞情況下沒有已知方法勝過暴力。舉個小演示，(x1 OR x2) AND (not x1 OR x2) AND (not x2) 不可滿足：最後一個子句逼出 x2 = 假，接著第一個逼出 x1 = 真，但第二個於是需要 not x1 OR x2 = 假 OR 假 = 假。沒有任何指派活得下來。
SAT 的名聲來自庫克-列文定理：它是第一個被證明為 NP 完全的問題，意味著 NP 中每個問題都歸約到它，所以 SAT 和整個類別一樣難。這使它成為證明其他問題 NP 困難的萬用種子——把 SAT（或 3-SAT）歸約到你的問題就大功告成。誠實而美妙的轉折在於理論與實務之間的落差：SAT 是 NP 完全（最壞情況難解），然而現代的 SAT「求解器」例行地解決來自晶片驗證與規劃、含數百萬變數的實例。最壞情況是一堵真實的牆，但典型的工業輸入離最壞情況很遠，所以「NP 完全」是關於最難實例的陳述，而非對你會遇到的每一個實例的判決。
可滿足範例：(x1 OR x2) AND (not x1 OR x3) AND (not x2 OR not x3)。試 x1 = 真、x3 = 真、x2 = 假：子句 1 有 x1 為真；子句 2 的 not x1 為假但 x3 為真；子句 3 有 not x2 為真。所有子句皆真，所以這組指派滿足公式——憑證是 (x1=真, x2=假, x3=真)。
SAT：存在某種真／假設定使每個子句都為真嗎？檢查容易；找出困難。
SAT 是 NP 完全並不代表每個實例都難。工業級 SAT 求解器每天破解龐大的真實公式；難解性是最壞情況、漸進的。反過來，別只因求解器厲害就假設你的公式容易——刻意刁難的實例確實會頑抗。