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;
}