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) を組み合わせたハイブリッド探索

なども作れますよ。

Feasiblity Study by sudoku

 アイデアの有効性を数独で検証しました。数独問題を解くのではなくて、数独の構造を有する割り当てを求める問題です。

この解は、数学的には、どのサイズでも必ず存在することが分かっています。 ラテン方格（Latin squares）とグレコラテン方格（Graeco‑Latin squares） の理論によって解を持つことは保証されています。一般化数独（n×n ブロックを持つ巨大数独）の 完成形（解） が、任意の n に対して存在することは、Herzberg & Murty (2007), Berend (2018) などの構成法で証明済みです。

なので、特殊解は、数学的方法で求めることが出来る筈です。それに対して、特殊解以外を含めて解の探索を行う一般的なアルゴリズムで、求めることは、結構難しく、MIPソルバで、5x5位まで(実測したことはありません。⇒9年前のRAMP講演でありました。）SATソルバで、10x10位ではないでしょうか？

今回の方法では、以下のような結果となりました。

Kissatの最新版を用いても、やはり10x10までしか求めることが出来ませんが、今回の方法では、12x12まで求めることが出来ました。このとき、変数数は、(12*12)^3=2985974です。もしかすると、SATソルバによる方法の世界記録かもしれません。これを、ナーススケジューリング問題にあてはめると、

■シフト数144　スタッフ1人/1日あたりのシフト数は1

■Day数144日　スタッフ144人の各シフト値の総和が1　144x144個の行制約がある

■Cover制約　各日に対して各シフト144について総和が1　144x144個の列制約がある

という問題の解が求まった。ということになります。上記評価結果を、ナーススケジューリング問題に言い換えると、今までは、シフト数100程度が限界だったのが、シフト数144まで求められるようになった、ということになります。自分で言うのもなんですが凄まじいです。

ちなみに、

■instance24の規模は、スタッフ数150人、Day数365日で、この点では、上の規模を上回っています。

■ローカルソルバで、どうなるかはやっていませんが、期待は持てないと思っています。

確か、昔は、6程度のサイズでも数秒かかっていたと思うので、(上表では、0.1秒もかかっていない）、ソルバとPCの両輪、ソフトウェアとハードウェアの掛け算で、性能向上を成し遂げてきたと思います。隔世の感がします。

instance24攻略に向けて、期待が持てる結果となりました。

Caidicalのポート

メモリ削減アイデアの検証用ソルバとして、Cadicalをポートします。

Cadicalは、KissatのC++バージョンです。Kissatは、未だにincrementalではないし、Maxsatでは必須のassumptionもサポートしていません。その点Cadicalは、Kissatに比べればメモリは、3倍位食いますが、最先端のソルバでありながら、全てのMaxSAT必要条件を満たします。大規模用の整数化ソルバとしてメタヒューリスティクスを検討していましたが、SATソルバでも上手く行けば、大規模でも性能を発揮できる可能性がある、と考えました。

コテコテのLinuxソースなのでWindowsポートは大変です。

#ifdef _WIN32

#define cadical_putc_unlocked _putc_nolock

#define cadical_getc_unlocked _getc_nolock

#else

#define cadical_putc_unlocked putc_unlocked

#define cadical_getc_unlocked getc_unlocked

#endif

#define NBUILD;__WIN32;NOGDI;

__builtin_clz  ⇒pal-winの中のunistdh　にマクロ

#ifdef _WIN32

    Strict=2

#else

    STRICT = 2,

#endif