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が動かない>

以下でエラー出るので、これも切っています。copyは、この他にissueが上がっていました。

copy the extension status (#158) · arminbiere/cadical@d27907a

この辺、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

  }

新しいアークテクチャに方針変更

 instance24が解けない

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

ので、

１）ローカルソルバ検討

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

２）時間制約の検討

https://schedule-nurse.blogspot.com/2026/02/instance24timeencode.html

３）MDDの検討

https://schedule-nurse.blogspot.com/2026/02/pb-bdd.html

https://schedule-nurse.blogspot.com/2026/02/mdd_14.html

と検討を行ってきました。

当初、軽いローカルソルバを目指していましたが、この壁に立ち向かうには、世界最高性能のMAXSATソルバをスクラッチからデザインし直すのが最も早道との考えに改めました。10年間続いた基幹アルゴリズムを変更することは、勇気が要りますが、それよりもinstance24を解くことの方が大事です。別途、開発スケジューリングの見直しを行うこととします。

新しいアーキテクチャは、ソルバ群の連携を前提にしたものです。個々の部品としても機能しますが、それよりは、各ソルバとの連携により新たな価値を生むことを前提に設計しています。こうした発想は、以前はありませんでした。同一問題を色々なアプローチから取り組み、互いの強みを生かして、相互連携により解けなかった問題を解けるようにすることを目的にしています。MaxSATソルバもそのための一部品という位置づけになります。ポートフォリオと言うよりは、複数の全く別のアプローチにより一つの目標を達成するアーキテクチャです。

解けなかったことが、逆に、新しいアーキテクチャを促し新しいソルバを生み出す原動力になっているので、解けなかったことに、むしろ感謝しなくてはいけない、と今は、思っています。

AE-Kissat-MABをWindowsにポート

AE-Kissat-MABは、SAT Competition 2025の優勝ソルバです。 

The Results of SAT Competition 2025

下のプロットを見ると他のソルバよりも明確な優位性が見られます。

このソルバは、生成AIでコードチューニングされています。

近年SAT Competitionの進歩は緩慢であり、これほどに大きなゲインは、Kissatの登場以来ではないかと思います。

しかし、この数か月後にNVIDA　SATLUTIONは、さらにこの上を行く発表しています。

https://schedule-nurse.blogspot.com/2026/02/saturation_9.html

が、コードは公開されていません。なので、現時点で、公開されている利用可能なSATソルバの頂点に位置するソルバと考えてよいです。

インスタンス24を解くには、やはりCardicalではメモリ使用量に難点があり、Kissatに頼らざるを得ない、ならば、最新ソルバを使用してみたい、という発想です。

で、疑似インクリメンタルな実装にしてみました。

https://schedule-nurse.blogspot.com/2026/02/kissatincremental.html

次が、作成したAPIです。胆は、

１）Phaseのセットができる

２）UnitClauseを含めた学習節のExport/Importが可能

３）簡略化で消されないようにするFreeze機能を装備

４）VSIDS/CHBのスコアをExport/Import

これにより、複数回Solveしても、問題なく求解できます。完全なシリアライズではありませんが、上記機能により主要な諸元は、リストアすることが出来ます。ほぼ、Warm Start機能を実現しました。問題なく機能が確認出来た後、Githubにアップします。

これでインスタンス24攻略に向けての最終部品がほぼ出来ました。Time制約のリソース改善を行った後、今後，各ソルバ群の統合化作業を行い、再挑戦を行う予定です。長い長い登攀でしたが、ようやく辿り着けそうな気がしてきました。

#ifndef KISSAT_WIN_API_H
#define KISSAT_WIN_API_H

#include "kissat.h"
#include 

// Windows特有の初期化（信号ハンドラやリソース制限のダミー設定）
kissat * kissat_win_init (void);

// 変数の保護（簡約化による消滅を防止）
void kissat_win_freeze_variables (kissat *solver, int first, int last);

// 外部から値をセットして求解し、学習内容を保存する一括処理
// 戻り値: 10 (SAT), 20 (UNSAT), 0 (UNKNOWN)
int kissat_win_solve_step (
    kissat *solver, 
    const int *phases,      // 変数1〜Nに対するTrue(1)/False(0)の配列
    int num_phases, 
    unsigned lbd_limit,     // 学習節の保存しきい値 (7等)
    const char *learned_path // 学習節の保存先 (NULLなら保存しない)
);

