CryptiminisatでCNF生成

 仕方なく、CNFを生成して他のソルバで、DRATを出力させようと思いました。

void write_cnf(string filename) {

    solver->open_file_and_dump_irred_clauses(filename);

}

ところが、UNSATの場合、CNFは、UNSATを意味する1行しか出力されておらず、元のCNF構成は、忘れてしまって出力できないようです。

仕方なく、自前でCNFを出力させました。

C++ で直接ファイルに書き出す場合

CryptoMiniSatのC++ API（solver.open_file_and_dump_irred_clauses()）などは、高速化の都合上 p cnf ... のヘッダーを自動で出力してくれない仕様になっています。
そのため、C++でソルバーに節を投入するのと同時に、自前で文字列ストリームなどに一時保存して書き出すのが確実です。 [1]

cpp

#include <iostream>
#include <fstream>
#include <vector>
#include <cmath>
#include <algorithm>

int main() {
    // 追加したい節のデータ
    std::vector<std::vector<int>> clauses = {
        {1, 2, 3},
        {-1, -2},
        {-1, -3}
    };

    // 変数の最大数と節の数をカウント
    int max_var = 0;
    for (const auto& clause : clauses) {
        for (int lit : clause) {
            max_var = std::max(max_var, std::abs(lit));
        }
    }
    int num_clauses = clauses.size();

    // ファイル書き出し
    std::ofstream outfile("problem.cnf");
    if (outfile.is_open()) {
        // ヘッダーを最初に出力
        outfile << "p cnf " << max_var << " " << num_clauses << "\n";

        // 各節と末尾の0を出力
        for (const auto& clause : clauses) {
            for (int lit : clause) {
                outfile << lit << " ";
            }
            outfile << "0\n";
        }
        outfile.close();
    }
    return 0;
}

しかし、上のコードは、Kissat等で用いられる形式で、CryptiminisatのMinisat伝統のLit形式ではありません。
そこで、仕方なく、自前で書きました。

void write_cnf(string filename) {
//    solver->open_file_and_dump_irred_clauses(filename);
    int max_var = 0;
    for (const auto& clause : lits_vec) {
        for (auto lit : clause) {
            if (max_var < (lit.var() + 1)) {
                max_var = lit.var() + 1;// std::max(max_var, std::abs(lit.var()));
            }

        }
    }
    int num_clauses = lits_vec.size();

    // ファイル書き出し
    std::ofstream outfile(filename);
    if (outfile.is_open()) {
        // ヘッダーを最初に出力
        outfile << "p cnf " << max_var << " " << num_clauses << "\n";

        // 各節と末尾の0を出力
        for (const auto& clause : lits_vec) {
            for (auto lit : clause) {
                if (lit.sign()) {
                    int v = -(int)(lit.var() + 1);
                    outfile <<v<< " ";
                }

                else {
                    int v = (lit.var() + 1);
                    outfile << v<<" ";
                }
                
            }
            outfile << " 0\n";
        }
        outfile.close();
    }


}

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