1 充足判定の概要
1.1 用語と基本概念
1.1.1 充足・充足可能性
充足判定とは、与えられた論理式に対して「それを真にする解が存在するか」を判断する枠組みである。論理式が真となるような解が存在するとき、その論理式は充足可能である、または充足すると呼ばれる。逆に、どの解を選んでも真にならない場合は充足不能となる。 この概念は「真偽の確定」を直接問うだけでなく、成立のための構造的な存在（満たす割当や解釈）を問題の中心に据える点に特徴がある。
1.1.2 解釈・変数への値割当
命題論理では変数（原子命題）に対し真偽値を与える割当が解に相当する。具体的には、ある集合に含まれる命題記号それぞれへ真（真理値）または偽を割り当て、式全体が真になるかを調べる。 述語論理ではさらに、定数記号の指す対象、関数記号の振る舞い、述語記号が対象の組に対して成り立つかを定める必要がある。これらをまとめて解釈と呼び、式中の変数には量化（存在・全称）によって変数の値域が選ばれるため、割当という語の使い方が状況により異なる。
1.1.3 真偽判定との違い
真偽判定は「与えられた論理式が、指定された解釈のもとで真か偽か」を問うことが多い。つまり、解釈や値が固定されている前提で評価する。 これに対し充足判定は、解釈や割当を探しに行き、条件を満たすものが存在するかを問う。評価対象が「ある解釈で真となるかどうか」へと変わるため、探索や推論の性質が強くなる。
1.2 対象となる論理式の種類
1.2.1 命題論理の充足判定
命題論理の充足判定は、原子命題への真偽値割当を選んだとき、複合論理式が真になるかを確認する問題として定式化される。演算子として、否定、連言、選言、含意などが用いられる。 実務では入力形式が多様であっても、計算上扱いやすい形に変換してからSATソルバにより求めることが一般的である。
1.2.2 述語論理の充足判定
述語論理の充足判定では、量化（存在量化・全称量化）を含む式を扱う。存在量化の下では、ある対象の選択により成り立つことが求められる一方、全称量化ではすべての対象で成り立つ必要がある。 その結果、命題論理よりも探索空間が拡大しやすい。さらに、対象領域や関数・述語の解釈が未固定であるため、充足性の判定にはより強い推論や変換が必要となる。
1.2.3 正規形・前処理の位置づけ
入力された論理式は、探索を効率化するために前処理を受けることが多い。代表的には、論理等価変形や正規形への変換が用いられる。 正規形は、充足性という性質を保ちながら、探索アルゴリズムが扱いやすい局所構造（節や制約の形）へ整理する役割を担う。前処理は最適化の一部であり、厳密な意味保存が基本となる。
2 関連する判定問題と位置づけ
2.1 包含関係と代表的な問題
2.1.1 恒真性・充足不能性との関係
恒真性は、あらゆる割当（または解釈）のもとで常に真となる性質である。命題論理では、恒真性は「充足不能性の否定」へ連結できる。すなわち、式が恒真でないことは「その否定が充足可能である」ことと対応する場合が多い。 一方、充足不能性は「どの割当でも真にならない」ことを意味し、否定すると充足可能性と表裏の関係になる。これにより、同一の探索枠組みを、肯定側と否定側のどちらから見るかで使い分ける設計が可能になる。
2.1.2 妥当性・論理的含意との関係
妥当性は「前提が成り立てば結論が必ず成り立つ」こと、すなわち論理的含意に対応する概念である。論理的含意 \(A \Rightarrow B\) は、もし \(A\) が真であり \(B\) が偽になる解が存在しなければ、妥当であると表現できる。 このとき、\(A\) かつ \(\lnot B\) を同時に満たす割当が存在するか、つまり充足判定に落とし込むことで、含意の成否を決定できる。したがって充足判定は、論理的推論の検査器として位置づけられる。
2.1.1.1 検証（モデル）と探索（満たす割当）の違い
モデル検証は、具体的な対象（たとえばある仕様のモデル、または与えられた解釈）を入力し、それが条件を満たすかを確認する作業である。ここでは解釈が与えられているため、成立不成立は評価に近い。 一方、満たす割当の探索は、条件を満たす解を自力で構成する方向に働く。成立の証拠として、真偽値の選び方や解釈の候補が求められるため、探索・推論の比重が増す。充足判定は後者の性質を中心に持つ。
2.2 計算量の直観的理解
2.2.1 意味づけの難しさ
充足性は、論理式の構造により探索の難しさが大きく変動する。変数数や節数などの量的指標だけでなく、依存関係の偏りや制約の絡み具合が効くため、直観的に性能を見積もるのが難しい。 また、同じ難度に見える式でも、前処理や探索順序の選択次第で計算量が大きく変わることがある。
2.2.2 代表的な難度クラスの概観
命題論理の一般的な充足判定は、典型的にNPに属する問題として理解されることが多い。これは「満たす割当が存在するなら、その提示が検算可能」という性質と整合する。 述語論理では量化が加わるため、より高い複雑さを取りうる。どの断片理論（制限付きの論理体系）を扱うかで、計算可能性や決定可能性の性質が異なり、難度は一様ではない。
3 代表的な手法
3.1 ブール充足（SAT）に基づく手法
3.1.1 DPLL系
DPLL系は、変数に対する真偽値を段階的に決め、矛盾が出れば巻き戻すという系統の探索法である。分岐（どの値を仮に置くか）と、制約から導ける自動決定（単位に関する推論）を組み合わせる。 矛盾は「仮定した割当が節の要件を満たさない」こととして現れ、バックトラックにより探索が進む。効果的な分岐順序や簡約が性能に直結する。
3.1.2 CDCL系
CDCL系（競合学習を含む系統）は、矛盾の発生時に、なぜ矛盾に至ったかを要約する情報（学習節）を生成し、その後の探索で再利用する。これにより同種の矛盾を繰り返しにくくなる。 学習と削除（節の管理）を組み合わせることで、巨大な探索木の一部を効果的に圧縮し、結果として探索が加速される場合が多い。
3.1.3 単位伝播と分岐
単位伝播は、ある節が「未割当の変数が1つだけで、残りがすでに偽」になっている状況など、満たすために残りの変数の値が一意に決まる場合に、その値を自動で割り当てる推論である。 この推論で矛盾が生じなければ、次に分岐でより大域的な選択を行う。分岐は探索の枝を増やすため、単位伝播の活用度が探索の伸びを抑える要となる。
3.2 形式変換によるアプローチ
3.2.1 論理式の正規化
形式変換では、充足性を保つ変形により、扱う論理式の形を一定の形式へ整える。命題論理なら、演算子の種類を制限し、連言標準形のような形に揃えることがある。 正規化は、後続処理（節学習や枝刈り）に都合のよい構造を生成し、アルゴリズムの適用を可能にする。
3.2.2 モデル探索への落とし込み
正規化の結果は、探索アルゴリズムが要求する入力形式へ変換される。たとえば、制約表現を節集合として表し、真偽割当の探索問題に変形することで、SATソルバの枠組みに載せられる。 述語論理の場合でも、特定の制限や近似、またはスキーレム化などを通じて、有限の探索へ落とし込む試みが行われることがある。落とし込みの選択は、完全性と計算の現実性のトレードオフになりやすい。
3.3 述語論理向けの手法
3.3.1 レベル付きスキーレムと探索
レベル付きスキーレムは、量化を含む式に対して、複数の「候補」を段階的に導入しながら充足性を探索する発想に関係する。レベル（深さ）を設けることで、どの程度まで候補の展開を許すかを制御し、探索領域を制約する。 これにより、無限に見える可能性を現実的な範囲へ近づけ、反例探索に似た挙動で進められることがある。
3.3.2 反証駆動（不可能性の導出）
反証駆動の枠組みでは、充足できないことを示す方向に推論を進める。すなわち「仮に満たせるなら」という仮定から矛盾を導き、不可能性の証拠を構成する。 このとき、単純な探索だけでなく、導出規則によって矛盾へ至る道筋を生成し、学習や簡約によって探索を整理することもある。結果として、充足不能性の裏付けが得られる場合がある。
4 出力と活用場面
4.1 充足時に得られる情報
4.1.1 充足割当（モデル）
充足判定が成功した場合、一般には満たす割当が返される。命題論理では各変数の真偽値リストが、述語論理ではより複雑な解釈情報や、量化に基づく具体例が相当する。 この割当は「存在の証明」であり、条件を満たす具体的な例として利用できる。さらに、割当から追加制約を検査することもできる。
4.1.2 反例ではなくモデルの提示
充足可能性の判断では、しばしば「満たす側の具体例」を提示する。これは、充足不能のときのように否定事例を提示するのとは対照的である。 モデルが得られると、仕様通りに動くことの具体的な見取り図が得られ、次の工程（設計の反復や理解の補助）に直結しやすい。
4.2 充足不能時に得られる情報
4.2.1 證明（充足不能性の根拠）
充足不能となる場合、ソルバは単に「不可能」と言うだけでなく、どの制約同士の競合が本質かを示す根拠を返すことがある。SAT系では学習節や矛盾導出の履歴が証明に相当しうる。 この証明は、後処理で検証可能な形式（証跡）として扱われる場合があり、単なる結論以上の価値を持つ。
4.2.2 どこまで探索したか
探索の進行範囲は、実装や出力設定により異なるが、「すべて試した」という形で完全性を保証するとは限らない。SAT系の一部では、矛盾により探索木が閉じたことが示されるため、理論上は網羅性が担保される。 一方で述語論理の近似や段階的展開では、探索の深さや打ち切り条件に依存して結論が得られることがあり、どの仮定のもとで言えるかを区別する必要がある。
4.3 実応用と関連領域
4.3.1 検証・テスト生成
充足判定は、仕様が両立するか、または成立条件を満たす入力が存在するかを確認する用途に広く使われる。特にテスト生成では、条件を満たす入力の存在を探すことで、自動的に候補が作られる。 モデルが得られる場合は、そのままテストケースとして利用できるため、手作業の負担を減らす。
4.3.2 設計制約の整合性チェック
部品配置、配線、スケジュールなどの設計制約を論理式に写像し、整合性（矛盾がないこと）を調べる場面がある。充足不能なら矛盾の原因候補が推定され、設計条件の見直しにつながる。 充足可能なら、実行可能な計画の種としてモデルが参照される。
4.3.3 ゲーム・パズルの解探索
ゲームやパズルでは、状態遷移やルールを制約として表し、勝利条件や達成条件を満たす配置・手順を探すことがある。充足判定により解の存在を調べ、得られたモデルを手順に復元して提示できる。 解が見つからない場合でも、ルールの組合せが矛盾している可能性や、探索上の前提が適切でない可能性を示唆する材料になりうる。