CryptminisatでDRAT生成

 Daily Cumulative Totalizerのデバッグで、DRATを使いたかったので以下の通りやってみました。

が、使っているCryptminisatのバージョンでは、上手く生成してくれませんでした。

CryptoMiniSat（CMSAT）のC++ APIでDRAT（DRAT証明 / Proof logging）を出力してUNSAT reason（矛盾の証明・最小化コア）を得るには、ソルバーオブジェクトにostream（またはファイルポインタ）をセットして探索を実行し、出力されたDRATログを外部ツール（drat-trim）で解析するフローをとります。

大規模問題では、先述の get_conflict()（変数単体の原因特定）よりも、このDRATによる「どの節の組み合わせが矛盾を招いたか」の証明ログ出力が標準的です。

---

1. C++ API側でのDRAT出力設定

CMSATの SATSolver クラスは、DRAT証明の出力先を直接指定するためのメソッド set_drat() （または環境により open_proof_file()）を提供しています。

cpp

#include <cryptominisat5/cryptominisat.h>
#include <fstream>
#include <iostream>
#include <vector>

using namespace CMSat;

int main() {
    SATSolver solver;

    // 1. DRAT出力用のファイルをオープン
    std::ofstream drat_file("proof.drat", std::ios::out | std::ios::binary);
    if (!drat_file) {
        std::cerr << "ファイルを開けません" << std::endl;
        return 1;
    }

    // 2. ソルバーにDRATストリームをセット
    // ※ 探索中の「学習節の追加」「不要節の削除」がこのファイルに自動記録されます
    solver.set_drat(&drat_file, false); // 第二引数はバイナリモード(FRAT等)にするかフラグ

    // --- 通常通りの問題定義 ---
    solver.new_vars(3);
    solver.add_clause({Lit(0, false), Lit(1, false)}); //  x1 v x2
    solver.add_clause({Lit(0, true)});                 // -x1
    solver.add_clause({Lit(1, true)});                 // -x2

    // 3. 探索を実行
    lbool result = solver.solve();

    // 4. ファイルを確実にクローズしてバッファを書き出す
    solver.set_drat(nullptr, false); 
    drat_file.close();

    if (result == l_False) {
        std::cout << "結果: UNSAT。 proof.drat に証明を出力しました。" << std::endl;
    }

    return 0;
}

UNSAT APPROACH

 MAXSATのアプローチの仕方としては、SATから攻める方法と、UNSATから積み上げていく方法があります。

基本的にスケジュールナースのAL1で使っているのは、上のSAT Approachになります。厳密解かどうかは、現在の目的関数値未満の値がUNSATとなることによって初めて、判明します。現在の目的関数値を下回る解が存在しない(UNSAT)を示すことに必要となるので、このハードルは、極めて高いです。ある目的関数値が示すことであれば、その1点だけに注力すればよいのですが、あらゆるケースにおいて存在しないことを示さないとUNSATとは言えないからです。

一方UNSAT approachは、Fu & Malikによって開発されたアルゴリズムで、UNSATを下から積み上げてゆく方式で、SATになったときに厳密解となります。

この方法は、前述のassumptionを用いることが必須です。この方式の難点は、UNSATのまま停滞することが多く、SAT解がえられないまま終わることが多い、つまり解が得られないまま終わる、ということです。スケジュールナースの実務インスタンスで言えば、ほとんどエラーのないインスタンスのみしか適用することが出来ないので、効果的な場面は存在するものの、汎用的ではありません。

残念なことに、kissatが、incremental/assumptionの実装を放棄した関係で、MAXSAT関係では、最新SATソルバの恩恵を得ることが出来ずに、最近の進歩は停滞しています。

UNSATコア取得別方法

 kissat以外では、大体assumptionが使えます。assumptionを引数として渡してUNSATが返ってくると、get_conflict()で、assumption bitsでのUNSATコアを取得することが出来ます。これを用いて、MAXSATでは、SAT解が出るまでunsatを積み重ねていく厳密解法があります。

CryptoMiniSat（CMSAT）のC++ APIでUNSATの原因（矛盾を引き起こした仮定のサブセット）を取得するには、solver.get_conflict() メソッドを使用します。

この機能を利用するには、あらかじめ変数や節（Clause）をそのまま解くのではなく、原因を特定したいリテラルを「仮定（Assumptions）」として solve() に渡す必要があります。

実装コード例

以下は、仮定（Assumptions）に矛盾がある場合に、その原因となったリテラル（UNSAT reason）を抽出する最小限の実装例です。

cpp

#include <cryptominisat5/cryptominisat.h>
#include <vector>
#include <iostream>

using namespace CMSat;

int main() {
    SATSolver solver;
    
    // 3つの変数を定義 (変数のインデックスは0から始まります)
    solver.new_vars(3);

    // 通常の節(Clauses)を追加
    // 例: (x1 ∨ x2)
    solver.add_clause({Lit(0, false), Lit(1, false)}); 

    // 矛盾を発生させるための「仮定(Assumptions)」を設定
    // 例: 「x1は偽(NOT x1)」かつ「x2は偽(NOT x2)」と仮定する
    std::vector<Lit> assumptions = {Lit(0, true), Lit(1, true)};

    // 仮定のリストをポインタで渡してソリューションを実行
    lbool result = solver.solve(&assumptions);

    if (result == l_False) {
        std::cout << "結果: UNSAT (充足不能)" << std::endl;
        std::cout << "--- 矛盾の原因 (UNSAT Reason) ---" << std::endl;

        // 矛盾を引き起こした仮定のサブセット（Conflict）を取得
        const std::vector<Lit> conflict = solver.get_conflict();

        for (const Lit& lit : conflict) {
            // 変数番号は0始まりなので、1始まり(DIMACS形式)に直して表示
            uint32_t var_num = lit.var() + 1;
            
            // lit.sign() が true の場合は否定（負のリテラル）
            if (lit.sign()) {
                std::cout << "-" << var_num << " ";
            } else {
                std::cout << var_num << " ";
            }
        }
        std::cout << std::endl;
    } else if (result == l_True) {
        std::cout << "結果: SAT (充足可能)" << std::endl;
    } else {
        std::cout << "結果: INDET (タイムアウトなどで未決定)" << std::endl;
    }

    return 0;
}

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

重要なポイント

1. Lit の構造: Lit(var_id, is_inverted)
   • 第一引数 var_id は 0 始まりの変数インデックスです。
   • 第二引数 is_inverted は、true で否定（\(\neg x\)）、false で肯定（x）を表します。
2. get_conflict() の中身:
   • solve() が l_False を返した直後に呼び出す必要があります。
   • 返されるベクターには、渡した仮定（assumptions）の中から矛盾の直接的な引き金となったリテラルだけが含まれます。

---