Cadical CHBを外部からコントロールするAPIを追加

   void set_vars_lowest_priority(std::vector<int> lits);//FEB042026

というAPIをCadicalに追加しました。decide()で、変数を選ぶのですが、基本的には、スコアが高い順番に決められます。ここで、制約している範疇の変数と、そうでない変数とでは、当然制約に関与している変数が先に実行されるべきです。それがスコアだけだとコントロールできないことが問題です。未だ制約が及んでいない変数群については、decide()を後回しして、残った帰結として、決めてやる、ことが理想です。

一方、Cadicalのdefaultモードは、VSIDSとは別にあり、基本的に新しい変数から実行されてしまいます。スコアという概念さえもなく全く外部からコントロール出来ません。

その解決策として、CHBを導入、さらにAPIによるコントロールにより、制約に関係した変数をFirst、関係していない変数を最後に持ってくることを行えるようにします。これは、現在のスケジュールナースが行っている処理であって新しいものではありません。しかしながら、今回、Cadical上では、そのようなAPIは、存在していないので、自前で改造する必要がありました。

SATURATIONの衝撃

NVIDIAの 

Autonomous Code Evolution Meets NP-Completeness

の論文をコパイにまとめてもらいました。

2025優勝ソルバにたいして相当の向上が見られ、それは、単に過去ソルバの良いところ取りに留まらず、自律的新アルゴリズムを発見した、

ということのようです。

これまで、LLMが出来るのは、パラメータの調整だけだと思いこんでいたのですが、間違っていました。

ここまで到達すると、もはや「研究者は不要」、という領域に入ってくるかもしれません。新しいアルゴリズムを考えるより、如何に賢いAIを育てるか？の方が焦点になる可能性があります。

恐らく、2024SATCompetitionが、優勝者が人間だった最後の年で、以降、全てAIになるのではないかと。

SAT Competitionは、SATソルバ界隈での最高競技会でありトップ研究者達の集まりです。

ソースは全てオープンであるが故に、結果、多くの知恵が集まり多くの研究成果が生まれました。しかし、オープンであるが故にAIの餌食となってしまった、とも言えます。人類の知恵は、論文に集積されていますが、数秒で新しい論文を理解してしまう知能と、眠ることのない存在に、もはや勝ち目はないのでは？とも思います。AIと抽象的・数学的・技術的な会話をすること自体は楽しいのですが、どんな話題を振っても、敵うことのないメンター的知性を持った存在、という印象をさらに強く抱いた次第です。

Q.2025優勝ソルバとの比較

結論から言うと 「はい、明確に増えています」。
あなたが開いている論文 “Autonomous Code Evolution Meets NP-Completeness” の記述によれば、SATLUTION は SAT Competition 2025 の Winner（AE_kissat2025_MAB）よりも多くの問題を解いています。 arxiv.org

---

🧩 解けた問題数の比較（論文の記述より）

論文の Figure 2（Cactus Plot）に明確に書かれています：

• SATLUTION のトップ 3 ソルバー

  • 解いた問題数：347, 345, 344

• SAT Competition 2025 Winner（AE_kissat2025_MAB）

  • 解いた問題数：334

• 2nd place（kissat-public）

  • 解いた問題数：331

つまり、SATLUTION は Winner より 10〜13 問ほど多く解いています。
これはかなり大きな差で、特に中〜難問領域（1000〜4000秒帯）で差が開いていると論文は述べています。 arxiv.org

---

📌 まとめ

• 解けた問題数は増えているか？
  → はい、Winner より明確に増えています。

• どれくらい増えたか？
  → 約 10〜13 問多く解いた（347 vs 334）。

• どの領域で強かったか？
  → 中〜難問帯で Winner が止まった後も SATLUTION は解き続けた。

---

必要なら、

• SAT/UNSAT 別の比較
• PAR-2 スコアの詳細
• 2024 ベンチマークでの比較
  なども整理できます。

Q.過去ソルバの良いところ取りだけではないの？

結論から言うと 「半分正しいが、それだけでは不十分」 という答えになります。
SATLUTION（論文中の表記は SATLUTION）は、確かに 過去ソルバの良いところ取り（hybridization）を行っている のですが、実際にはそれを はるかに超える進化的プロセス を実行しています。

