充足可能論理式 (Satisfiable Formula) と非充足可能論理式 (Unsatisfiable Formula)

SAT・充足可能性は、命題変数に真偽値を割り当てて、与えられた論理式を真にできるかを問う問題である。充足可能なら具体的な割り当てが証人になり、非充足ならどの制約が衝突したかを説明する必要がある。充足可能論理式 (Satisfiable Formula) と非充足可能論理式 (Unsatisfiable Formula)では、仕様を制約へ翻訳することが中心になる。

使い方と確認

制約の意味を自然言語の要件と照合し、SATならモデルを、UNSATなら矛盾の核や証明を確認する。DPLLなどの探索では、変数順序・単位伝播・学習・タイムアウトを結果とともに記録する。

限界と注意点

SATであることは仕様が正しいことを保証せず、UNSATも入力エンコーディングの誤りを排除しない。SMTや近似を使う場合は、理論・整数丸め・未モデル化の環境条件を明示する。