Skip to content

2-SAT

2-SAT implication graph: clauses become directed edges between literals

Satisfying Boolean Clauses with Graph Theory

You have N boolean variables and M clauses. Each clause says "at least one of these two literals must be true." Can you assign true/false to every variable so all clauses are satisfied? This is 2-SAT, and it reduces to SCC on a special directed graph called the implication graph.

The 2-SAT Problem

A 2-SAT formula has this shape:

(a1 OR b1) AND (a2 OR b2) AND ... AND (am OR bm)

Each clause has exactly 2 literals. A literal is either a variable xi or its negation NOT xi. The question: is there an assignment of true/false to each variable that satisfies every clause?

3-SAT (clauses of size 3) is NP-complete. But 2-SAT is solvable in O(N + M) time.

The Implication Graph

The clause (a OR b) is logically equivalent to two implications: - NOT a -> b (if a is false, b must be true) - NOT b -> a (if b is false, a must be true)

Build a directed graph with 2N nodes: for each variable xi, create node xi (true) and node NOT xi (false). For each clause, add two directed edges.

Node encoding: Variable i (1-indexed) uses node i for the positive literal and node i + N for the negative literal.

int neg(int x, int n) {
    return x <= n ? x + n : x - n;
}

void addClause(int a, int b, int n) {
    int na = neg(a, n), nb = neg(b, n);
    adj[na].push_back(b);
    radj[b].push_back(na);
    adj[nb].push_back(a);
    radj[a].push_back(nb);
}

💡 Key insight. The implication graph captures all forced assignments. If you set a literal to true, follow its outgoing edges to see what else must be true. A chain of implications is a path in the graph.

Why SCCs Solve 2-SAT

If nodes xi and NOT xi are in the same SCC, that means xi implies NOT xi (through some chain) AND NOT xi implies xi. Both can't be true simultaneously. The formula is unsatisfiable.

If no variable shares an SCC with its negation, the formula is satisfiable. To extract the assignment:

  • For each variable i, compare the SCC IDs of i and i+N.
  • Set variable i to true if comp[i] comes later in topological order than comp[i+N].
  • Kosaraju's gives SCCs in topological order (comp 0 first), so "later" means higher comp ID.
bool satisfiable = true;
vector<bool> val(n + 1);
for (int i = 1; i <= n; i++) {
    if (comp[i] == comp[i + n]) {
        satisfiable = false;
        break;
    }
    val[i] = (comp[i] > comp[i + n]);
}

⚠ Gotcha. The comparison comp[i] > comp[i+n] depends on Kosaraju's ordering convention. If your SCC algorithm gives SCCs in the opposite order (Tarjan's does), flip the comparison.

Full 2-SAT Template

#include <bits/stdc++.h>
using namespace std;

const int MAXN = 400005;
vector<int> adj[MAXN], radj[MAXN];
int comp[MAXN];
bool vis[MAXN];
vector<int> order;

void dfs1(int u) {
    vis[u] = true;
    for (int v : adj[u])
        if (!vis[v]) dfs1(v);
    order.push_back(u);
}

void dfs2(int u, int c) {
    comp[u] = c;
    for (int v : radj[u])
        if (comp[v] == -1) dfs2(v, c);
}

int n; // number of variables

int neg(int x) { return x <= n ? x + n : x - n; }

void addClause(int a, int b) {
    int na = neg(a), nb = neg(b);
    adj[na].push_back(b);  radj[b].push_back(na);
    adj[nb].push_back(a);  radj[a].push_back(nb);
}

// Force literal a to be true: add clause (a OR a)
void forceTrue(int a) { addClause(a, a); }

int main() {
    int m;
    cin >> n >> m;

    for (int i = 0; i < m; i++) {
        // Read clause. Positive literal i = variable i.
        // Negative literal = i + n.
        int a, b;
        cin >> a >> b;
        // Adjust signs as needed per problem format
        addClause(a, b);
    }

    int total = 2 * n;
    for (int i = 1; i <= total; i++)
        if (!vis[i]) dfs1(i);

    memset(comp, -1, sizeof(comp));
    int numSCC = 0;
    for (int i = (int)order.size() - 1; i >= 0; i--)
        if (comp[order[i]] == -1)
            dfs2(order[i], numSCC++);

    for (int i = 1; i <= n; i++) {
        if (comp[i] == comp[i + n]) {
            cout << "IMPOSSIBLE\n";
            return 0;
        }
    }

    for (int i = 1; i <= n; i++)
        cout << (comp[i] > comp[i + n]) << " \n"[i == n];
}

