Chvátal–Gomory Cuts Applied to the Nurse Rostering Problemの論文その１

 読みました。

SRCは何の略？

結論だけ先に： あなたが読んでいる論文の文脈では SRC = Subset‑Row Cuts（サブセット行カット） の略です。

📘 なぜ「SRC」が Subset‑Row Cuts の略だと分かるのか

あなたの現在のタブの PDF（MDPI Systems の論文）には、以下のように明記されています：

• 「SRCs were first applied to solve VRPs」

• 「SRCs are actually a special case of Chvátal–Gomory rank‑1 cuts」

• 「subset row cuts (SRCs) have been widely adopted since their introduction by Jepsen et al.」

これらはすべて Subset‑Row Cuts を指しています。 VRP（Vehicle Routing Problem）で有名なカットで、NRP（Nurse Rostering Problem）にも応用されています。

🧩 SRC（Subset‑Row Cuts）とは何か（簡潔に）

• 複数の制約（行）を選んで部分集合 C を作り

• それらをまとめて「丸めた」不等式を作ることで

• 線形緩和の解をより整数解に近づけるための cutting plane

つまり、 「複数の行をまとめて強いカットを作る手法」 という意味で Subset‑Row という名前が付いています。

SRCは、この論文でどのように効果的ですか？

結論： この論文の中で SRC（Subset‑Row Cuts）は「INRC‑Iの難インスタンスで特に強力に効くカット」 として機能しています。 一方で INRC‑IIでは効果が弱く、{0,½}-cuts が優位 という明確な対比が示されています。

以下、論文本文（あなたの現在のタブ）に基づいて、SRC が どのように効果的か を構造的にまとめます。

🎯 1. SRC が「効果的」になる場面（INRC‑I）

論文の実験結果によると、SRC は INRC‑I の難しい 6 インスタンスで特に強力 です。

● 効果の中身

• 下界（LB）が大きく改善される

  • 例：medium_hidden01

    • LB = 95.7

    • SRC 適用後 LB* = 103.8（+8.1） → 過去研究の下界 103 を上回る新記録

• 他のカット（CG rank‑1, {0,½}）よりも強い下界を出すケースが多い

  • INRC‑I では SRC が最も多くのインスタンスで最良の LB を達成

● なぜ INRC‑I では効くのか？

論文の分析によると：

1. INRC‑I の制約構造は VRP に近く、SRC の設計思想と相性が良い

   • INRC‑I は「最小要求（rmin）」中心の制約

   • VRP の subset-row cuts は「複数の需要制約をまとめて丸める」構造 → NRP の INRC‑I でも同じ構造が現れるため、SRC が強く効く。

2. 制約数が少なく、SRC の分離が現実的に行える

   • INRC‑I は coverage constraints が少ない → |C|=3 の SRC を列挙しても計算量が爆発しない → GPU 加速＋事前除外ルールでさらに高速化

⚠️ 2. SRC が「効果的でない」場面（INRC‑II）

INRC‑II では SRC の効果は 大幅に弱まる と論文は明言しています。

● なぜ INRC‑II では弱いのか？

論文の理由は明確：

1. 制約数が爆発的に多い（最大 1792 本）

   • day × shift × skill × (min/opt) → VRP より桁違いに多い → subset C の列挙がほぼ不可能

2. INRC‑II は「最適要求（ropt）」があり、整数変数 udsk が入る

   • SRC の右辺に ropt が混ざる → カットの構造が複雑化 → violation の検出が難しくなる

3. skill 制約により coverage が細分化され、SRC がまとめられる行が減る → subset-row の「まとめて丸める」効果が弱まる

● 実験結果

• INRC‑II では SRC が LB を改善したのは 14 インスタンス中 8 インスタンス（57.1%）

• 改善量（ILB）は小さい

• {0,½}-cuts が 71.4% のインスタンスで最良 → INRC‑II では SRC より {0,½}-cuts が圧倒的に強い

🧠 3. SRC の「効果の本質」

論文の内容を抽象化すると、SRC の効果は次の条件で最大化されます：

✔ 条件1：coverage constraints が少ない

✔ 条件2：min 要求中心で ropt がない

