1 SATの基本
SATは、与えられた論理式が同時に真となるような変数の割当が存在するかを調べる問題領域である。計算機科学では、論理、探索、制約処理を結び付ける基礎的な枠組みとして扱われ、理論研究と実装技術の双方で重要な位置を占める。
1.1 充足可能性の定義
充足可能性とは、論理式の各条件を矛盾なく満たせるかどうかを指す。式全体を真にする割当が少なくとも1つ見つかれば充足可能、いかなる割当でも真にできなければ充足不可能である。
1.1.1 ブール変数と論理式
SATで扱う中心的な対象はブール変数であり、各変数は真または偽の2値をとる。これらを論理和、論理積、否定などで組み合わせた論理式が入力となり、式の構造によって満たしやすさや探索の難度が変化する。
1.1.2 真偽割当（解）の考え方
真偽割当は、各変数に真偽値を対応させた配置である。SATでは、この割当が全体の制約を満たすかを判定し、満たす場合にはその割当自体が解として扱われる。複数の解が存在することもあり、その場合は異なる割当が同じ式を充足する。
1.2 SATの形式表現
SATは抽象的な論理概念である一方、計算機上では一定の標準形式に変換して扱うことが多い。これにより、入力の記述が統一され、解法アルゴリズムを共通化しやすくなる。
1.2.1 結合正規形（CNF）
結合正規形は、複数の節を論理積で結んだ形で、各節はリテラルの論理和として表される。実用的なSATソルバーはこの形を前提とすることが多く、理論面でも標準的な表現として広く用いられている。
1.2.2 リテラル・節・変数の役割
リテラルは変数またはその否定を意味し、節はそれらをまとめた小さな条件群である。変数は命題の基本単位として振る舞い、節はその変数群に対する局所的な制約を与える。式全体は、こうした局所条件の組合せとして理解できる。
1.3 問題としての性質
SATは、単なる計算手順ではなく、明確な入力と判定基準を持つ意思決定問題である。この性質により、可解性の研究、計算量の分析、アルゴリズム比較が可能になる。
1.3.1 決定問題としての位置づけ
決定問題とは、答えが「はい」か「いいえ」で表される問題である。SATでは、式が充足可能か否かを判定することが中心であり、解の具体的な列挙や最適化とは区別される。
1.3.2 充足不可能・充足可能の意味
充足可能であるとは、条件群を同時に満たせる割当が存在する状態を意味する。逆に充足不可能であれば、どの割当を選んでも少なくとも1つの条件が破綻する。後者は、制約同士の衝突が本質的であることを示す。
2 代表的なSATの種類
SATには、入力の表現や制約の構造に応じたさまざまな派生形がある。これらは理論的な分類だけでなく、実装上の扱いやすさ、探索の効率にも影響を与える。
2.1 分類の観点
分類は、式の記述方法や変数への制約の強さなど、複数の尺度で行われる。用途によって重視される観点が異なり、適切な分類は問題理解に役立つ。
2.1.1 形式（CNF以外の表現）
CNFが最も一般的だが、一般の論理式や別の正規形で与えられる場合もある。これらは必要に応じて標準形式へ変換されるが、変換過程で式の大きさや構造が変わることがある。
2.1.2 変数の制約条件
問題によっては、各変数が現れる回数や符号の偏りに制約がある。こうした制限は、理論的には難易度の境界を考える手がかりとなり、実務では問題構造の特徴を表す指標になる。
2.2 代表例
SATの代表例には、式が解を持つかを直接問う基本形だけでなく、全解探索や他の最適化課題と結び付くものがある。いずれも、真偽割当を中心に据えている点が共通している。
2.2.1 充足性判定
最も基本的な形は、与えられた式が充足可能かを判定するSATである。これは、解の存在を問う単純な設定でありながら、計算量理論や自動推論の中心的話題になっている。
2.2.2 全解探索と最適化との関係
SATは解の存在判定に焦点を当てるが、実際の応用では全ての解を列挙したり、追加条件の下で最良の解を探したりすることがある。こうした拡張は、制約充足問題や最適化問題との接点を形成する。
2.3 リテラル数や構造による性格
式の構造は、理論上の難しさと実際の解きやすさの双方に関係する。節の長さ、変数の分布、依存関係の密度などが、探索の挙動を左右する。
2.3.1 節のサイズ（k-SAT）
k-SATは、各節にちょうどk個のリテラルが含まれる形を指す。特に3-SATは代表的な形式としてよく知られ、計算量理論における基準問題として利用される。
2.3.2 変数出現の偏りと難しさ
ある変数が多くの節に現れる場合、その変数の値が広範囲に影響する。偏りが強い構造では、局所的な選択が全体へ波及しやすく、探索木の形や解法性能に差が生じる。
3 解法アプローチ
SATの解法は、論理的推論を段階的に積み重ねながら、矛盾を早期に発見する方向に発達してきた。実際のソルバーでは、探索、伝播、学習、簡約が組み合わされる。
3.1 体系的探索
体系的探索は、候補となる割当を順に調べつつ、矛盾する分岐を切り捨てる方法である。無駄な試行を減らす工夫が重要で、単純な総当たりより大幅に効率的である。
3.1.1 部分割当による枝刈り
一部の変数だけを決めた段階で、すでに満たせない節が見つかることがある。この場合、その分岐以下をまとめて除外できるため、探索空間を圧縮できる。
3.1.2 再帰探索とバックトラック
再帰探索では、ある変数に値を入れた後、残りの式を同様に処理する。矛盾が生じたら直前の分岐点へ戻り、別の値を試す。これがバックトラックであり、SATの基本的な探索戦略の一つである。
3.2 代表的アルゴリズム
実用的なSATソルバーの多くは、古典的な分岐探索を土台にしつつ、学習と伝播の仕組みを組み合わせている。代表例として、DPLL系とCDCL系が挙げられる。
3.2.1 DPLL系の考え方
DPLL系は、分岐、単位伝播、純リテラル除去などを用いる古典的枠組みである。論理式を部分的に確定しながら探索することで、単純な列挙法よりはるかに効率よく解を見つける。
3.2.2 CDCL（競合学習）系の枠組み
CDCLは、矛盾が起きたときにその原因を解析し、新しい節を学習して同じ失敗を繰り返しにくくする方法である。現代のSATソルバーの中心技術であり、探索の再利用と早期打ち切りに強みを持つ。
3.3 変換と簡約
入力式は、そのまま解くよりも、扱いやすい形に整えることで性能が向上することが多い。簡約は、意味を保ちながら式を縮めたり、推論しやすい状態にしたりする操作である。
3.3.1 単位伝播の活用
単位伝播は、ある節に1つの未確定リテラルしか残っていないとき、その値が強制される性質を利用する。これにより、連鎖的に多くの変数が決まり、探索前に矛盾が判明することもある。
3.3.2 強制条件と簡約規則
強制条件とは、ある値を選ぶ以外に整合的な道がない状況を指す。簡約規則は、冗長な節の除去や固定された変数の整理などを含み、式の骨格を保ちながら計算負荷を下げる。
4 実用と応用
SATは理論上の研究対象にとどまらず、実際の問題を記述し解くための汎用手段として使われている。制約の記述が適切なら、異なる分野の課題を同じ解法基盤で扱える。
4.1 SATソルバーの利用
SATソルバーは、論理式を入力として受け取り、充足可能性の判定や解の出力を行うプログラムである。利用には、問題を論理式へ翻訳する作業と、返された結果を元の意味へ戻す作業が伴う。
4.1.1 入力作成（モデル化）の流れ
モデル化では、現実の条件を変数と節に対応付け、論理式として表現する。制約の抜けや過剰な表現があると結果の解釈が難しくなるため、入力設計は性能だけでなく正確さにも影響する。
4.1.2 出力の解釈（割当の読み取り）
ソルバーの出力は、変数ごとの真偽値の一覧として示されることが多い。この割当を元の問題設定に戻して読むことで、どの条件がどのように満たされたかを確認できる。
4.2 応用分野
SATは、制約を論理式に変換できる多様な課題に適用される。特定分野の専用手法と比べても、表現の柔軟さとソルバー技術の成熟が利点となる。
4.2.1 制約充足としての問題整理
複雑な条件付きの課題は、SATとして整理することで、個別の規則を統一的に扱える。これにより、問題の構造が明確になり、解の存在確認や候補生成がしやすくなる。
4.2.2 プログラム検証・スケジューリング
プログラム検証では、実行経路の整合性や不変条件の確認にSATが利用される。スケジューリングでは、時間的制約や資源制約を論理条件に落とし込み、実行可能な配置を探す。
4.3 性能評価の指標
SATソルバーの性能は、単一の数値ではなく複数の観点で評価される。入力の性質によって結果が変わるため、総合的な見方が必要である。
4.3.1 実行時間とメモリ使用量
最も基本的な評価指標は、解答までに要する時間と消費する記憶領域である。高速でもメモリを大量に使う場合があり、実用では両者のバランスが重要になる。
4.3.2 ベンチマークと難度の評価
ベンチマークは、複数の問題例を用いて性能を比較するための標準的な試験集合である。難度の評価では、式のサイズだけでなく、構造や変数依存の複雑さも考慮される。