SATソルバとは

SATソルバとは・・
CNF(乗法標準系)で表された論理式が充足可能（SAT）か充足不能（UNSAT）か調べるプログラムのこと。
　
CNFとは・・
変数もしくは変数の否定（NOT）の和(OR)の積(AND)で表される論理式のこと
例1) (P₁∨P₂)∧(¬P₁∨P₄)
　
充足可能（SAT）とは・・
論理式全体がTrueとなる変数の組が1つ以上存在すること
　
充足不能（UNSAT）とは・・
論理式全体がTrueとなる変数の組が存在しないこと