SAT solver 是解決 SAT 問題的程式的統稱，這裡介紹一些先備知識，以及 miniSAT 這套開源的 SAT solver。
variable boolean function 裡面用到的那些值就叫 variable，例如: (¬a ∨ b ⊕ x)，a, b, x 就是它的 variable，當然 variable 要取什麼名子都可以。
literal 在 boolean function 中實際出現的 variable 就叫 literal，其中帶有 NOT(negation, ¬) 的叫 negative literal，沒有的叫 positive literal，例如: (¬a ∨ a)，就有 a 的 negative literal、positive literal 各一個。