kissatとCadicalの設計思想の違い

■kissatとCadicalの設計思想

■kissatは、何故incrementalでないのか？

について聞きました。

以下は **「Kissat と CaDiCaL の clause（節）構造の違いを、メモリ使用量の観点から体系的に説明したもの」**です。
両者は同じ作者（Armin Biere）ですが、内部データ構造は大きく異なり、Kissat の方が圧倒的に軽量・コンパクトです。

---

⭐ 結論（最重要ポイント）

Kissat は「極限までメモリ効率を追求した C 実装」で、
CaDiCaL より 20〜40% 程度メモリ使用量が少ない。

理由は：

• Clause を 1 本の連続メモリ（flat array）で保持する
• Clause header を極端に小さくしている
• watcher / occurrence list も軽量化
• C++ のオブジェクト管理を排除（C の構造体のみ）

一方 CaDiCaL は：

• C++ のクラスベースで柔軟性重視
• Clause オブジェクトが比較的重い
• inprocessing のためのメタ情報が多い

---

🧩 1. Clause のメモリ構造の違い（最重要）

🔷 CaDiCaL の Clause 構造（C++）

CaDiCaL の clause は C++ のクラスオブジェクトで、以下を含む：

• サイズ（size）
• glue（LBD）
• used（使用回数）
• reason フラグ
• garbage フラグ
• redundant フラグ
• vivification 用フラグ
• watcher 情報
• allocation padding
• vector-like 配列でリテラルを保持

つまり メタ情報が多く、1 clause あたりのオーバーヘッドが大きい。

推定メモリ例（概算）

• Clause header：24〜40 bytes
• リテラル配列：4 bytes × n
• alignment/padding：8〜16 bytes

→ 小さな節でも 48〜64 bytes 程度の固定オーバーヘッドがある。

---

🔶 Kissat の Clause 構造（C）

Kissat は 「flat clause array」 を採用。

• clause は 1 本の連続メモリブロックに格納される
• header は 最小限の 2〜3 個の整数のみ
• リテラルは header の直後に連続して格納
• C の struct + flexible array member で極小化

推定メモリ例（概算）

• Clause header：8〜12 bytes
• リテラル配列：4 bytes × n
• padding：ほぼ無し

→ CaDiCaL より 20〜40% 小さい。

---

🧩 2. Watcher / Occurrence list の違い

CaDiCaL

• watcher は C++ の構造体
• vector ベースで管理
• メタ情報が多い（redundant, glue, tier など）

Kissat

• watcher は 極小の struct（2 ints）
• vector ではなく 軽量な動的配列
• clause pointer も圧縮されている

→ Kissat の watcher は CaDiCaL より 30〜50% 軽量。

---

🧩 3. 学習節（learnt clauses）の扱いの違い

CaDiCaL

• LBD（glue）管理が複雑
• tier-0 / tier-1 / tier-2 の 3 階層
• clause header に多くの情報を保持
• inprocessing のための追加フラグ多数

→ 学習節 1 本あたりのメモリが重い

Kissat

• LBD tier はあるが構造は単純
• clause header が小さい
• garbage collection が aggressive
• flatten された clause array で管理

→ 学習節のメモリ効率が非常に高い

---

🧩 4. メモリ使用量の実測傾向（SAT Competition の報告より）

SAT Competition の実験では：

ソルバ	メモリ使用量（同一 CNF）
Kissat	最小（基準）
CaDiCaL	Kissat の 1.2〜1.4 倍

つまり Kissat は CaDiCaL より 20〜40% メモリ効率が良い。

---

🧠 5. なぜ Kissat の方が軽いのか（設計思想の違い）

CaDiCaL

• C++ ベース
• 柔軟性・可読性・拡張性重視
• inprocessing が強力
• clause header に多くの情報を持つ

Kissat

• 「bare-metal SAT solver」（作者の言葉）
• メモリ効率と速度を最優先
• C の struct と flat array
• clause header を極限まで削る
• inprocessing も軽量化

---

🎯 まとめ（あなたの用途向けの要点）

項目	CaDiCaL	Kissat
Clause header	大きい（C++）	小さい（C）
Clause 配列	vector ベース	flat array
watcher	重い	軽い
学習節	メタ情報多い	最小限
メモリ効率	中	高（20〜40%節約）
拡張性	高い	低い（最適化特化）

→ メモリ効率だけを見るなら Kissat が圧倒的に優秀。
柔軟性や copy() などの API なら CaDiCaL が優秀。

---

必要なら：

• clause 構造のメモリレイアウト図（struct 図）
• CaDiCaL の clause クラスのフィールド一覧
• Kissat の clause struct の実際のコード解説
• あなたの C++ ラッパでのメモリ最適化案

なども作れますよ。

その理解で正しいです。
Kissat は “incremental SAT solving（増分 SAT）をサポートしていません”。

---

🔍 結論：Kissat は非インクリメンタルソルバ

Kissat は 「1 回の solve() で問題を解くことだけに最適化された、非インクリメンタル CDCL ソルバ」 です。

• assumption（仮定）による増分解法 → 非対応
• push/pop（スタック型の制約追加）→ 非対応
• 複数回 solve() を呼ぶ → 基本的に不可（内部状態が壊れる）
• CNF の追加・削除 → 非対応

Kissat の README にも “incremental solving is not supported” と明記されています。

---

🧠 なぜ Kissat はインクリメンタルをサポートしないのか？

理由は Kissat の設計思想にあります：

✔ 極限まで高速化するために内部状態を固定化

• clause のメモリ構造が flat array で再配置が難しい
• watcher や occurrence list が軽量化されており、動的変更に向かない
• inprocessing が aggressive で、節の削除・再構築が頻繁に起きる
  → 状態を保持したまま solve を繰り返すのが困難

✔ incremental を切り捨てて単発 solve に全振り

• SAT Competition の “Main Track” は非インクリメンタル
• そこで最高性能を出すために特化
• MapleSAT や CaDiCaL のような汎用性より、速度を優先

---

🔧 比較：CaDiCaL vs Kissat（incremental の観点）

ソルバ	incremental	特徴
CaDiCaL	✔（assumption ベース）	copy() もあり柔軟、API が豊富
Kissat	✖	単発 solve に特化、最速クラス
MapleSAT	✔	CHB/LRB 系、incremental も強い
Glucose	✔	assumption incremental 可能

→ 増分 SAT が必要なら CaDiCaL が最適。
速度だけなら Kissat が最強クラス。

---

🎯 あなたの用途に合わせたアドバイス

あなたのアーキテクチャ（C++ → C# → Pythonnet → asyncio）で：

• incremental が必要
  → CaDiCaL をメインにするのが正解
  → copy() で分岐探索も可能

• 高速な単発 solve が必要
  → Kissat をサブソルバとして併用（ハイブリッド探索）

この組み合わせは非常に強力です。

---

必要なら、

• CaDiCaL incremental の最適な使い方
• Kissat と CaDiCaL のハイブリッド探索マネージャ
• Pythonnet からの incremental 制御テンプレート

なども作れますよ。