Translating Clauses to Implications

Different clause patterns produce different edges:

Clause Implication 1 Implication 2
(x OR y) NOT x -> y NOT y -> x
(x OR NOT y) NOT x -> NOT y y -> x
(NOT x OR y) x -> y NOT y -> NOT x
(NOT x OR NOT y) x -> NOT y y -> NOT x
(x) [force true] NOT x -> x (same edge)

💡 Key insight. "At most one of x, y is true" is the clause (NOT x OR NOT y). "Exactly one of x, y is true" requires two clauses: (x OR y) AND (NOT x OR NOT y).

CSES Giant Pizza

Problem: N people, M toppings. Each person specifies two preferences: "I want topping a" or "I don't want topping a." Each person must have at least one preference satisfied. Find a valid topping selection or report impossible.

Each person's two preferences form a 2-SAT clause. Preference "+" for topping i means literal i. Preference "-" for topping i means literal i + M (negation).

#include <bits/stdc++.h>
using namespace std;

const int MAXN = 2000005;
vector<int> adj[MAXN], radj[MAXN];
int comp[MAXN];
bool vis[MAXN];
vector<int> order;

void dfs1(int u) {
    vis[u] = true;
    for (int v : adj[u])
        if (!vis[v]) dfs1(v);
    order.push_back(u);
}

void dfs2(int u, int c) {
    comp[u] = c;
    for (int v : radj[u])
        if (comp[v] == -1) dfs2(v, c);
}

int m; // number of toppings (variables)

int neg(int x) { return x <= m ? x + m : x - m; }

void addClause(int a, int b) {
    int na = neg(a), nb = neg(b);
    adj[na].push_back(b);  radj[b].push_back(na);
    adj[nb].push_back(a);  radj[a].push_back(nb);
}

int main() {
    int n;
    cin >> n >> m;

    for (int i = 0; i < n; i++) {
        char s1, s2;
        int t1, t2;
        cin >> s1 >> t1 >> s2 >> t2;
        int a = (s1 == '+') ? t1 : t1 + m;
        int b = (s2 == '+') ? t2 : t2 + m;
        addClause(a, b);
    }

    int total = 2 * m;
    for (int i = 1; i <= total; i++)
        if (!vis[i]) dfs1(i);

    memset(comp, -1, sizeof(comp));
    int numSCC = 0;
    for (int i = (int)order.size() - 1; i >= 0; i--)
        if (comp[order[i]] == -1)
            dfs2(order[i], numSCC++);

    for (int i = 1; i <= m; i++) {
        if (comp[i] == comp[i + m]) {
            cout << "IMPOSSIBLE\n";
            return 0;
        }
    }

    for (int i = 1; i <= m; i++)
        cout << (comp[i] > comp[i + m] ? "+" : "-")
             << " \n"[i == m];
}

Trace: Small 2-SAT Instance

Variables: x1, x2. Clauses: (x1 OR x2), (NOT x1 OR x2), (x1 OR NOT x2).

Nodes: 1 = x1, 2 = x2, 3 = NOT x1, 4 = NOT x2.

Clause Edge 1 Edge 2
(x1 OR x2) 3 -> 2 4 -> 1
(NOT x1 OR x2) 1 -> 2 4 -> 3
(x1 OR NOT x2) 3 -> 4 2 -> 1

SCCs: {1, 2} (x1 and x2 imply each other), {3, 4} (NOT x1 and NOT x2 imply each other).

Check: comp[1] != comp[3], comp[2] != comp[4]. Satisfiable.

Assignment: x1 = true (comp[1] > comp[3]), x2 = true (comp[2] > comp[4]).

Verify: (T OR T) = T, (F OR T) = T, (T OR F) = T. All satisfied.

Problems

Problem Link Difficulty
CSES Giant Pizza cses.fi/problemset/task/1684 Medium
practice2_h — Two SAT atcoder.jp/contests/practice2/tasks/practice2_h Medium