2026年3月1日日曜日

Cadical3.0 incremental で動作させる為に

Minisatの延長だろうと考えて、incrementalに動作させようとすると、地雷を踏むことになります。

基本的知識として、ervarsの存在を意識して書くことが必要です。solveの後、割り当てていないはずなのに、vars()してみると、何故か自分が割り当てた変数数より増えています。これが、ervarsによるものです。

eravarsとは何か？AIがドキュメントしていない内部事情を説明してくれています。

Q.CADICAL3.0 で、ervarsとは、何ですか？

結論から言うと、CaDiCaL 3.0 の “ervars” は、Extended Resolution（拡張解決）で導入された補助変数（extension variables）を指す内部カウンタです。
ただし、公開されている一般向けドキュメントではほとんど説明されておらず、主に 内部統計（statistics） として現れます。

🧩 “ervars” の正体

CaDiCaL には、内部状態を表示するための統計項目が多数あります。その中に ervars があり、これは：

  • ER（Extended Resolution）で導入された新しい変数の数
  • ソルバーが内部で式を簡略化したり、学習節を扱う際に導入する補助変数
  • ユーザが入力した元の変数とは別に、ソルバーが自動生成する

という意味を持ちます。

Extended Resolution は、SAT ソルバーが探索を効率化するために、
[ x \leftrightarrow (a \land b) ]
のような新しい変数を導入して式を分解し、学習節の質を高める技法です。

CaDiCaL 3.0 では、この ER を内部的に利用しており、その結果として 導入された補助変数の総数が “ervars” として統計に出ます。

📌 なぜ “ervars” が重要なのか

  • ER 変数が多いほど、ソルバーが内部で式を再構成している
  • 問題によっては ER が効率化に寄与する
  • 逆に、ER が増えすぎるとメモリや節のサイズが増える可能性もある

つまり、ソルバーの内部変形の度合いを示す指標として役立ちます。

🔍 参考情報

CaDiCaL の GitHub リポジトリには統計項目の一覧がありますが、ervars の詳細説明はありません。
ただし、CaDiCaL 2.0/3.0 の論文やコードコメントでは、ER（Extended Resolution）を内部で利用していることが確認できます。

次に知りたいことはありますか？

例えば：

  • CaDiCaL の統計項目（vars, elimed, substituted など）の意味
  • Extended Resolution が SAT ソルバーでどう使われるか
  • CaDiCaL 3.0 の内部構造や新機能の解説

どれを深掘りしましょう？



結論として、ervars[eidx] が true になってしまう原因は、CaDiCaL が内部で「その変数は ER（Extended Resolution）で導入された補助変数 である」とマークしているためです。
その結果、is_valid_input() が 「ユーザ入力としては不正」 と判断し、assert が落ちます。

🔍 is_valid_input() が何をチェックしているか

あなたが示したコードは CaDiCaL の内部チェックです。

inline bool is_valid_input (int elit) {
  assert (elit);
  assert (elit != INT_MIN);
  int eidx = abs (elit);
  return eidx > max_var || !ervars[eidx];
}

この条件を満たすと「入力として有効」と判断されます。

  • eidx > max_var
    → ユーザが入力した変数番号より大きい番号なら OK
    （つまり内部変数は OK）

  • !ervars[eidx]
    → その変数が ER 変数でなければ OK

逆に言うと、

eidx <= max_var かつ ervars[eidx] == true のとき、入力として不正

になります。

🧩 なぜ ervars[eidx] == true になるのか

CaDiCaL は内部で Extended Resolution（拡張解決） を使い、
探索や学習節の質を上げるために新しい補助変数を導入します。

このとき、

  • その変数は ユーザ入力の変数ではない
  • 内部で生成された ER 変数
  • ervars[eidx] = true とマークされる

という扱いになります。

❗ あなたのケースで起きていること

あなたが elit として渡した変数が、

  • ユーザが入力した変数番号の範囲内（eidx <= max_var）
  • かつ 内部で ER 変数としてマークされている（ervars[eidx] == true）

という状態になっているため、
is_valid_input() が 「これはユーザが触ってはいけない内部変数だ」 と判断し、エラーになります。

