制約充足問題のモデリング

論理変数の組み合わせで矛盾しない割り当てを求める問題において、各制約が「Aを選択するならばBは不可」のような2項条件に限定される場合、2-SATアルゴリズムが有効です。この手法は、論理式を有向グラフとして表現し、強連結成分(SCC)の解析を通じて解の存在を判定します。

グラフ構築のポイント

各変数xについて、2つのノードを定義します：

• x_true：変数xを真とする選択
• x_false：変数xを偽とする選択

制約条件「xが真ならばyは偽」は、x_true → y_false およびその逆命題 y_true → x_false の2本の有向辺で表現されます。この対称性が解法の根幹となります。

解の存在判定アルゴリズム

グラフを構築後、Tarjanのアルゴリズムで強連結成分を抽出します。任意の変数xについて、x_true と x_false が同一のSCCに含まれない場合に限り、充足可能な割り当てが存在します。

実装コードの最適化

以下のサンプルでは、再帰呼び出しをスタックベースの実装に置き換え、メモリ効率を改善しています：

// 変数管理クラス
class VariableManager {
    vector<vector<int>> graph;
    vector<int> index, lowlink, component;
    stack<int> stk;
    int counter = 0, compCount = 0;

public:
    explicit VariableManager(int n) : graph(2 * n + 1) {}

    void addConstraint(int a, bool aVal, int b, bool bVal) {
        int aNode = getNode(a, aVal);
        int bNode = getNode(b, bVal);
        graph[getNode(a, !aVal)].push_back(bNode);
        graph[getNode(b, !bVal)].push_back(aNode);
    }

    bool solve(vector<bool>& assignment) {
        int n = graph.size() / 2 - 1;
        assignment.resize(n + 1);
        for (int i = 1; i <= 2 * n; ++i) {
            if (index[i] == 0) tarjan(i);
        }
        for (int i = 1; i <= n; ++i) {
            if (component[2 * i] == component[2 * i + 1]) 
                return false;
            assignment[i] = component[2 * i] < component[2 * i + 1];
        }
        return true;
    }

private:
    int getNode(int var, bool value) {
        return 2 * var + (value ? 0 : 1);
    }

    void tarjan(int start) {
        stack<int> dfsStack;
        dfsStack.push(start);
        
        while (!dfsStack.empty()) {
            int node = dfsStack.top();
            if (index[node] == 0) {
                index[node] = lowlink[node] = ++counter;
                stk.push(node);
                for (int next : graph[node]) {
                    if (index[next] == 0) {
                        dfsStack.push(next);
                    } else if (component[next] == 0) {
                        lowlink[node] = min(lowlink[node], index[next]);
                    }
                }
            } else {
                dfsStack.pop();
                for (int next : graph[node]) {
                    if (component[next] == 0) {
                        lowlink[node] = min(lowlink[node], lowlink[next]);
                    }
                }
                if (lowlink[node] == index[node]) {
                    int w;
                    do {
                        w = stk.top(); stk.pop();
                        component[w] = compCount;
                    } while (w != node);
                    ++compCount;
                }
            }
        }
    }
};

応用例：論理式の充足可能性検証

論理式 (A∨B)∧(¬B∨C) の充足可能性を判定する場合：

VariableManager solver(3);
// (A∨B) → ¬A→B, ¬B→A
solver.addConstraint(1, false, 2, true);
solver.addConstraint(2, false, 1, true);
// (¬B∨C) → B→C, ¬C→¬B
solver.addConstraint(2, true, 3, true);
solver.addConstraint(3, false, 2, false);

vector<bool> result;
if (solver.solve(result)) {
    cout << "Solution found: ";
    for (int i = 1; i < result.size(); ++i) {
        cout << "X" << i << "=" << result[i] << " ";
    }
}

この実装では、SCCのインデックス比較により、各変数の真偽値を効率的に決定しています。トポロジカル順序の逆順となるSCC番号の大小関係から、矛盾しない割り当てを導出することが可能です。