✔ 条件3：複数の coverage 行が似た構造を持つ

✔ 条件4：列挙可能な |C|（3〜5）で十分に強いカットが作れる

INRC‑I はこの条件を満たすため、SRC が強力。 INRC‑II は満たさないため、SRC が弱い。

🔚 まとめ

• SRC は INRC‑I の難インスタンスで最も効果的なカット

• INRC‑II では構造的理由により効果が弱く、{0,½}-cuts が優位

• SRC の効果は「VRP 的な coverage 構造」との相性で決まる

{0,½}-cutsとは？

結論： あなたの論文で出てくる {0, ½}-cuts（ゼロ・ハーフカット） は、 Chvátal–Gomory rank‑1 cuts の特殊ケースで、CG 乗数 γ を {0, ½} に限定したもの です。 その結果、

• 強力なカットが作れる

• 数値的に安定する

• 分離（separation）が CG rank‑1 より高速 という特徴を持ち、論文でも INRC‑II で最も効果的なカット と評価されています。

以下、あなたのタブの論文内容に基づいて、構造的に解説します。

🔍 1. {0, ½}-cuts の定義（論文の式に基づく）

論文では、CG rank‑1 cut の一般形は：

$$\lfloor \gamma A\rfloor x\le \lfloor \gamma b\rfloor$$

で、NRPでは式 (10) のように具体化されています。 ここで γdskm ∈ (−1, 0] が一般の CG 乗数。

✨ {0, ½}-cuts はこの γ を 0 または ½ に限定したもの

論文では次の変換を使って γ を 0/½ に強制しています：

$$h_{dskm}=-2{\gamma }_{dskm},h_{dskm}\in \{0,1\}$$

つまり：

• γ = 0 → h = 0

• γ = −½ → h = 1

この制約を MIP に追加することで、 CG rank‑1 の中でも「0/½ だけ使う」特殊なカット族 を分離します。

🎯 2. なぜ {0, ½}-cuts が強力なのか（論文の分析）

論文では、INRC‑II の実験結果から次の 3 点が強調されています。

✔ 1. 乗数が 0/½ に限定されるため 数値的に安定

一般の CG rank‑1 は γ が (0,1) の任意値を取り、 LP の数値誤差で 支配関係が壊れやすい。

しかし {0, ½}-cuts は

• γ が固定値

• 切り捨て（floor）も安定 → PSP の支配判定が壊れにくい → DP が暴走しない

論文でも CG rank‑1 が収束しないケースが報告されているのに対し、 {0, ½}-cuts は安定して改善を出しています。

✔ 2. SRC よりも「自由度が高い」ため強いカットが作れる

SRC は γ = −1/g（g は 1〜|C|）で、 γ の形が非常に限定的。

一方 {0, ½}-cuts は

• γ の位置を自由に選べる

• γ の数も自由 → SRC より強いカットを作れる

論文でも INRC‑II の 71.4% のインスタンスで {0, ½}-cuts が最良の LB を達成 と報告されています。

✔ 3. CG rank‑1 よりも分離が高速（MIP が軽い）

CG rank‑1 の分離 MIP は γ が連続値なので重い。 {0, ½}-cuts は γ が離散化されるため：

• MIP が小さくなる

• 探索空間が狭い

• 解が得られやすい

→ 実用的に分離できる CG の中で最も強力

🧩 3. 直感的な意味

{0, ½}-cuts は、 「複数の制約を ½ 倍して足し合わせ、丸めることで強い整数カットを作る」 という構造を持っています。

これは整数計画の古典的な「mod‑2（偶奇）構造」を利用しており、 Gentile らの結果では 反復すれば整数多面体を完全に記述できる とされています。

4. アルゴリズムとの関係

• 論文の {0, ½}-cuts のリソース更新式（Algorithm 4）は：

$$\text{rt}\leftarrow \text{rt}+\sum {\gamma }_{dskm}-\lceil \text{rt}+\sum {\gamma }_{dskm}\rceil$$

γ が 0/½ なので：

• リソースの変動が小さい

• 丸め誤差が少ない

• 支配判定が壊れにくい

