似て別物です。世界が違うと言ってもよいかもしれません。各々に得意分野があり、その特異分野で、威力を発揮させるようにする、ことがポイントです。
結論から言うと、IIS（Irreducible Infeasible Subsystem） と UNSAT Core は「不整合の最小原因を抽出する」という点で似ているが、
目的・性質・使われる世界（数理最適化 vs SAT/SMT）・最小性の意味 がかなり違います。
実務・アルゴリズム観点での“本質的な違い” をまとめます。
🎯 まず一言で対比
IIS（LP/MIP） → 制約集合の中で「これだけで infeasible になる最小セット」 → 数理最適化ソルバーが使う概念（Gurobi, CPLEX, COPT）
UNSAT Core（SAT/SMT） → 充足不能になる「節（またはアサーション）の部分集合」 → SAT/SMTソルバー（Kissat, Z3, CVC5）が使う概念
どちらも「不整合の原因を最小化して抽出する」機能だが、 最小性の定義が違う のが最大のポイント。
🧩 IIS と UNSAT Core の“最小性”の違い
◆ IIS の最小性（LP/MIP）
除去最小性（minimal） IIS に含まれる制約のどれか 1 つでも除くと実行可能になる
ただし “最小サイズ” ではない（minimum ではない） → 複数の IIS が存在する → ソルバーはそのうちの 1 つを返すだけ
◆ UNSAT Core の最小性（SAT/SMT）
除去最小性（minimal） が基本
さらに SMT では 最小 UNSAT Core（minimum UNSAT core） を求めるアルゴリズムも存在 → サイズ最小化（cardinality minimal） → MUS（Minimal Unsatisfiable Subset）とも呼ばれる
SAT/SMT の世界は「節の集合」が明確なので、 MUS/MCS（Minimal Correction Set） などの理論が発達している。
🏭 実務的な違い
1. IIS は連続制約（LP/MIP）の世界に限定
線形制約
変数の上下限
MIP の integrality も含むが、節レベルの扱いではない
ソルバー内部のフェーズ I/II、Farkas 証明などを使う
2. UNSAT Core は論理式（SAT/SMT）の世界
CNF の節
SMT のアサーション
証明オブジェクト（DRAT, LRAT）を使って抽出
3. Kissat は UNSAT Core を返せるが IIS は返せない
Kissat は SAT ソルバーなので、 UNSAT Core（節の集合） は返せるが、 IIS（LP/MIP の制約集合） は扱えない。
🔧
✔ SAT/SMT の世界では UNSAT Core 抽出は標準機能
Kissat → DRAT 証明を出力 → 外部ツールで UNSAT Core 抽出可能
CaDiCaL → UNSAT Core 抽出機能あり
Z3 →
get-unsat-coreで直接取得CVC5 → UNSAT Core 取得可能
PicoSAT → コア抽出あり
つまり SAT/SMT では UNSAT Core は普通に取れる。
✔ LP/MIP の IIS を SAT ソルバーで代替することはできない
理由：
LP/MIP の制約は論理節ではない
実数・不等式・連続領域が SAT の CNF では表現できない
変換すると SMT（線形算術）になるが、これは別物
🧠 IIS と UNSAT Core の“構造的な違い”を図で示す
IIS（LP/MIP）
制約1: x ≥ 10
制約2: x ≤ 5
制約3: y ≥ 0
制約4: y ≤ 100
IIS = {制約1, 制約2}
UNSAT Core（SAT）
(¬A ∨ B)
(¬B)
(A)
(C ∨ D)
UNSAT Core = { (¬A ∨ B), (¬B), (A) }
🔥 あなたの研究に役立つ“本質的なまとめ”
◆ IIS と UNSAT Core は似ているが別物
IIS = LP/MIP の不整合の最小制約集合
UNSAT Core = SAT/SMT の不整合の最小節集合
◆ SAT ソルバー（Kissat）は UNSAT Core を返せる
DRAT 証明 → コア抽出ツールで可能
◆ IIS を SAT ソルバーで代替することはできない
LP/MIP の構造が SAT の節に落ちないため
0 件のコメント:
コメントを投稿