// 解（Model）の取得
int kissat_win_get_value (kissat *solver, int lit);

#endif

CNF2LPコンバータ制作

 世の中には、既にあるので、目新しくはありません。

msakai/toysolver: My sandbox for experimenting with solver algorithms.

作者は、Preferred Networks, Inc.の酒井さんです。色々なフォーマットのコンバージョンをサポートしています。

以下に、AIとの会話を示します。コードも書いてありますが、しっかりバグがありました。行頭が、（マイナス）ー項で始まると、ーが除去されてしまうので、使用しないでください。

MPSファイルもFortran風の謎の記述制約がありますが、LPファイルもその流れを汲んでいるようです。この時代のパーサを組んだ人は、古風な記法が好きなのかな？と思いました。

AT（充足可能性問題）の構造をLP（線形計画法）ファイル形式で記述する場合、主にCPLEX LPフォーマットが標準的に利用されます。この形式は人間が読みやすい代数的な記述が特徴です。 

以下に、LPファイルの主要なセクションとその構造を解説します。

1. 目的関数 (Objective Function)

「Maximize」または「Minimize」で始めます。SAT問題を単に解くだけ（充足可能性の判定）なら、目的関数は定数（例：0）でも構いません。 

text

Maximize
 obj: 0

コードは注意してご使用ください。

2. 制約式 (Constraints)

「Subject To」（または st）で始め、SATの各節（クローズ）を不等式として記述します。 

• 変数の表現: 各論理変数を 
  

  $$
   とし、真を 
  

  $$
  、偽を 
  

  $$
   とみなします。
• 節の変換: 例えば節 
  

  $$
   は、
  

  $$
   と記述します。

text

Subject To
 c1: x1 - x2 + x3 >= 0
 \ (x1 + (1 - x2) + x3 >= 1 を整理したもの)

コードは注意してご使用ください。

3. 変数の範囲と型 (Bounds & Types)

SAT変数は 

$$

 か 

$$

 の値しか取らないため、バイナリ変数として宣言します。 

• Bounds: 変数の下限・上限を指定します（バイナリ宣言すれば省略可能）。
• Binaries: 変数を 
  

  $$
   または 
  

  $$
   に制限します。

text

Binaries
 x1 x2 x3

コードは注意してご使用ください。

4. 終了キーワード

ファイルの最後には必ず End を記述します。 

---

LPファイルの全体構成例

SATの節 

$$

 と 

$$

 を表現する例です。

text

\ コメントはバックスラッシュで記述可能
Maximize
 obj: 0
Subject To
 c1: x1 - x2 >= 0       \ x1 + (1 - x2) >= 1
 c2: - x1 + x3 >= 0      \ (1 - x1) + x3 >= 1
Binaries
 x1 x2 x3
End

コードは注意してご使用ください。

実装上の注意点:

• 変数名: アルファベットで始め、最大255文字まで使用可能です。
• 定数項: 変数のない定数は、制約式の右辺（RHS）に寄せる必要があります。
  
  
  
  changeColBound的な事は、LPファイル上ではできないのですね。
  いいえ、LPファイル（CPLEX LPフォーマット）でも変数の境界（Bounds）を個別に指定する

  Bounds セクションが存在します。 

  API（changeColBound 等）のようにプログラム実行中に動的に変更するのではなく、ファイル記述として変数の動域を制限することが可能です。

  LPファイルでの境界指定（Bounds）

  制約式（Subject To）の後、Binaries や End の前に Bounds セクションを設けます。

  記述ルール

  • デフォルトでは、すべての変数は 
    

    $$
     （非負）とみなされます。
  • SAT問題でバイナリ変数として扱う場合は、後述の Binaries セクションに書けば自動的に 
    

    $$
     または 
    

    $$
     に固定されますが、Bounds で明示的に書くこともできます。 

  例：特定の変数の範囲を固定・制限する 

  text

  Subject To
   ... (制約式) ...
  
  Bounds
    x1 = 1            \ x1 を 1 に固定 (真に固定)
    0 <= x2 <= 1      \ x2 の範囲を指定
    x3 >= 0.5         \ 下限だけ指定
    x4 free           \ x4 を自由変数（-∞ to +∞）にする
  
  Binaries
    x1 x2 x3 x4
  End
  

  コードは注意してご使用ください。

  まとめ：APIとの対応

  • プログラム(API): lp.set_col_bounds(col, lb, ub) や changeColBound で逐次変更。
  • LPファイル: Bounds セクションに lb <= var <= ub の形式で静的に記述。 

  もし、SATの「特定の変数に特定の値を割り当てた状態（Partial Assignment）」で解きたい場合は、この Bounds セクションで x1 = 1 のように記述するのが正解です。
  
  

