充足可能性判定手法(Satisfiability)とは、モデル検査の代表的なアルゴリズムの１つで、与えられた論理関数全体を１とするような変数値の割り当てが存在するか否かを判定する手法（SAT手法）のことです。二分決定グラフ（BDD）では、与えられた論理式を満たす解を全てグラフ（木の枝状）で表現、つまり全ての解を保有しているのに対し、SAT手法では、解を１つ見つけようと探索します。SCADEで採用しているSAT手法は、Stalmarckのアルゴリズムという特別な検証エンジンです。