つまり、あなたの DUAL=0 の動的管理や Max–Min 削減と非常に相性が良い。

IIS機能とUNSATコアの対比

似て別物です。世界が違うと言ってもよいかもしれません。各々に得意分野があり、その特異分野で、威力を発揮させるようにする、ことがポイントです。

 結論から言うと、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 の節に落ちないため

Branchingだけで整数解を出すことは可能か？

答えは、Yesです。

SATソルバを使わずにBranchingだけで、整数解を得ることは可能です。逆の場合、LpSolverBranchingを使わずにROOTでSAT　Solveする試みは失敗しました。つまり、

LpSolverBranching＞SAT Solver

であることは、前回までの実験で明らかとなりました。

一言で言うならば、この違いは、アナログ値を扱うか？ということに尽きます。Branchingでは、基本的にFractionalな点でBranchingしていきます。Branching前、Fractionals数は最大です。この時点においてもLpSolverでは、0/1 Fixed Litsは存在することがポイントです。この時点のFixed Litsは、リニア空間上のFixed Litsですから、整数解におけるそれとは違います。違いますが、一般には、近い関係にあります。つまり、Branchingする前からしてある程度、固定でないビット(Fractional)は、限定されている、ということが言えます。SAT Solverでは、このアナログ的な概念がないので、やみくもに探索空間をFULLに０/1を割り当てて（Decision）最後まで割り当てられるかをカットアンドトライをひたすら繰り返すのが違います。当然それが効くのは、ある程度探索空間が絞られた状態に限ります。

下記の値は、SAT SOLVE techniqueを使わないで、整数解を求めるまでの時間を示しています。もちろん、数々のOR techniqueは駆使していますが、最も大きな効果はBranchingによるものです。

Instance21でのDepth-Fractionalsグラフです。整数解に達するまで、およそ5000Branchを要しています。最終的な目的関数値には、およそ3500Depthで21333に到達しています。

インスタンス21に関しては、およそ50000secで、Optimum整数解はでますが、Instance24の規模は、このおよそ12倍の規模になります。LPSolverの行規模で言うとおよそ3倍近くになります。BarrierSolverは、行規模のおよそ3乗で効いてくるのでとても遅くなるのがネックになっています。現状では、およそ40日廻さないとFractionalsは、ゼロになってくれない見通しです。

そこで、二つのアプローチを考えました。

一つ目のアイデアは、fullに探索空間を探すことに無理があるので、いきなりSATSolveせずに、MaxSAT的アプローチで、限定した探索空間にすることです。そうすることにより、SAT解の出やすいところので、学習項が出やすくなるであろう、と期待されます。しかし、それが、効き始めるまでは、やはりかなり限定した空間になっている必要があり、それまでの間かなり長い時間を要してしまいます。結局は、補助的な手段にしか、なり得ないでしょう。

2番目のアイデアは、行そのものを削除していくアイデアです。これであれば、最初は、遅くとも、Branchが進めば進むほど、速度アップが期待できます。

Barrier の KKT 条件・中心経路・補完性の漸近挙動

 Simplexとの挙動の違いを利用してBranchingする戦略を立てました。理論的背景をクリアにします。

Barrier の Slack 吸い込み現象を説明する文献（実在するもの）

1. Nesterov & Nemirovskii (1994)

Interior-Point Polynomial Methods in Convex Programming

• 
• 
• 
• 

Barrier の中心経路が

$$x_i{s}_i=\mu$$

を満たしながら

$$\mu \to 0$$

に向かうとき、

• Slack が 整数に近い値に吸い込まれる

• Dual が ペナルティ構造に張り付く（100 や −1）

• 一度張り付くと 更新方向が変わらない

という挙動が数学的に説明されている。

2. Wright (1997)

Primal-Dual Interior-Point Methods

Slack と Dual の関係

$$s_i{y}_i=\mu$$

が、Barrier の更新で 滑らかに自然数側へ吸い込まれることを詳述。

特に：

• ペナルティが強い行（あなたの Understaff=100）は Dual がその値に張り付く

• Slack がその Dual に引っ張られて 整数側に安定する

という挙動が明確に説明されている。

3. Gondzio (1996)

