スケジュールナースのブログ: 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;
}

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

ロジックの解説

定数のまとめ方: 否定リテラル
が現れた場合、数式上は
です。これを
のように、定数
を右辺に送り出すことで、RHSを自動的に整理しています。
Cardinality対応: addCardinality メソッドにより、「
個のリテラル中
個以上（以下）」といった制約を直接LPの1行として出力できます。
変数の管理: 使用された最大のインデックスを追跡し、最後に一括して 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";
        // ... (以前のコードと同様) ...
    }
};

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

スケジュールナースのブログ

2026年2月21日土曜日

CNF2LPコンバータ制作

0 件のコメント:

コメントを投稿