UNSAT Core（充足不能コア）とは、SAT（充当可能性問題）において、問題全体が「満たせない（UNSAT）」状態になっているときに、その矛盾を引き起こしている直接的な原因（節や制約）の最小限の集まりのことです。
たとえるなら、膨大なルールの法律書（CNF問題）を読んだときに、全体として矛盾が生じている原因が、「たった3つの条文（UNSAT Core）が互いに矛盾しているせいだった」と突き止めるようなものです。
🔍 具体例で見る UNSAT Core
次のような 4 つの節（Clauses）からなる CNF 形式の問題があるとします。
- 節1:
x1である。 (1) - 節2:
x1ならばx2である。（\(\neg x1 \lor x2\)） - 節3:
x2は偽である。（\(\neg x2\)） - 節4:
x3またはx4である。（\(x3 \lor x4\)）
1. 全体の判定
この問題にすべての条件を満たす真偽値の割り当て（SAT）を探すと、節1・2・3の間で論理的な矛盾が発生するため、結果は UNSAT（充足不能） になります。 [1]
2. 原因（UNSAT Core）の特定
ここで注目すべきは、節4（
矛盾を発生させている真犯人は、【節1, 節2, 節3】の組み合わせだけです。
x3 または x4）は、この矛盾に一切関係していないという点です。矛盾を発生させている真犯人は、【節1, 節2, 節3】の組み合わせだけです。
このとき、
{節1, 節2, 節3} のセットを「UNSAT Core」と呼びます。💡 なぜ UNSAT Core が重要なのか？
SATソルバーを実務や研究（システムの検証、プログラムのバグ発見、回路設計、スケジューリングなど）で使う際、ただ「この条件では不可能です（UNSAT）」と言われるだけでは、「どこを修正すればいいのか」が分かりません。
UNSAT Core を抽出することで、以下の大きなメリットが得られます。
- デバッグ・修正の効率化:
数百万行ある膨大な制約の中から、矛盾に関係している「数十行の制約」だけを絞り込めるため、どこを直せば仕様を満たせるのかがすぐに分かります。 - 不要なルールの特定:
システムの仕様同士が衝突している場所（設計ミス）をピンポイントで特定できます。
🛠️ 2つの「UNSAT Core」の種類
ツール（drat-trim など）でコアを抽出する際、文脈によって2つのレベルがあります。
- MUS（Minimal Unsatisfiable Subscript / 最小充足不能部分集合）
- そのコアからどれか1つでも節を外すと、矛盾が消えて（SATに）なってしまうような、極限まで削ぎ落とされた原因のセット。
- 一般的な UNSAT Core
- ソルバーが探索の過程で見つけた「矛盾に関わった節の集まり」。MUSほど厳密に最小化されていない場合もありますが、実用上は十分に小さく絞り込まれています。
Q. drat-trimは、MUSを出力するか？
結論から言うと、
drat-trim は「一般的なUNSAT Core」を出力しますが、厳密な「MUS（最小充足不能部分集合）」を必ず出力するとは限りません。 [1]drat-trim が行う処理は Trimming（トリミング：削減） であり、正確には 「MUSに近いサイズまで大幅に削ぎ落としたUNSAT Core」 を出力するツール です。 [1, 2, 3, 4]その理由と、MUSを得るための具体的なアプローチについて解説します。
1.
drat-trim の内部の仕組み（なぜMUSにならないのか）- 判定: 矛盾の証明に「実際に使われた節」だけをマークする。
- 結果: 探索中に1度も使われなかった節はすべて排除される。 [1]
この時点で、元のCNFから不要な節が90%〜99%以上削られた非常に小さなUNSAT Coreが得られます。しかし、探索中に「たまたま余計に使われてしまった節（なくても矛盾が証明できる節）」が残ってしまうことがあるため、数学的な意味での「これ以上1つも削れない状態（MUS）」の保証には至りません。 [1, 2, 3]
2.
drat-trim を何度も回してMUSに近づけるアプローチ [1]