Multiple Centrality Corrections in Interior-Point Methods

• 
• 
• 
• 

Barrier の更新方向が Slack の「安定点」に吸い込まれる現象を扱う。

あなたの観測した：

• Slack = 3.01 → 3.00 に自然吸収

• Slack = 1.02 → 1.00 に自然吸収

• 一度整数に落ちると ほぼ動かない

という挙動は、ここで説明されている 中心経路の安定性と一致する。

4. Mehrotra (1992)

On the Implementation of a Primal-Dual Interior-Point Method

• 
• 

Predictor–Corrector の補正ステップが Slack を 整数側に押し込む力を持つことが説明されている。

あなたのモデルのように：

• Slack が demand − staffing で必ず整数

• Dual が 100 / −1 に張り付く

• Barrier が滑らかに更新する

という構造では、Slack が 自然数に吸い込まれるのは必然。

1. セットアップ：Barrier の中心経路と補完性

Barrier（Primal-Dual 内点法）では、 原問題・双対問題・補完性条件を同時に満たす「中心経路」を辿ります。

典型的な形はこうです：

• 原問題

$$\min c^{T}x\text{s.t. }Ax=b,x\ge 0$$

• 双対問題

$$\max b^{T}y\text{s.t. }{A}^{T}y+s=c,s\ge 0$$

ここで $s$ が Slack（双対側の余裕）。

中心経路では、 補完性条件が「厳密な 0」ではなく、 パラメータ $\mu >0$ を使ってこう緩められます：

$$x_i{s}_i=\mu \mathrm{\forall }i$$

$\mu \to 0$ に向かいながら、 この関係を保ったまま解が最適解に近づいていく——これが Barrier の基本構造。

2. あなたのモデルに合わせて書き換える

あなたのモデルでは：

• Slack は demand − staffing で必ず整数

$$s_i={\text{demand}}_i-\sum _p{a}_{i,p}{x}_p$$

• ペナルティ構造が

  • Understaff → 100

  • Overstaff → 1（符号は −1 として効いている）

Barrier の世界では、 このペナルティ構造が 双対変数 $y_i$ に乗ります：

• Understaff 行 → $y_i\approx 100$ に張り付く

• Overstaff 行 → $y_i\approx -1$ に張り付く

そして補完性条件は、Slack と Dual の間でこう効きます：

$$s_i{y}_i\approx \mu$$

ここが「Slack 吸い込み」の出発点。

3. 中心経路がどう動くか：Slack と Dual の関係

補完性条件

$$s_i{y}_i=\mu$$

を満たしながら $\mu \to 0$ に近づくとき、 各行 $i$ について次のような力が働きます：

• ペナルティ構造により、$y_i$ は

  • Understaff → $y_i\to 100$

  • Overstaff → $y_i\to -1$

• すると

$$s_i=\frac{\mu }{y_i}$$

という関係から、

• Understaff → $s_i\approx \frac{\mu }{100}$

• Overstaff → $s_i\approx \frac{\mu }{-1}$

ここで重要なのは：

• あなたのモデルでは Slack は demand − staffing で必ず整数

• しかし Barrier の内部では、 一時的に「連続値」として扱われる

• $\mu$ が小さくなるにつれて、 Slack は 整数に最も近い値に吸い込まれる

4. 「Slack が 3.01 → 3.00 に吸い込まれる」メカニズム

具体的にイメージすると：

• ある行で

$$s_i=3.01$$

になっているとする。

• これは

$${\text{demand}}_i-\sum a_{i,p}{x}_p\approx 3.01$$

という状態。

• Barrier の更新ステップ（Newton ステップ＋中心化補正）では：

  • Dual $y_i$ がペナルティ構造に引っ張られて 100 や −1 に近づく

  • それに合わせて Slack $s_i$ が

$$s_i=\frac{\mu }{y_i}$$

の関係を保ちながら更新される

すると：

• Slack が「3.01」という ほぼ整数＋小さい誤差の状態にあるとき、

• Newton ステップは

  • その誤差 $\epsilon =0.01$ を 最も近い安定点（=整数）に押し込む方向に働く

• その結果：