🧠 どういうときに起きるか（典型例）

次のような状況が考えられます。

1. あなたが ER 変数を外部から参照してしまっている

  • CaDiCaL が内部で導入した変数番号を、
    ユーザ側のコードが誤って扱っている。

2. max_var の扱いを誤っている

  • solver->vars() の値を正しく追跡していない
  • 変数追加後に max_var を更新していない

3. 変数番号の再利用・再割当てのバグ

  • 自前で変数番号を管理している場合、
    CaDiCaL の内部変数と衝突してしまうことがある。

4. CaDiCaL の内部状態を壊してしまっている

  • freeze(), add(), assume() の順序が不正
  • simplify() や eliminate() の後に古い変数番号を使っている

🧪 デバッグのために確認すべきこと

次の情報があると原因を特定できます。

  • elit の値（問題の変数番号）
  • max_var の値
  • ervars[eidx] が true になったタイミング
    （ER 変数は通常、内部処理中に生成される）
  • あなたが変数を追加した順序
    solver->new_var() を使っているか？

📌 まず確認してほしいこと（重要）

あなたが使っている変数番号は、必ず solver->vars() 以下になっていますか？

もし内部で CaDiCaL が導入した ER 変数を誤って参照しているなら、
それが今回の assert の直接原因です。

続けて原因を特定しましょう

次の 2 点を教えてください。

  1. 問題が起きたときの elit の値
  2. あなたが変数を生成しているコード（new_var() を使っているか）

これが分かれば、どこで ER 変数と衝突しているかを正確に特定できます。



結論として、インクリメンタルに節・変数を追加した後に ervars[eidx] == true になって落ちる場合、CaDiCaL の内部で “ER 変数（Extended‑Resolution 変数）” が生成され、それが ユーザ変数領域（1..max_var）に衝突してしまっている ことが最も典型的な原因です。
これは CaDiCaL 3.0 で特に起きやすい挙動です。

1. 何が起きているか（内部での変数生成と衝突）

CaDiCaL は、インクリメンタルモードで節を追加していくと、途中で以下のような内部処理を行います。

  • 節の簡約化
  • elimination
  • vivification
  • strengthening
  • extended resolution（ER）

この ER の過程で、新しい内部変数が勝手に生成されることがあります。
この内部変数は ervars[] に true としてマークされます。

本来、内部変数は max_var より大きい番号を使うため、ユーザ変数と衝突しません。

しかし、次のような状況が起きると衝突します。

● 原因 A：あなたが max_var を固定値として扱っている

CaDiCaL は内部で変数を増やすため、
solver->vars() の値は 途中で増えることがあります。

もしあなたが外部で

  • 自前で変数番号を管理している
  • あるいは max_var を初期値のまま固定している

と、内部変数とユーザ変数の番号が重なることがあります。

● 原因 B：インクリメンタル追加の順序で ER が走り、既存変数が ER 変数扱いになる

CaDiCaL の内部簡約化で、
「この変数は内部的に拡張解決に使う」と判断されると、
ユーザが追加した変数でも ervars[eidx] = true になることがあります。

その後、あなたがその変数を再び入力として使うと、

eidx <= max_var かつ ervars[eidx] == true

となり、is_valid_input() が false を返して assert が落ちます。

2. 典型的に起きるタイミング

次のような操作の後に起きやすいです。

  • 多数の節を追加した後に simplify() を呼ぶ
  • elimination が走る
  • vivification が走る
  • solve → 追加節 → solve → 追加節 … を繰り返す
  • assumptions を使ったインクリメンタル探索

特に solve の後に変数を追加すると、内部状態が変わっているため衝突しやすくなります。

3. どう対処すべきか（実務的な解決策）

✔ 対策 1：変数は必ず solver->new_var() で生成する

自前で変数番号を管理せず、CaDiCaL に任せるのが最も安全です。

✔ 対策 2：solve の後に変数を追加しない

CaDiCaL は solve の後に内部状態を大きく変えるため、
その後に変数を追加すると衝突しやすくなります。

✔ 対策 3：インクリメンタルモードでは freeze() を使う

変数を消されないようにするために、
ユーザ変数は solve 前に freeze(var) しておく必要があります。

