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）の中から矛盾の直接的な引き金となったリテラルだけが含まれます。

---