HIGHSは、LPファイルをサポートしていますか？

はい、

HiGHSはLPファイル（CPLEX LPフォーマット）を公式にサポートしています。 1.2.2, 1.3.6 

HiGHS Documentationによると、.lp という拡張子のファイルを読み込むことで、モデルを自動的に解釈して実行できます。 

C++コードコンバータは、出来ますか？　通常CNF用と、Cardinals用があると良いです。RHSに定数をまとめてくれるのを希望。

SATの節（CNF）および基数制約（Cardinality Constraints）を、定数項を右辺（RHS）にまとめたLPファイル形式へ変換するC++クラスを作成しました。

このコンバータは、各変数を 

$$

 として出力し、否定リテラル 

$$

 を 

$$

 と展開して定数項を計算します。

SAT to LP Converter (C++)

cpp

#include <iostream>
#include <vector>
#include <string>
#include <numeric>
#include <fstream>

class SatToLpConverter {
private:
    int max_var_index = 0;
    std::vector<std::string> constraints;

    void update_max_var(const std::vector<int>& literals) {
        for (int lit : literals) {
            max_var_index = std::max(max_var_index, std::abs(lit));
        }
    }

public:
    // 通常のCNF節 (l1 v l2 v ... v ln) -> l1 + l2 + ... >= 1
    void addClause(const std::vector<int>& literals) {
        update_max_var(literals);
        long rhs = 1;
        std::string expr = "";

        for (size_t i = 0; i < literals.size(); ++i) {
            int lit = literals[i];
            if (lit > 0) {
                expr += (expr.empty() ? "" : " + ") + ("x" + std::to_string(lit));
            } else {
                expr += (expr.empty() ? "" : " - ") + ("x" + std::to_string(-lit));
                rhs -= 1; // (1 - x) の 1 を右辺へ移動
            }
        }
        constraints.push_back(expr + " >= " + std::to_string(rhs));
    }

    // 基数制約 (At-least-k, At-most-k)
    // is_at_least=true で >= k, false で <= k
    void addCardinality(const std::vector<int>& literals, int k, bool is_at_least = true) {
        update_max_var(literals);
        long rhs = k;
        std::string expr = "";

        for (int lit : literals) {
            if (lit > 0) {
                expr += (expr.empty() ? "" : " + ") + ("x" + std::to_string(lit));
            } else {
                expr += (expr.empty() ? "" : " - ") + ("x" + std::to_string(-lit));
                rhs -= 1;
            }
        }
        std::string op = is_at_least ? " >= " : " <= ";
        constraints.push_back(expr + op + std::to_string(rhs));
    }

    void writeToFile(const std::string& filename) {
        std::ofstream out(filename);
        out << "Minimize\n obj: 0\nSubject To\n";
        for (size_t i = 0; i < constraints.size(); ++i) {
            out << " c" << i << ": " << constraints[i] << "\n";
        }
        out << "Binaries\n";
        for (int i = 1; i <= max_var_index; ++i) {
            out << " x" << i << (i % 10 == 0 ? "\n" : " ");
        }
        out << "\nEnd\n";
    }
};

int main() {
    SatToLpConverter conv;
    // 節 (x1 v -x2 v x3)
    conv.addClause({1, -2, 3});
    // 基数制約: x1 + x4 + x5 >= 2
    conv.addCardinality({1, 4, 5}, 2, true);
    
    conv.writeToFile("output.lp");
    return 0;
}

コードは注意してご使用ください。