以下、論文内容に基づいて整理します（ arxiv.org）。

---

🧩 SATLUTION がやっていることは「良いとこ取り＋自律的進化」

① 良いところ取り（hybridization）は確かに行っている

論文では、初期状態として SAT Competition 2024 の 5 つの強力なソルバを seed として与えています。

• kissat-sc2024
• kissat-mab-dc
• kissat-mab-binary
• BreakID-Kissat
• AMSAT

SATLUTION はこれらのコードベースを読み込み、
互いの強みを組み合わせる方向に進化する と明記されています。

“SATLUTION made rapid progress in the first 5–10 iterations, quickly lowering PAR-2 by combining complementary strengths from the different seed solvers.”
（ arxiv.org）

つまり、初期段階ではまさに「良いところ取り」をして性能を底上げしています。

---

② しかし本質は「自律的な新規アルゴリズム発見」

SATLUTION の特徴は、単なるマージではなく 新しいヒューリスティックやアルゴリズムを自動生成する点 にあります。

論文では、進化の過程で以下のような 新規の最適化手法 を自律的に発見したと書かれています：

• Multi-UIP clause learning の新しいバリエーション
• Bandit（多腕バンディット）による UIP depth の動的調整
• Vivification の SAT/UNSAT 感度分析と動的制御
• Adam-like updates を使った reward tuning
• Multi-domain bandit による複数ヒューリスティックの協調制御
• BreakID の統合による対称性検出
• Compressed watch list architecture の導入

これらは単なる「良いところ取り」ではなく、
既存ソルバにも存在しない新規アイデア です。

---

③ さらに、ルールベースと自己進化ルールにより「設計思想」まで進化

SATLUTION はコードだけでなく、
自分自身の進化ルール（rulebase）も自動で更新する という仕組みを持っています。

• forbidden patterns（禁止パターン）の自動追加
• correctness rules の強化
• logging / documentation rules の自動更新
• failure patterns を学習して次の iteration に反映

これは人間の開発プロセスに近い「メタ進化」であり、
単なるソルバの合体では到達できない領域です。

---

🔍 まとめ：良いところ取りは「入口」であり、本質はもっと深い

観点	SATLUTION の実際
過去ソルバの良いところ取り？	YES（初期段階で大きく寄与）
それだけ？	NO（中盤以降は新規アルゴリズムを自律生成）
進化の本質	ルールベース＋フィードバックによる 自律的コード進化
最終的な成果	2025 Winner を超える性能（347 solved vs 334 solved）

---

🎯 結論

「良いところ取り」は SATLUTION の進化の一部にすぎず、
本質は “自律的に新しい SAT ソルバを設計する AI エージェント” です。

---

もし興味があれば、

• どの seed solver のどの要素が取り込まれたのか
• 新規に生まれたヒューリスティックの詳細
• 進化の各 iteration の変化（Figure 8）
  なども深掘りできます。

CadicalにCHBを実装

 CHBの実装をコパイに依頼したら、次のコードを提示されました。

int Internal::pick_chb_branch_lit () {
  double best = -1.0;
  int best_idx = 0;

  // 変数集合のイテレーション：CaDiCaL の実装に合わせて調整
  for (int idx = 2; idx <= max_var; idx++) { // idx: internal literal index (±)
    if (!active (idx)) continue;
    if (val (idx)) continue;          // すでに割り当て済み

    const double s = chb_score (idx);
    if (s > best) {
      best = s;
      best_idx = idx;
    }
  }
}

これは、却下です。変数の全スコアをスキャンして、その最高値を持ってくる実装ですが、遅すぎて話になりません。折角、スコア用のヒープを備えているのですから、それを利用しない手はありません。

struct score_smaller {
  Internal * internal;
  score_smaller (Internal * i) : internal (i) { }
  bool operator () (unsigned a, unsigned b);
};
struct ScoreComparator {//FEB042026
    Internal* internal;
    ScoreComparator(Internal* i) : internal(i) {}
    // ここが比較の核心：internal->score (a) の値を直接見ている
    bool operator () (unsigned a, unsigned b)const;

};
typedef heap ScoreSchedule;
typedef heap ScoreHeap;//FEB042026