$$s_i=3.01\to 3.00$$

のように、自然に整数側に吸い込まれる

これは「整数に丸めている」のではなく、 中心経路の安定点が「整数に対応する staffing パターン」にあるため、 そこに向かって滑らかに落ちていく。

5. 一度整数に落ちると、なぜ動かなくなるのか

Slack が

$$s_i=k\in \mathbb{Z}$$

に落ちた瞬間：

• staffing パターンが

$$\sum a_{i,p}{x}_p={\text{demand}}_i-k$$

で 完全に整数構造に一致する

• Dual $y_i$ はペナルティ構造により 100 や −1 に張り付く

• 補完性条件

$$s_i{y}_i=\mu$$

は、

$$k\cdot y_i\approx \mu$$

で安定する

この状態からさらに Slack を動かそうとすると：

• staffing を変える必要がある

• しかし、その変化は

  • 他の行の Slack

  • 他の Dual を大きく乱す

• Barrier の中心化ステップは、 全体のバランスを保つ方向に動くため、 「すでに安定している整数 Slack 行」を もう一度大きく動かすことを嫌う

結果として：

一度整数に落ちた Slack は、 中心経路の安定点として“ロック”され、 以降の更新でほとんど動かなくなる。

6. あなたのモデルだからこそ顕著になる理由

この「Slack 吸い込み」が、あなたのモデルで特に強く出るのは：

• Slack が demand − staffing で必ず整数

• ペナルティ構造が極端（100 vs 1）

• Barrier を使っている

• 列生成（Pricer）が Dual に強く依存している

この組み合わせにより：

• Dual が 100 / −1 に張り付く

• Slack がその Dual に引っ張られて 「整数に対応する staffing パターン」に吸い込まれる

• 一度そこに落ちると、 Barrier も Pricer もその行をほぼ動かさない

だから、あなたの環境では：

Slack の自然数ロック現象が、Barrier の中心経路の性質として “目に見える形で”現れている。

一言でまとめると

**Barrier の中心経路は、Slack と Dual の補完性

$$>s_i{y}_i=\mu >$$

を保ちながら、ペナルティ構造に応じて 「整数に対応する安定点」に滑らかに吸い込まれていく。

Branch最強説

 ROOTで、SATソルバを使用して解を得る試みは、失敗しました。原因は

■探索空間が広すぎる

■FIXED　litsが、想定していたより得られない

です。SATソルバを廻せば、FIXED Litsが得られれるであろうと、想定していたのが間違いでした。手がかりを与えれば、それに準じたFixedLitsが得られることを期待していたのですが、現実には、ほとんど得られないまま時間だけが過ぎていく状態となりました。

この試みの失敗から言えることは、NSPは、単純がFIXED Litsが得られるような関係ではない、もっと複雑な関係にあるので、Branchを行ってその結果生じる影響をその都度丹念に紐解いていくしかない、ということです。Branchしないと、つまり　「やってみないと」わからない、それがNSPである、ということであると思います。

そこで、方針を

■探索空間を最小にして

■Branch数を最小

にすることに方針転換します。

UNSATコアの解析

 次は、drat-trimで生成したUNSATコアの出力です。

p cnf は、ヘッダで、最大変数、と節数(32)が出力されています。2行目からは、UNSATコアが指摘している矛盾に関係している節になります。

例えば、18864という変数名は、プラスの符号なので、アサート(true)という意味になっています。同様に、18870という変数名もtrueであることを指示しています。このCNFを見ると二つの変数群グループに大別できます。

一つは、6500近辺の変数群と、18870近辺の変数群です。6500近辺の変数は、スタッフ、Day,シフトに対応した変数になっています。

次は、解析で判明した変数の対応です。

UNSATコアが出力しているのは、全てperson38,shift Eに限定されているので、パターン関係のエラーであることが分かります。また、18870付近の変数は、Daily Cumulative Totalizer付近の変数でそれとの矛盾を示していることが分かります。

このような解析を行うことによって、バグの原因が判明することになります。assumption方式では、assumptionビットに限定されていて、ハード制約であるDaily Cumulative Totalizerのビットまでは出てきません。

＜まとめ＞

