データを取ってみると数倍以上遅いです。
恐らくは、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 環境に統合する設計図
なども作れますよ
