UNSATコアとは

 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（x3 または x4）は、この矛盾に一切関係していないという点です。
矛盾を発生させている真犯人は、【節1, 節2, 節3】の組み合わせだけです。

このとき、{節1, 節2, 節3} のセットを「UNSAT Core」と呼びます。

---

💡 なぜ UNSAT Core が重要なのか？

SATソルバーを実務や研究（システムの検証、プログラムのバグ発見、回路設計、スケジューリングなど）で使う際、ただ「この条件では不可能です（UNSAT）」と言われるだけでは、「どこを修正すればいいのか」が分かりません。

UNSAT Core を抽出することで、以下の大きなメリットが得られます。

• デバッグ・修正の効率化:
  数百万行ある膨大な制約の中から、矛盾に関係している「数十行の制約」だけを絞り込めるため、どこを直せば仕様を満たせるのかがすぐに分かります。
• 不要なルールの特定:
  システムの仕様同士が衝突している場所（設計ミス）をピンポイントで特定できます。

🛠️ 2つの「UNSAT Core」の種類

ツール（drat-trim など）でコアを抽出する際、文脈によって2つのレベルがあります。

1. MUS（Minimal Unsatisfiable Subscript / 最小充足不能部分集合）
   • そのコアからどれか1つでも節を外すと、矛盾が消えて（SATに）なってしまうような、極限まで削ぎ落とされた原因のセット。
2. 一般的な 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にならないのか）

drat-trim は、ソルバーが出力した「証明ログ（DRAT）」を、最後の矛盾点（空節）から逆方向にトレース（Backward Checking） します。 [1]

1. 判定: 矛盾の証明に「実際に使われた節」だけをマークする。
2. 結果: 探索中に1度も使われなかった節はすべて排除される。 [1]

この時点で、元のCNFから不要な節が90%〜99%以上削られた非常に小さなUNSAT Coreが得られます。しかし、探索中に「たまたま余計に使われてしまった節（なくても矛盾が証明できる節）」が残ってしまうことがあるため、数学的な意味での「これ以上1つも削れない状態（MUS）」の保証には至りません。 [1, 2, 3]

2. drat-trim を何度も回してMUSに近づけるアプローチ [1]

drat-trim の機能を利用して、極限までMUSに近づける（あるいはMUS化する）ために、研究や実務ではループ（反復クレンジング）という手法が使われます。 [1]