#ifdef USE_CHB
inline bool ScoreComparator::operator() (unsigned a, unsigned b) const {
    assert(1 <= a);
    assert(a <= (unsigned)internal->max_var);
    assert(1 <= b);
    assert(b <= (unsigned)internal->max_var);
    return internal->chb_score(a) < internal->chb_score(b);
}

#endif
#ifdef USE_CHB
  double& chb_score(int lit) { return chb[vidx(lit)]; }
#endif
void Internal::bump_variable_score (int lit) {
  assert (opts.bump);
  int idx = vidx (lit);

#ifdef USE_CHB
  
  const int64_t conflicts = stats.conflicts;

  // CHBの報酬計算: 1 / (現在のコンフリクト番号 - 最後にこの変数が関与した番号 + 1)
  double reward = 1.0 / (double)(conflicts - last_conf[idx] + 1);
  //CHBは「直近のコンフリクト」を重視するため、探索が進むにつれて学習率を下げていかないと、スコアが激しく変動しすぎて探索が安定しません。 Liangらの論文で推奨されている標準的な設定は以下の通り： 初期値(\(\alpha _{ start }\)) : 0.4下限値(\(\alpha _{ min }\)) : 0.06減衰量(\(\alpha _{ step }\)) : 1e-6（衝突1回につき）
  if (chb_alpha > 0.06) {
      chb_alpha -= 0.000001;
  }
  // ERWA (Exponential Recency Weighted Average) 更新
  // Q = (1 - alpha) * Q + alpha * reward
  // α の減衰
  
  chb[idx] = (1.0 - chb_alpha) * chb[idx] + chb_alpha * reward;
  last_conf[idx] = conflicts;

  // ヒープの更新（ScoreComparatorがchbを参照するようになっているため、これで並び替わる）
  if (chb_scores.contains(idx)) chb_scores.update(idx);


#endif

Liangさんの論文に示された通りの実装にしています。上の更新式は、一次IIRフィルタに似ています。

当時、確か、機械学習の発想を取り入れた、との話があったかに記憶しています。

https://ojs.aaai.org/index.php/AAAI/article/view/10439

なお、CHBは、VSIDSよりもリスタート間隔を短くした方がよい、という説もありますが、真偽は分かりません。

Combining VSIDS and CHB Using Restarts in SAT

Cadical/Kissa共、CHBを実装していないのですが、最近のSAT competitioin優勝ソルバは、いずれもMAB方式です。

A new variable ordering for in-processing bounded variable elimination in SAT solvers | Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence

Cadical バグを修正

 多分バグだと思いますが、GCCでは警告がないのかもしれません。

radix sort部分でクラッシュしました。コパイにお願いすると、VisualStudioのエラーと一致する指摘となりました。完全に書き換えるコードの提案をされて、安直に置き換えてみるとエラーは消失しました。凄い。C++ソースも完全に理解しているのですね。

c == b の比較で vector がエラーになる理由は、このコードが イテレータ同士の比較をしているように見えて、実際には “別コンテナのイテレータを比較している” 可能性が非常に高いからです。

---

🔍 問題の本質：c と b は「同じコンテナのイテレータ」ではない

コードの該当部分を抜き出すと：

I a = first, b = last, c = a;
...
std::vector<T> v;
...
if (!initialized) {
    v.resize(n);
    b = v.begin();
    initialized = true;
}
...
I d = (&*c == &*a) ? b : a;
...
c = d;
...
if (c == b) {
    for (size_t i = 0; i < n; i++)
        a[i] = b[i];
}

ここでのポイントは：

✔ a と c は 元の配列（FIRST〜LAST） のイテレータ

✔ b は vector v の begin()

❌ つまり c == b は 異なるコンテナのイテレータ比較

C++ の規格では：

異なるコンテナのイテレータを比較することは未定義動作（UB）

未定義動作なので、クラッシュしたり、比較が常に false になったり、ランダムな挙動をします。

---

🧨 なぜこのコードは UB を踏んでしまうのか？

c は毎ループで a または b に切り替わる。

• c = a のとき → 元の配列のイテレータ
• c = b のとき → vector のイテレータ

最後に

if (c == b)

を行うが、c が元配列のイテレータのままなら 異なるコンテナのイテレータ比較 になる。

---

🛠 解決策：イテレータ比較ではなく「どちら側か」を示すフラグを使う

最も安全で一般的な修正は：

✔ c が vector 側を指しているかどうかを bool で管理する

例：

bool using_vector = false;
...
if (!initialized) {
    v.resize(n);
    b = v.begin();
    initialized = true;
}
...
I d;
if (&*c == &*a) {
    d = b;
    using_vector = true;
} else {
    d = a;
    using_vector = false;
}
c = d;
...
if (using_vector) {
    for (size_t i = 0; i < n; i++)
        a[i] = b[i];
}

これなら 異なるコンテナのイテレータ比較を避けられる。

---

🎯 まとめ

問題点	理由
c == b がクラッシュ	異なるコンテナのイテレータ比較は未定義動作
なぜ起きる？	c は元配列 or vector のどちらかを指す可能性がある
解決策	イテレータ比較ではなく、どちら側を使っているかを bool で管理

---

必要なら、この radix sort 全体を 安全に書き直したバージョン も作れます。
あるいは、あなたのプロジェクトに合わせて 最適化版 を作ることもできますよ。

了解、孝幸さん。
あなたのコードは CaDiCaL の radix sort 実装をベースにしていますが、イテレータが別コンテナを指す可能性があるのに比較してしまうという UB（未定義動作）が潜んでいました。

そこで、イテレータ比較を完全に排除し、状態フラグで安全に制御するバージョンを用意しました。
元のアルゴリズム構造は維持しつつ、C++ として安全に動くように書き直しています。

---

✅ 安全に書き直した rsort（イテレータ比較なし・UBなし）

template <class I, class Rank>
void rsort(I first, I last, Rank rank) {
    using T = typename std::iterator_traits<I>::value_type;
    using R = typename Rank::Type;

    assert(first <= last);
    const size_t n = last - first;
    if (n <= 1) return;

    const size_t l = 8;
    const size_t w = (1 << l);
    const unsigned mask = w - 1;

    size_t count[w];

    I a = first;
    I c = a;

    std::vector<T> v;
    I b;                 // vector 側の begin()
    bool using_vector = false;  // ★ どちら側を使っているかを管理

    R upper = 0, lower = ~upper;
    R shifted = mask;
    bool bounded = false;

    R masked_lower = 0, masked_upper = mask;

    for (size_t i = 0; i < 8 * sizeof(rank(*first)); i += l, shifted <<= l) {

        if (bounded && (lower & shifted) == (upper & shifted))
            continue;

        memset(count + masked_lower, 0,
               (masked_upper - masked_lower + 1) * sizeof *count);

        const I end = c + n;
        bool sorted = true;
        R last_bucket = 0;

        for (I p = c; p != end; p++) {
            const auto r = rank(*p);
            if (!bounded) {
                lower &= r;
                upper |= r;
            }
            const auto m = (r >> i) & mask;
            if (sorted && last_bucket > m)
                sorted = false;
            last_bucket = m;
            count[m]++;
        }

        masked_lower = (lower >> i) & mask;
        masked_upper = (upper >> i) & mask;

        if (!bounded) {
            bounded = true;
            if ((lower & shifted) == (upper & shifted))
                continue;
        }

        if (sorted)
            continue;

        size_t pos = 0;
        for (R j = masked_lower; j <= masked_upper; j++) {
            const size_t delta = count[j];
            count[j] = pos;
            pos += delta;
        }

        if (!using_vector) {
            v.resize(n);
            b = v.begin();
        }

        I d = using_vector ? a : b;  // ★ ここで切り替え
        bool next_using_vector = !using_vector;

        for (I p = c; p != end; p++) {
            const auto m = (rank(*p) >> i) & mask;
            d[count[m]++] = *p;
        }

        c = d;
        using_vector = next_using_vector;
    }

    if (using_vector) {
        for (size_t i = 0; i < n; i++)
            a[i] = b[i];
    }

#ifndef NDEBUG
    for (I p = first; p + 1 != last; p++)
        assert(rank(p[0]) <= rank(p[1]));
#endif
}

---

🔒 このバージョンが安全な理由

問題点	修正内容
異なるコンテナのイテレータ比較 (c == b)	bool using_vector で状態管理
&*c == &*a のような危険なアドレス比較	完全に排除
イテレータがどちらの配列を指すか不明瞭	using_vector と next_using_vector で明確化
UB（未定義動作）	ゼロ

---

🎁 さらに改善したい場合

• std::array<size_t, w> を使って stack allocation を明示化
• std::span を使って safer pointer arithmetic
• std::bit_width を使って動的にパス数を決定
• std::pmr::vector でアロケーション最適化

必要なら、これらも組み込んだ モダン C++20/23 版の高速 radix sort も作れます。

---

もっと最適化したい、あるいは CaDiCaL の他の部分も安全化したい場合は続けてどうぞ。

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 制御テンプレート

なども作れますよ。

何故Cadicalは、遅いか？

データを取ってみると数倍以上遅いです。 

恐らくは、VSIDSにあります。現在のスケジュールナースのソルバは、CHBをベースに据えていて、この特性差によるものと、考えます。CHBは、最近のConflictに対してよく効いてSAT解が速く求まる傾向にあります。それに対してVSIDSは、じっくり考えるタイプで、後からじわじわ効いてくる感じでしょうか？　恐らくは、SAT Competitionの時間が1時間以上なので、それで最適化すると、VSIDS選択になるのでしょう。が、スケジュールナース系の1－2分内で答えを出すような用途では、CHBの方が良いと思っています。MaxSAT系のCompetitionで求解の速さを競うトラックがあるのですが、ここに何故かCadical系が登場しないのは、こういった理由があるのかもしれません。

Cadicalの実装をCHBにする手間について、コパイに聞きました。Armin Biere さんが、CHBを何故採用しなかったか？について、かって言及した文献は見たことがありません。CHBが台頭してきた時期、Armin Biere さんは、意図的に無視しているように感じる部分はありました。

それに対して、コパイは、設計者が語ったことのない設計思想まで踏み込んで断じています。LLMがC++ソースの中身まで理解していないとここまで断じることはないと思いますが、それにしても、凄い技術力です。最近、中国系の研究者は、SATソルバをLLMを使って最適化しようという研究を盛んに行っており、そこでの学習成果かもしれません。

＊＊＊

結論から言うと CaDiCaL は CHB（Conflict History Based branching）をサポートしていません。
内部の決定ヒューリスティックは VSIDS（正確には EVSIDS）固定で、CHB に切り替える API もオプションも存在しません。

あなたの質問の意図はよく分かるので、背景と理由を整理しておきます。

---

🎯 結論

ヒューリスティック	CaDiCaL で使える？	備考
VSIDS / EVSIDS	✔（標準）	CaDiCaL の中心
CHB	✖（非対応）	実装なし
LRB（Learning Rate Branching）	✖	実装なし
Hybrid（VSIDS+CHB）	✖	実装なし

CaDiCaL は VSIDS + Target Phase + Restart 戦略 に最適化されており、
CHB のような Glucose 系の branching heuristic は採用していません。

---

🔍 なぜ CaDiCaL は CHB を採用していないのか

CaDiCaL の設計思想は：

• シンプルな EVSIDS を徹底的に最適化する
• inprocessing（vivification, subsumption, rebuild）で性能を稼ぐ
• ヒューリスティックの切り替えは行わない

CHB は Glucose 4.0 以降で導入された手法で、
「変数の最近の学習節への貢献度」を使うヒューリスティックですが、
CaDiCaL の内部構造とは相性が良くありません。

---

🧠 どうしても CHB を使いたい場合の選択肢

1. ソルバを CHB 実装のあるものに切り替える

CHB を実装している代表的ソルバ：

• Glucose 4.1
• MapleSAT
• MapleLCMDistChronoBT
• Kissat（CHB ではないが LRB 系の実験実装あり）

特に MapleSAT 系は CHB の実装が成熟しています。

---

2. CaDiCaL に CHB を自前で追加する（非推奨）

技術的には可能ですが、以下の理由で非常に難しいです：

• CaDiCaL の branching は solver.cpp に深く埋め込まれている
• VSIDS 活動値の decay と bump が多数の箇所に散在
• CHB のためには per-variable の “recent conflict contribution” を追跡する必要がある
• CaDiCaL の inprocessing が VSIDS を前提に設計されている

実質的にソルバの大改造になります。

---

🧩 あなたの用途に合わせた提案

あなたのアーキテクチャ（C++ → C# → Pythonnet → asyncio）を考えると：

• CaDiCaL は VSIDS 固定で使う
• CHB を試したいなら MapleSAT / Glucose を別プロセスで呼ぶ
• 複数ソルバを統合する SolverManager を C++ で作る

という構成が最も現実的です。

必要なら、

• MapleSAT / Glucose を C++ から安全に呼ぶラッパ
• CaDiCaL と CHB ソルバのハイブリッド探索
• CHB の効果を比較する実験設計
• あなたの WinForms + Pythonnet 環境に統合する設計図

なども作れますよ

Cadicalのcopy

 cadical.hppの説明だけでは、判然としない部分があり、コパイに聞いてみました。deep cloneではない、とヘッダには書いてありましたが、コパイの説明だと、deep copyということです。


ところで、LLMは、マニュアルの説明だけではなく、「Armin Biere さんが言っているように...」と、別な情報源も含めて回答を作成しています。このような状態を意図的に作り出すことが、スケジュールナースMCPソルバの目的です。ただしネットの情報は、間違っていることも多いので、公式なLLM用のDocumentとして、ULIで指定するところがミソです。多くのCommunityから参照される情報は、何もしなくとも、LLMが勝手に学習しますが、ニッチな分野でのアプリに過ぎないスケジュールナースにとって、LLMが参照する情報は正確かつ有用な情報に限定してやる必要があります。

それは、ともかく、deep copyとして使えることは、大きな利得です。Cadicalは、assumption廻りがとても遅くて、もしかして使えないかな？と思い始めていたのですが、これは、その欠点を補って余りある大きなメリットです。ソルバ構造の大変更になってしまいますが、検討する価値はあります。

＊＊＊＊

結論から言うと **CaDiCaL の copy() API は「学習節も含めて、ほぼ完全な内部状態を複製する」ので、実質的に ほぼ完全な Duplicate と考えて問題ありません。
ただし、いくつかの重要なニュアンスがあります。

---

✅ 結論：copy() は学習節もコピーする（＝実質 Duplicate）

CaDiCaL の Solver::copy() は、内部の状態を deep copy します。

含まれるもの：

• 元の CNF（元節）
• 学習節（learnt clauses）
• 変数の状態
• ヒープ・活動値（VSIDS scores）
• trail / assignment
• watcher 構造
• inprocessing の進行状況
• restart / rephase の内部カウンタ

つまり、solve() の途中で copy() を呼ぶと、その時点のソルバ状態を丸ごと複製した新しい Solver が得られます。

---

⚠️ ただし、完全な Duplicate ではない部分もある

CaDiCaL の作者 Armin Biere が明言しているように、
copy() は 「完全に bit-identical な複製」ではありません。

理由：

• メモリ配置は異なる
• 一部の統計カウンタはリセットされる
• ランダムシードはコピーされるが、後の探索は divergence する可能性が高い
• 外部割り込み状態（terminate フラグ）はコピーされない

しかし、探索状態（学習節・活動値・trail）はコピーされるため、実質的には Duplicate として使える。

---

🧠 実際の用途：copy() は「分岐探索の分岐点保存」に使える

あなたのように solver を複数方向に分岐させたい場合：

Solver* base = ...;  // solve() の途中
Solver* branchA = base->copy();
Solver* branchB = base->copy();

branchA と branchB は 同じ学習節を共有していない独立インスタンス になるので、
それぞれ別の探索を進められます。

---

🔍 copy() がコピーしないもの

• 外部の callback（if any）
• 外部の file handle / logging 状態
• terminate フラグ
• 一部の統計（stats）

これらは安全性のためコピーされません。

---

🎯 まとめ

項目	copy() でコピーされる？	備考
元節（CNF）	✔	完全コピー
学習節	✔	deep copy
VSIDS 活動値	✔	ほぼ完全コピー
trail / assignment	✔	solve 中でもコピー可能
restart 状態	✔	ほぼコピー
terminate フラグ	✖	コピーされない
統計カウンタ	△	一部リセット
メモリ配置	✖	異なる

→ 実質的には Duplicate として使える。
学習節も含めて探索状態を丸ごと複製する。

---

必要なら：

• copy() を使った「並列分岐探索」テンプレート
• copy() を使った「バックトラック高速化」
• copy() と limit(conflicts) を組み合わせたハイブリッド探索

なども作れますよ。