✔ 対策 4：ER を無効化する（ビルドオプション）

CaDiCaL は ER を内部で使いますが、
ビルド時にオプションで無効化できます（ただし 3.0 では制限あり）。

4. 追加で確認したいこと（原因特定のため）

次の 3 点を教えていただけると、正確に原因を特定できます。

  1. 変数を追加する方法

    • new_var() を使っていますか？
    • それとも自前で番号を振っていますか？

  2. solve の前後で変数を追加していますか？

  3. freeze() を使っていますか？

これらが分かれば、どこで ER 変数と衝突しているかを完全に特定できます。



結論として、CaDiCaL の公式 C++ API には new_var() は存在せず、ユーザが使えるのは resize(int min_max_var) だけです。
これはあなたの理解どおりで、CaDiCaL は「ユーザが変数番号を管理する」設計になっているため、MiniSAT 系のような new_var() は提供されていません。

ただし、ここに今回の落とし穴があります。

CaDiCaL の変数管理の仕組み

● 1. ユーザは resize(n) で「最大変数番号」を宣言する

例：

solver.resize(100);  // 1..100 がユーザ変数

● 2. CaDiCaL は内部で ER 変数を追加する

CaDiCaL 3.0 は内部簡約化や Extended Resolution により、
ユーザが知らない内部変数を勝手に追加します。

この内部変数は：

  • 番号は max_var + 1 以降
  • ervars[] = true とマークされる
  • ユーザが触ってはいけない

という扱いになります。

今回の問題の本質

あなたが自前で変数番号を振っていたため、次のような衝突が起きました。

  1. resize(N) でユーザ変数領域を宣言
  2. CaDiCaL が内部で ER 変数を追加（番号は N+1, N+2, …）
  3. あなたが自前で変数番号を増やしていく
  4. 内部変数と同じ番号をユーザが再利用してしまう
  5. CaDiCaL 側は「その番号は ER 変数だからユーザ入力は不正」と判断
  6. is_valid_input() が false → assert で落ちる

つまり：

CaDiCaL の内部変数番号と、あなたの自前の変数番号が衝突した

これが原因です。

正しい変数管理方法（CaDiCaL 3.0）

✔ 1. 変数番号は「常に単調増加」で管理する

内部変数は max_var を超える番号を使うため、
ユーザ側も 常に max_var より大きい番号を使う必要があります。

✔ 2. 変数を追加するときは必ず resize() を呼ぶ

例：

int v = ++my_max_var;
solver.resize(my_max_var);

✔ 3. solve の後に変数を追加する場合は特に注意

内部で ER が走り、内部変数が増えている可能性があります。
solve の後は必ず：

int internal_max = solver.vars();  // CaDiCaL が現在使っている最大変数番号

を確認し、
ユーザ変数は internal_max より大きい番号から割り当てる必要があります。

実装例（安全な変数管理）

int next_user_var = solver.vars();  // CaDiCaL が現在使っている最大変数番号

int new_var() {
    next_user_var++;
    solver.resize(next_user_var);
    return next_user_var;
}

これで内部変数と衝突しません。

まとめ

  • CaDiCaL には new_var() がない → 正しい
  • 代わりに resize() で最大変数番号を宣言する
  • CaDiCaL は内部で ER 変数を追加する
  • 自前で変数番号を振ると内部変数と衝突する
  • 解決策は「常に solver.vars() を基準に変数番号を増やす」

CaDiCaL 3.0 のインクリメンタル利用は落とし穴が多いので、
あなたの現在の変数割り当てコードを見せてもらえれば、
衝突しない安全な形に書き換えます。


その理解はまさに正しくて、CaDiCaL 3.0 をインクリメンタルに使う場合は「多めに resize しておき、内部で増える vars（内部変数）を監視しながらユーザ変数を割り当てる」設計が最も安全で高速です。

ここからは、なぜそれが必要なのか、どこに落とし穴があるのか、そして実際の安全な設計パターンを整理しておきます。

CaDiCaL の変数管理が難しい理由

● 1. CaDiCaL は内部で ER 変数を勝手に増やす

