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

---

UNSATコアとは

 UNSAT Core（充足不能コア）とは、SAT（充当可能性問題）において、問題全体が「満たせない（UNSAT）」状態になっているときに、その矛盾を引き起こしている直接的な原因（節や制約）の最小限の集まりのことです。

たとえるなら、膨大なルールの法律書（CNF問題）を読んだときに、全体として矛盾が生じている原因が、「たった3つの条文（UNSAT Core）が互いに矛盾しているせいだった」と突き止めるようなものです。

---

🔍 具体例で見る UNSAT Core

次のような 4 つの節（Clauses）からなる CNF 形式の問題があるとします。

• 節1: x1 である。 (1)
• 節2: x1 ならば x2 である。（\(\neg x1 \lor x2\)）
• 節3: x2 は偽である。（\(\neg x2\)）
• 節4: x3 または x4 である。（\(x3 \lor x4\)）

1. 全体の判定

この問題にすべての条件を満たす真偽値の割り当て（SAT）を探すと、節1・2・3の間で論理的な矛盾が発生するため、結果は UNSAT（充足不能） になります。 [1]

2. 原因（UNSAT Core）の特定

ここで注目すべきは、節4（x3 または x4）は、この矛盾に一切関係していないという点です。
矛盾を発生させている真犯人は、【節1, 節2, 節3】の組み合わせだけです。

このとき、{節1, 節2, 節3} のセットを「UNSAT Core」と呼びます。

---

💡 なぜ UNSAT Core が重要なのか？

SATソルバーを実務や研究（システムの検証、プログラムのバグ発見、回路設計、スケジューリングなど）で使う際、ただ「この条件では不可能です（UNSAT）」と言われるだけでは、「どこを修正すればいいのか」が分かりません。

UNSAT Core を抽出することで、以下の大きなメリットが得られます。

• デバッグ・修正の効率化:
  数百万行ある膨大な制約の中から、矛盾に関係している「数十行の制約」だけを絞り込めるため、どこを直せば仕様を満たせるのかがすぐに分かります。
• 不要なルールの特定:
  システムの仕様同士が衝突している場所（設計ミス）をピンポイントで特定できます。

🛠️ 2つの「UNSAT Core」の種類

ツール（drat-trim など）でコアを抽出する際、文脈によって2つのレベルがあります。

1. MUS（Minimal Unsatisfiable Subscript / 最小充足不能部分集合）
   • そのコアからどれか1つでも節を外すと、矛盾が消えて（SATに）なってしまうような、極限まで削ぎ落とされた原因のセット。
2. 一般的な UNSAT Core
• ソルバーが探索の過程で見つけた「矛盾に関わった節の集まり」。MUSほど厳密に最小化されていない場合もありますが、実用上は十分に小さく絞り込まれています。

Q.　drat-trimは、MUSを出力するか？

結論から言うと、drat-trim は「一般的なUNSAT Core」を出力しますが、厳密な「MUS（最小充足不能部分集合）」を必ず出力するとは限りません。 [1]

drat-trim が行う処理は Trimming（トリミング：削減） であり、正確には 「MUSに近いサイズまで大幅に削ぎ落としたUNSAT Core」 を出力するツール です。 [1, 2, 3, 4]

その理由と、MUSを得るための具体的なアプローチについて解説します。

---

1. drat-trim の内部の仕組み（なぜMUSにならないのか）

drat-trim は、ソルバーが出力した「証明ログ（DRAT）」を、最後の矛盾点（空節）から逆方向にトレース（Backward Checking） します。 [1]

1. 判定: 矛盾の証明に「実際に使われた節」だけをマークする。
2. 結果: 探索中に1度も使われなかった節はすべて排除される。 [1]

この時点で、元のCNFから不要な節が90%〜99%以上削られた非常に小さなUNSAT Coreが得られます。しかし、探索中に「たまたま余計に使われてしまった節（なくても矛盾が証明できる節）」が残ってしまうことがあるため、数学的な意味での「これ以上1つも削れない状態（MUS）」の保証には至りません。 [1, 2, 3]

2. drat-trim を何度も回してMUSに近づけるアプローチ [1]

drat-trim の機能を利用して、極限までMUSに近づける（あるいはMUS化する）ために、研究や実務ではループ（反復クレンジング）という手法が使われます。 [1]