1 充足可能性の基本概念
1.1 命題論理における定義
1.1.1 変数への真偽値の割り当て
命題論理では、論理式は真偽値をとる変数（原子命題）と、論理結合子（たとえば「かつ」「または」「否定」「ならば」など）から構成される。変数への割り当てとは、各変数に対して「真」または「偽」のいずれかを対応づけることである。割り当てが与えられると、論理式は構成規則に従って一意に真偽が決まる。
1.1.2 真となる割り当ての存在条件
充足可能性とは、「ある割り当てによって当該の論理式が真になるか」という問いに対応する。つまり、変数への割り当てを全探索していく過程で、少なくとも一つでも論理式全体を真に評価する割り当てが見つかれば、その論理式は充足可能とされる。逆に、どの割り当てを選んでも偽になってしまうなら充足不能である。
1.2 充足可能・充足不能の区別
1.2.1 充足可能性の判定結果
判定の結果は二値である。充足可能性が肯定される場合、論理式を満たす具体的な割り当て（モデル）が存在することになる。否定される場合は、満たす割り当てが存在しないという意味で、論理式は矛盾を含む状態として捉えられる。
1.2.2 充足不能性との関係
充足不能性は「論理式が充足されない」という事実そのものを指すが、直観的には「内部条件が両立しない」ことの表現でもある。たとえば、ある条件が同時に成り立たない形で組み合わされていると、どの割り当てを選んでも矛盾が現れ、論理式は常に偽評価になる。
1.3 充足可能性と同値・論理的帰結
1.3.1 同値な論理式の扱い
二つの論理式が充足可能性の観点で同じ振る舞いをすることがある。たとえば、論理式AとBがあらゆる割り当てで同じ真偽値をとるなら、充足可能性は一致する。実際の手続きでは、論理式を等価変形して形を整えることが多いが、このとき変形が同値であれば充足可能性の結果を保つ。
1.3.2 知識（条件）から結論（制約）を導く視点
充足可能性は、情報源としての前提（条件）と、要請される制約（結論の形）の関係を扱うのに向く。典型的には「前提に反する形の制約は満たせるか」を見ることで、ある帰結が前提から導けるかどうかを判定できる場合がある。すなわち、充足不能性は「矛盾が不可避である」ことを示唆し、情報の整合性確認として解釈されやすい。
2 決定問題としての定式化
2.1 充足可能性問題（SAT）
2.1.1 入力としての論理式
SAT（充足可能性問題）は、与えられた論理式を充足可能かどうかで答える決定問題として定式化される。入力は命題論理の論理式であり、変数集合と結合子からなる構造が与えられる。実務では扱いやすい内部表現に変換されることが多いが、概念としては「その論理式が満たされるか」を問う点に本質がある。
2.1.1.1 正規形への変換の考え方
多くのSAT手法では、論理式を正規形（例として節の連言形式）へ変換して扱う。変換は、真偽評価に関する同値性や充足可能性の保存を保証する形で行うのが基本である。正規形にすると、各部分の制約が局所的に整理され、アルゴリズムの判定規則が機械的に適用しやすくなる。
2.1.2 出力としての充足有無
2.1.2.1 「モデル（充足する割り当て）」の提示
SATの出力は「充足可能」または「充足不能」のいずれかである。多くの解法では、充足可能の場合に加えて、具体的なモデル（変数への割り当て）を提示できる。これは、単なる有無判定にとどまらず、満たす構成例を得るという意味で重要な成果となる。
2.2 拡張された枠組み（SMTなど）
2.2.1 理論（例：整数・実数）の組み込み
SMT（制約充足問題を理論拡張した枠組み）では、命題変数だけでなく、整数や実数、配列、ビット列などのデータ領域を扱う論理を用いる。論理式には、これらの領域に関する述語が含まれ、値の整合性まで同時に満たす必要がある。結果として、単なる真偽だけでなく、具体的な数値関係も条件として表現できる。
2.2.2 充足可能性判定の役割
SMTでは「拡張された論理式が満たされるか」が中心問題として据えられる。探索は命題部分だけでなく、領域固有の整合性をチェックする必要があるため、SATより表現力が高い一方で手続きは複雑になりやすい。ただし、満たす割り当てが見つかれば具体的な解として利用でき、満たせなければ矛盾の証拠に基づく解析に進める。
2.3 決定不能性や計算困難性の位置づけ
2.3.1 計算量の一般的な見通し
命題論理に基づくSATは、一般に計算困難とされる領域に属する。入力サイズが増えるにつれて、最悪の場合の計算量が急速に大きくなる可能性があるという意味で、効率は万能ではない。とはいえ、典型的な実用インスタンスには規則性が含まれることも多く、特化手法が大きく効く場合がある。
2.3.2 問題の難しさと実用上の工夫
実務では、探索空間の削減、矛盾の早期検出、学習による再利用などの工夫が組み合わされる。たとえば、矛盾が生じる原因に関する情報を記録し、次の分岐の選択を改善することで、同じ失敗を繰り返しにくくする。さらに、正規形への変換や制約の整理により、アルゴリズムが扱いやすい構造が作られる。
3 代表的な手法とアルゴリズム
3.1 バックトラッキングと探索
3.1.1 深さ優先探索の考え方
バックトラッキングは、変数に順序を与え、値を仮定して部分的に真偽を評価しながら進める方法である。深さ優先探索では、いまの仮定で矛盾が出ない限り次へ進み、矛盾が出たら直近の仮定を反転して別の分岐を試す。探索木の枝を辿るため、見通しは直観的である。
3.1.2 早期打ち切り（枝刈り）
枝刈りは、「この先に進んでも解が見つからない」ことが検出された時点で探索を打ち切る工夫である。矛盾が部分評価の段階で発見されれば、それ以降の深掘りを省略できる。これにより無駄な分岐を減らし、計算時間の短縮が期待できる。
3.2 逐次代入と制約伝播
3.2.1 単位節の扱い
逐次代入では、確定できる値を優先的に決める。単位節（残りの未確定部分が一つだけで、その節が満たされるために特定の値が必要になる状況）に遭遇すると、その値は強制的に決まる。これにより、選択の自由度が減り、矛盾の兆候も早く見えるようになる。
3.2.2 伝播による矛盾の検出
制約伝播は、ある代入が他の節に影響し、結果として追加の代入が発生する流れを指す。連鎖的に新しい確定が生じ、最終的に節が同時に満たせなくなる状態が現れれば矛盾が成立する。矛盾が確認されると、その時点で現在の分岐が不可能であると判断できる。
3.3 衝突主導型手法（CDCL系）
3.3.1 衝突の学習の概念
CDCL（衝突主導型の学習）では、矛盾が生じた原因を記録し、次回以降に活用する。具体的には、矛盾を説明する形の情報を新たな制約として追加することで、同種の失敗を避ける方向へ探索が誘導される。学習は単なるログではなく、実際の判定規則を通じて探索を加速する。
3.3.2 どこまで巻き戻すか（バックジャンプ）
矛盾に直面したとき、直近の仮定だけを反転する代わりに、より前の分岐点へ戻ることがある。どのレベルまで戻すかは、学習した情報が示す依存関係に基づいて決められる。この性質により、無駄な探索を短い巻き戻しで済ませられる場合がある。
3.4 確率的・ヒューリスティックなアプローチ
3.4.1 ランダム化の狙い
確率的手法は、固定した規則だけでは探索が停滞する状況を避けるために、分岐や初期割り当てに乱数を導入する。偶然の選択により局所的な行き止まりを突破できることがある一方、安定した保証は状況依存となる。そこで複数回の試行を組み合わせる設計がよく用いられる。
3.4.2 ヒューリスティック選択の例
ヒューリスティックでは、どの変数を次に決めるか、どちらの値を試すかを「見込み」に基づいて選ぶ。たとえば、頻繁に登場する変数、最近になって矛盾への寄与が大きかった変数などを優先する考え方がある。目的は、矛盾に到達するまでの手数を平均的に減らすことにある。
4 応用領域と具体例
4.1 検証・妥当性確認
4.1.1 条件の整合性チェック
形式仕様における複数条件の整合性は、充足可能性として扱える。条件群を論理式へ整理し、「同時に満たせる割り当てがあるか」を調べることで、互いに両立するか否かを機械的に評価できる。結果として、設計上の矛盾が早期に見つかる。
4.1.2 バグの再現条件の探索
バグ再現の条件が「あるイベント列が成立し、かつ特定の状態に到達する」などの形で記述できる場合、充足可能性は有効な探索器として働く。満たすモデルは、バグを引き起こす入力や前提の具体例として得られることがある。これにより、再現の手作業を減らし、解析を効率化する。
4.2 計画・スケジューリング
4.2.1 制約充足としての定式化
計画問題では、行動の選択、実行順序、資源制約などを論理式に落とし込むことで、計画全体を一つの充足問題へまとめられる。各時点における選択肢を変数で表し、「同時に矛盾する行動は選ばない」「必要な前提が揃ってから実行する」といった条件を制約として組み立てる。
4.2.2 実行可能スケジュールの探索
充足可能性が肯定されれば、条件を満たすスケジュールが存在することになる。モデルは、各時点にどの行動を割り当てるべきかの形で得られ、実行可能性の根拠として利用できる。さらに目的関数を導入する場合は、満たせるかだけでなく「より良い」計画へ拡張する設計が可能となる。
4.3 暗号・セキュリティへの利用
4.3.1 キーや条件の整合性探索
暗号関連では、「ある観測に整合する鍵候補が存在するか」といった問いが充足可能性として表現されることがある。暗号内部の変換を論理式へ近似的に展開し、観測値と矛盾しない割り当てを探索する枠組みである。成功すれば整合的な鍵候補の一例を得られる。
4.3.2 攻撃方針の定式化
攻撃手順の条件を論理制約としてまとめ、どの組合せが成り立つかを調べる用途でも利用される。ここでは、攻撃に必要なイベントや条件を満たすモデルが存在するかが問題になる。結果が「満たせない」であれば、その組合せでは攻撃が成立しない可能性を示す材料になる。
4.4 仕様と要件の「満たせるか」確認
4.4.1 ユーザー要件の論理化
要件を自然言語から論理式へ変換する際、許容範囲や禁止条件を明確にし、それらを論理結合子で表す。たとえば「Aが選ばれるならBも満たす」「Cは同時に満たしてはならない」といった構造を整理し、充足可能性として問い直すことで、要件間の衝突を早期に検出できる。
4.4.2 破綻箇所の特定（原因分析）
充足不能が判明した場合、どの部分が原因で両立しないのかを調べる作業が重要になる。一般に、矛盾の原因に関係するサブセットを抽出する方向で解析が進められ、必要な修正点の候補が提示される。これにより、要件文書の手戻りを減らす効果がある。
4.5 恋愛・人間関係への比喩（軽い応用）
4.5.1 「条件を全部満たす組み合わせはあるか」という見立て
恋愛の会話でも、「譲れない条件を複数並べたとき、それらを同時に満たせる相手像が存在するか」という比喩として充足可能性が語られることがある。たとえば連絡頻度、価値観の傾向、将来の希望などを条件として並べ、「全部を満たす組合せがあるか」を考える視点である。
4.5.2 譲れない条件の整理と優先順位
比喩としての利点は、条件を整理して衝突を見つけやすくなる点にある。満たせないと感じたときに、どれが障害になっているかを見直し、優先順位の再設定に結びつけられる。現実の意思決定では論理式のような厳密さはないが、整理の枠組みとしては役立つ場合がある。
5 関連概念
5.1 包含関係：充足可能性・妥当性・充足性
充足可能性は「少なくとも一つの割り当てで真になる」ことを問う性質である。一方、妥当性(恒真性)は「すべての割り当てで真」であることを意味し、充足性は文脈により「満たす割り当てを持つ」ことを指す場合がある。これらは互いに異なる概念だが、真偽評価の仕方によって関係づけられる。
5.2 モデル、解、反例の考え方
モデルは、論理式を真にする具体的割り当てであり、充足可能性の肯定証拠となる。反例は、主張が正しいと仮定したときにそれを否定する割り当てや状況として扱われることが多い。充足不能の場合には、反例ではなく矛盾の一貫性が示される点が対照的である。
5.3 正規形（CNFなど）と変換の意味
正規形は論理式の形を特定の規則に従わせることで、推論や探索に適した構造を作るために用いられる。CNFのような形に変換することで、各制約が「節」として扱いやすくなる。変換が同値性または充足可能性保存を満たすことが前提となる。
5.4 ブール代数との関係
命題論理の変数と論理結合子は、ブール代数の演算として捉えられることがある。否定、論理和、論理積などの対応が明確であるため、充足可能性はブール式が特定の評価で真になるかどうかという問題に同型化できる。これにより、代数的な視点からも性質を理解しやすくなる。
5.5 証明（充足）と反証（充足不能）の対応
充足可能性に対しては、モデルが見つかることで充足の証拠として機能する。充足不能性に対しては、理屈の上で矛盾が必ず生じることを示す形の証明が対応する。アルゴリズムによっては「どうしても満たせない」ことを導くための補助情報が出力され、それが反証に相当する役割を担う。