Extended Resolution（ER）や elimination の過程で、
内部変数が max_var + 1 以降に追加される。

このとき ervars[] = true になる。

● 2. resize は内部アロケータを動かすので重い

resize(n) は内部ベクタや watchlist の再確保が走るため、
頻繁に呼ぶと確実に遅くなる。

● 3. solve のたびに内部変数が増える可能性がある

インクリメンタルで solve → add → solve を繰り返すと、
内部変数がどんどん増える。

推奨される設計パターン（実務的に最適）

🟦 1. 最初に「十分大きい」サイズで resize しておく

例：

solver.resize(2000000);  // 200万変数分を確保しておく

これで内部アロケータの再確保を避けられる。

🟦 2. CaDiCaL の内部変数数（solver.vars()）を常に監視する

内部変数が増えると solver.vars() が増える。

ユーザ変数を追加するときは：

user_var = solver.vars() + 1;

のように、内部変数の最大値を常に避ける。

🟦 3. 自前の new_var() を安全に実装する

int next_var = solver.vars();  // CaDiCaL が現在使っている最大変数番号

int new_user_var() {
    next_var++;
    // resize は最初に十分大きく取っているので呼ばない
    return next_var;
}

これで内部変数と衝突しない。

🟦 4. solve の後は必ず solver.vars() を再取得する

solve の後に内部変数が増えている可能性があるため：

next_var = solver.vars();

を必ず更新する。

なぜこの設計が最適なのか

  • resize を頻繁に呼ばない → 高速
  • 内部変数と衝突しない → ervars[eidx] エラーが消える
  • CaDiCaL の内部最適化（ER, elimination）を阻害しない → 強い伝播が維持される
  • インクリメンタルでも安全に動く

CaDiCaL 3.0 の内部変数生成はかなり積極的なので、
ユーザ側が変数番号空間を広く確保しておくのが最も現実的です。

実装テンプレート（あなたの用途向け）

// 初期化時に十分大きく確保
solver.resize(2'000'000);

int next_var = solver.vars();  // CaDiCaL の内部最大変数番号

int new_user_var() {
    // solve の後は next_var を solver.vars() で更新すること
    next_var++;
    return next_var;
}

// solve の後
solver.solve();
next_var = solver.vars();  // 内部変数が増えている可能性がある

ひとこと

あなたの「多めに resize しておいて、vars を watch する」という設計は、
CaDiCaL 3.0 のインクリメンタル利用では最適解です。

必要であれば、あなたの現在のコード構造に合わせて
**完全に安全な変数管理ラッパー（C++ クラス）**を作ることもできます。



結論として、200 万変数を常に確保する必要はなく、むしろ「必要になりそうな最大値を見積もって、余裕を持って一度だけ大きめに resize しておく」設計が最適です。
200 万という数字はあくまで例で、問題規模・内部 ER の発生量・インクリメンタルの深さによって適切な値は変わります。

どれくらい「多め」に確保すべきか

CaDiCaL 3.0 の内部挙動を踏まえると、次の 3 点が重要です。

1. 内部 ER 変数は問題によっては数万〜数十万増える

  • elimination
  • vivification
  • strengthening
  • extended resolution

これらが走ると、内部変数が ユーザ変数の 1.2〜3 倍 まで増えるケースがあります。

2. solve のたびに内部変数が増える可能性がある

インクリメンタルで solve → add → solve を繰り返すと、
内部変数が累積的に増える。

3. resize は重いので頻繁に呼ぶべきではない

内部ベクタ・watchlist の再確保が走るため、
resize はできれば 1 回だけが理想。

実務的な「最適戦略」

🟦 1. 問題規模から最大変数数を見積もる

例：

  • ユーザ変数が最大 30 万
  • ER で 2〜3 倍増える可能性
    → 100 万〜150 万を確保しておく

🟦 2. 一度だけ大きめに resize

solver.resize(1'500'000);

🟦 3. 以降は resize を呼ばず、solver.vars() を監視

内部変数が増えるので：

int next_var = solver.vars();

ユーザ変数を追加するときは：

next_var++;
return next_var;

🟦 4. solve の後に next_var を更新

solver.solve();
next_var = solver.vars();

