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


}