Cadical 3.0をWindowsにポート

 前回と同じように行ったのですが、

https://schedule-nurse.blogspot.com/2026/01/caidical.html

3.0になってポート出来ない箇所(congruence　ゲート抽出)がありました。原因はほぼ分かっています。ポートの問題ではなくCadicalのバグの可能性が大です。

プリプロセスだけの話なので、切って使うことにしました。

問題箇所は、

sort_literals_by_var (g->rhs);

Gate *h = find_and_lits (g->rhs, g);

にあるらしいことは掴めました。table に入れた Gate の rhs を後から変更すると、unordered_set の内部構造が壊れる。C++のUBらしいです。しかし、該当箇所は沢山ありまして、バグFixまでには至りませんでした。GCCでは検出されなくて、MSVCで検出されるのは、これでCadical2回目になります。結構な人が使っていると思うのですが、未だ枯れてないんですね。

もう少し、綺麗で安全な書き方があると思うのですが...congruence　は鬼門です。

とりあえず使うには、以下のように切ります。

bool Internal::extract_gates (bool remove_units_before_run) {

    #ifdef _WIN32

  return false;//Cong

なお、このオプションがなくても、性能劣化は殆ど私のプロジェクトではありません。

ゲート抽出は、x1==x2となっているところを抽出して節を削減する手法です。一般にXORゲートを多用する暗号化、または、LSI演算回路系検証等のCNFには効果が期待できますが、私のプロジェクトでは、UnitPropagationを重視していてUnitPropagationを阻害するXORゲート記述は、基本使用禁止です。なので、なくても差しさわりありません。

Biere教授に報告すべき案件ですが、バグFIXできていないので確信が持てずレポートはしていません。

<copyが動かない>

以下でエラー出るので、これも切っています。

この辺、AIに聞いても、Windowsポートの問題（あなたの問題）という立ち位置で、取り合ってくれませんでした。ポートの問題ではないことは確認済みで、これも修正すべきと思います。AIも先入観があるのか、あるいは最新版のビルドに関して学習が済んでいないのか分かりませんが、意外に人間っぽいと思います。

void Solver::add (int lit) {

  TRACE ("add", lit);

  REQUIRE_VALID_STATE ();

  if (lit) {

      #ifndef _WIN32

    if (internal->opts.factor && internal->opts.factorcheck == 1)

      REQUIRE (

          abs (lit) <= external->max_var,

          "adding literal '%d' with undeclared variable '%d' "

          "(checking that user variables are declared explicitly failed "

          "as both 'factor' and 'factorcheck' are enabled)",

          lit, (int) abs (lit));

    if (internal->opts.factorcheck == 2)

      REQUIRE (

          abs (lit) <= external->max_var,

          "adding literal '%d' with undeclared variable '%d' "

          "(checking that user variables are declared explicitly failed "

          "as 'factorcheck == 2' even if 'factor' is disabled)",

          lit, (int) abs (lit));

    #endif

  }