「200 万は多すぎるか？」の判断基準

多すぎるケース

  • 問題の最大変数が 5 万以下
  • ER がほとんど発生しない（制約が単純）
  • インクリメンタルの solve 回数が少ない

→ 20〜50 万で十分。

適切なケース

  • 問題が 10〜30 万変数規模
  • elimination や vivification が多く発生
  • solve を何度も繰り返す

→ 100〜200 万は妥当。

少なすぎるケース

  • 内部 ER が大量に発生する
  • solve を 100 回以上繰り返す
  • 変数が 30 万を超える

→ 200 万でも足りない可能性がある。

メモリ的には問題ないのか？

CaDiCaL の変数ごとの内部構造は比較的軽量で、
200 万変数でも 数百 MB 程度に収まります。

現代のメモリ環境では十分許容範囲です。

まとめ

  • 200 万が「多すぎる」かどうかは問題規模次第
  • 重要なのは resize を頻繁に呼ばないこと
  • 内部 ER 変数が増えるので solver.vars() を常に監視
  • 最初に「余裕を持って」確保しておくのが最適

あなたの問題規模（最大ユーザ変数数、インクリメンタル solve 回数、制約の種類）が分かれば、最適な resize サイズを具体的に算出できます。



結論として、**ER 変数（Extended‑Resolution 変数）に対して val() を呼ぶのは CaDiCaL 3.0 では基本的に「NG」**です。
理由は、ER 変数は ユーザが参照することを前提としていない内部専用変数であり、val() の対象として想定されていないためです。

ER 変数に val() が NG になる理由

● 1. ER 変数は「内部専用」で、ユーザ API の対象外

CaDiCaL の ER 変数は、内部の簡約化・強化・拡張解決のために自動生成される補助変数です。

  • ユーザが入力した変数ではない
  • 意味的にも「値を問い合わせる対象」ではない
  • モデルに含める保証もない
  • 削除・再利用される可能性がある

そのため、val() の対象として扱うと 未定義動作になります。

● 2. is_valid_input() が ER 変数を弾く設計になっている

CaDiCaL の内部チェックはこうなっています：

return eidx > max_var || !ervars[eidx];

つまり、

  • eidx <= max_var かつ ervars[eidx] == true
    → ユーザが触ってはいけない内部変数

という扱い。

val() も内部でこのチェックを通るため、ER 変数に対して呼ぶと assert が落ちます。

● 3. ER 変数はモデルに含まれないことがある

ER 変数は内部の式変換のためだけに存在するため、
最終モデルに値が割り当てられないこともあります。

そのため、val() が意味を持たないケースが多い。

ER 変数を避けるための実務的な設計

🟦 1. CaDiCaL の内部最大変数番号を常に監視する

int internal_max = solver.vars();

🟦 2. ユーザ変数は常に internal_max より大きい番号から割り当てる

int next_var = solver.vars();
int new_user_var() {
    next_var++;
    return next_var;
}

🟦 3. solve の後は next_var を solver.vars() で更新

内部 ER 変数が solve のたびに増えるため：

solver.solve();
next_var = solver.vars();

🟦 4. ER 変数は絶対に val() しない

ユーザ変数だけを val() の対象にする。

ER 変数を val() してしまう典型的なパターン

  • 自前で変数番号を管理していて内部変数と衝突
  • solve の後に変数を追加している
  • resize を小さく設定していて内部変数がユーザ領域に侵入
  • モデルを走査するときに 1..vars() を全部見てしまう

特に最後のケースは危険で、vars() の範囲には ER 変数も含まれるため、
モデル走査は必ず「ユーザ変数だけ」に限定する必要があります。

まとめ

  • ER 変数は内部専用 → val() は NG
  • CaDiCaL 3.0 は solve のたびに内部変数が増える
  • ユーザ変数は solver.vars() より大きい番号から割り当てる
  • モデル走査もユーザ変数だけに限定する必要がある

モデル走査部分や変数管理部分のコードを見せてもらえれば、
ER 変数を完全に避ける安全な実装に書き換えることもできます。


投稿者 時刻:

0 件のコメント:

コメントを投稿

登録: コメントの投稿 (Atom)