ロジックの解説

1. 定数のまとめ方: 否定リテラル 
   

   $$
    が現れた場合、数式上は 
   

   $$
    です。これを 
   

   $$
    のように、定数 
   

   $$
    を右辺に送り出すことで、RHSを自動的に整理しています。
2. Cardinality対応: addCardinality メソッドにより、「
   

   $$
    個のリテラル中 
   

   $$
    個以上（以下）」といった制約を直接LPの1行として出力できます。
3. 変数の管理: 使用された最大のインデックスを追跡し、最後に一括して Binaries セクションに出力します。

このコードで生成された output.lp を HiGHS C++ API の highs.readModel("output.lp") で読み込めば、そのまま最適化計算が可能です。

ごめんなさい。MIPではなく、LPソルバとして機能させる場合には、どうしたらよいのですか？Boundはそのままに。

SAT問題を純粋な

LP（線形計画法）として解く場合、変数が 

$$

 または 

$$

 という制約を外し、

$$

 の連続変数として扱うことになります。

HiGHSをLPソルバーとして動作させるための手順は以下の通りです。

1. LPファイルの記述を変更する

LPファイル内の Binaries セクションを削除し、代わりに Bounds セクションで範囲を指定します。

text

\ Binaries セクションを削除し、以下のように記述
Bounds
 0 <= x1 <= 1
 0 <= x2 <= 1
 ...
End

コードは注意してご使用ください。

2. C++コンバータの修正

先ほどのコードの writeToFile メソッド内の Binaries 出力部分を、以下のように Bounds 出力に書き換えます。

cpp

void writeToFile(const std::string& filename) {
    std::ofstream out(filename);
    out << "Maximize\n obj: 0\nSubject To\n";
    for (size_t i = 0; i < constraints.size(); ++i) {
        out << " c" << i << ": " << constraints[i] << "\n";
    }
    // Binaries の代わりに Bounds を使用
    out << "Bounds\n";
    for (int i = 1; i <= max_idx; ++i) {
        out << " 0 <= " << getVarName(i) << " <= 1\n";
    }
    out << "End\n";
}

目的関数値の書き方を教えて。SATでは、ビットxkに対して制約違反重みを定数Coeffkで与える。

SATの制約違反に重み（コスト）を持たせる場合、それは一般的に

Weighted MaxSATの形式となります。LPファイルにおいて、特定のビット（変数）

$$

 が「真」になった際のコスト 

$$

 を目的関数に反映させる書き方は以下の通りです。

1. LPファイルでの記述形式

目的関数セクション（Minimize または Maximize）に、変数と係数の積を並べます。

方針: 制約違反を最小化したい場合、違反を表す変数 

$$

 にコスト 

$$

 を掛けて Minimize します。

text

Minimize
 obj: Coeff1 x1 + Coeff2 x2 + Coeff3 x3 ...
Subject To
 ... (SATの制約式) ...
Binaries
 x1 x2 x3 ...
End

コードは注意してご使用ください。

---

2. C++コンバータへの組み込み例

変数のインデックス 

$$

 と重み 

$$

 を紐付ける std::map を使い、目的関数行を生成するロジックを追加します。

cpp

#include <map>
#include <string>
#include <vector>
#include <fstream>

class SatToLpConverter {
private:
    std::map<int, double> weights; // 変数インデックス -> 重み(Coeff)
    // ... 他のメンバ変数 ...

public:
    // 特定の変数に重みを設定
    void setWeight(int idx, double coeff) {
        weights[idx] = coeff;
    }

    void writeToFile(const std::string& filename) {
        std::ofstream out(filename);
        
        // 1. 目的関数の出力
        out << "Minimize\n obj: ";
        bool first = true;
        for (auto const& [idx, coeff] : weights) {
            std::string name = getVarName(idx);
            if (!first && coeff >= 0) out << " + ";
            else if (coeff < 0) out << " - ";
            
            out << std::abs(coeff) << " " << name;
            first = false;
        }
        if (first) out << "0"; // 重みが設定されていない場合
        out << "\n";

        // 2. 制約式以降の出力
        out << "Subject To\n";
        // ... (以前のコードと同様) ...
    }
};

コードは注意してご使用ください。