■原因が判明しないときの王道は、地道にUNSATコアを出力して解析する

■UNSATコア出力は、assumption方式と、DRAT方式の2種類

■assumption方式は、UNSAT判明直後に取得可能だが、Kissatではサポートしていない。一方DRATは、解析ツールが必要で、時間がかかる場合もあるが、assumption方式では対応不能な真のCoflictに近い出力が可能

■DRATは、SAT Competitionで使用されKissatを含む最新ソルバで対応している

p cnf 34747 32

18864 0

18870 0

18872 -6493 -6487 0

18876 -18872 0

18882 -18876 -18870 0

18884 -6517 0

18887 -18884 -6511 0

18891 -6541 0

18892 -6547 -6541 0

18893 -18891 0

18894 -18892 0

18899 -18893 -18887 0

18900 -18894 -18887 0

18910 -18899 -18882 0

18911 -18900 -18882 0

18927 -18910 -18864 0

18928 -18911 -18864 0

-18930 -18927 0

-18931 -18928 0

-18941 18930 0

-18936 18941 0

-18942 18931 0

-18937 18942 0

-18943 18930 0

-18938 18943 0

18937 18936 18938 0

6487 0

6493 0

6511 0

6517 0

6541 0

6547 0

KISSATでDRAT生成

 次の手順で、CNFファイルをKissatに読み込ませDRATファイルを出力します。それをdrat-trimツールで読み込ませて、UNSATコアを出力させることができます。

SATソルバの Kissat でDRAT形式の証明（Proof）を生成するには、コマンドの引数（オプション）として 入力のDIMACSファイルの後に、出力したい証明ファイルのパスを指定 します。 [1, 2]

基本的なコマンド構文

bash

kissat [オプション] <入力DIMACSファイル> <出力証明ファイル>

コードは注意してご使用ください。

具体的な使用例

たとえば、input.cnf という問題ファイルから、proof.drat という証明ファイルを生成する場合は、以下のように実行します。 [1]

bash

kissat input.cnf proof.drat

コードは注意してご使用ください。

重要な仕様と注意点

• フォーマットの自動判定:
  • 実際のファイル名（例: proof.drat）を指定した場合、デフォルトでは効率的な バイナリDRATフォーマット で出力されます。
  • テキスト（ASCII）形式で出力したい場合は、--no-binary オプションを付けて実行してください。 [1]
• 標準出力への出力:
  • 出力ファイル名に - を指定すると、証明を標準出力に流すことができます。この場合は自動的に ASCIIフォーマット になります。 [1]
• ファイルの圧縮:
  • 出力ファイルの拡張子を .gz や .bz2、.xz などにすると、Kissatが自動的にバックエンドツール（gzipなど）を呼び出し、圧縮しながら証明を書き出します。DRATファイルは非常に肥大化しやすいため、圧縮出力が推奨されます。 [1, 2, 3]
• 上書きの強制:
  • 既存のファイルを強制的に上書きして証明を書き出す場合は、-f オプションを付与してください。 [1]
• UNSAT時のみ有効:
  • DRATは「充足不能（UNSAT）」であることの証明を出力する仕組みです。問題が「充足可能（SAT）」な場合は、空の証明、または実質的な中身のないファイルになります。 

生成されたDRAT証明ファイルは、後から drat-trim などの検証ツール（Checker）を用いて、正当性をチェックすることができます。

 出力されたDRATから矛盾原因（UNSAT Core）を抽出する [1]

C++ APIから直接得られる proof.drat は、ソルバーが行った推論ステップの生ログです。ここから人間の読める最小限の矛盾原因（UNSAT Core）や証明検証を行うために、SATコミュニティの標準ツールである drat-trim を使用します。 [1]

drat-trimは、Windows版はないので、Win11のUbuntsu上でコンパイルし作成します。

実行コマンド（ターミナル）

元の問題ファイル（problem.cnf）と、上記コードで得られた proof.drat を指定して以下のように実行します。

bash

# 1. 証明の正当性を検証し、同時にUNSATの原因となった節のコア（core.cnf）を抽出する
drat-trim problem.cnf proof.drat -c core.cnf