SATソルバとは・・CNF(乗法標準系)で表された論理式が充足可能（SAT）か充足不能（UNSAT）か調べるプログラムのこと。 CNFとは・・変数もしくは変数の否定（NOT）の和(OR)の積(AND)で表される論理式のこと例1) (P1∨P2)∧(¬P1∨P4) 充足可能（SAT）とは・・論理…