2-SAT and Implication Graphs

2-SAT asks whether Boolean variables can satisfy a conjunction of clauses, each containing at most two literals. A literal is x or its negation ¬x. Constraints such as “choose A or B,” “not both,” or “if A then B” become two-literal clauses. General SAT is much harder, but 2-SAT reduces to strongly connected components in a directed implication graph and runs in linear time.

Prerequisites: Depth-first search; Strongly Connected Components. Difficulty: Advanced. Review: Strongly connected components.

Build the idea

1. 1. Translate clauses, not intuition

   The clause (a∨b) is equivalent to both implications ¬a→b and ¬b→a: if either literal is false, the other must be true. For “not both x and y,” use (¬x∨¬y). For x→y, use (¬x∨y). A forced literal a is represented by (a∨a). These formulas are logical equivalences, so satisfying the graph’s implications satisfies all input clauses.

2. 2. Encode complementary vertices

   Variable i uses vertex 2(i−1) for positive xᵢ and the next vertex for ¬xᵢ. XOR 1 flips the truth literal. Graph vertices here are 0-based because paired encodings become simpler; user-facing variable labels remain 1..n. The signed input literal −3 means ¬x₃, not a negative vertex ID. Store the transpose alongside the graph for Kosaraju’s second pass.

3. 3. Find contradictions with SCCs

   If x and ¬x are mutually reachable, choosing either truth value forces its opposite, so no assignment exists. Conversely, if no variable shares an SCC with its complement, the SCC condensation is acyclic and choices can be made consistently in topological order. DFS first records FINISHING order. Traverse the transpose in reverse finishing order to label SCCs. This lesson uses Kosaraju; the later Tarjan lesson offers a one-pass alternative.

4. 4. Recover truth values with the right convention

   For this exact two-pass ordering, component IDs increase from earlier to later SCCs in the original condensation DAG. Set xᵢ true when component[xᵢ] > component[¬xᵢ]. Informally, process SCCs from later to earlier: if a component and its complement are still unassigned, make that component true and its complement false. Outgoing implications have already been settled compatibly. Reversing the SCC numbering convention would require reversing this comparison; arbitrary SCC labels are insufficient.

5. 5. Work the example

   Clauses (x₁∨x₂), (¬x₁∨x₂), (x₁∨¬x₂) force both variables true. The second clause rules out x₁=true,x₂=false; the third rules out x₁=false,x₂=true; the first rules out both false. Output is YES and 1 1. To create a contradiction on x₁, add both unit clauses (x₁∨x₁) and (¬x₁∨¬x₁); their implication edges put the complementary literals in one SCC.

This is a complete program. Compile with C++17 and enter the input described below.

#include<iostream>
#include<vector>
#include<functional>
#include<cstdlib>
using namespace std;
int main(){
    int n,m;
    if(!(cin>>n>>m)){
        return 0;
    }
    int N=2*n;
    vector<vector<int>>graph(N),reverseGraph(N);
    auto literal=[](int x){
        return 2*(abs(x)-1)+(x<0);
    };
    auto edge=[&](int u,int v){
        graph[u].push_back(v);
        reverseGraph[v].push_back(u);
    };
    for(int i=0;i<m;++i){
        int a,b;
        cin>>a>>b;
        int u=literal(a),v=literal(b);
        edge(u^1,v);
        edge(v^1,u); // (a OR b).
    }
    vector<char>seen(N,false);
    vector<int>order,component(N,-1);
    function<void(int)>dfs1=[&](int v){
        seen[v]=true;
        for(int u:graph[v]){
            if(!seen[u]){
                dfs1(u);
            }
        }
        order.push_back(v); // Finishing order, not discovery order.
    };
    for(int v=0;v<N;++v){
        if(!seen[v]){
            dfs1(v);
        }
    }
    function<void(int,int)>dfs2=[&](int v,int id){
        component[v]=id;
        for(int u:reverseGraph[v]){
            if(component[u]==-1){
                dfs2(u,id);
            }
        }
    };
    int id=0;
    for(int i=N-1;i>=0;--i){
        if(component[order[i]]==-1){
            dfs2(order[i],id++);
        }
    }
    for(int i=0;i<n;++i){
        if(component[2*i]==component[2*i+1]){
            cout<<"NO\n";
            return 0;
        }
    }
    cout<<"YES\n";
    for(int i=0;i<n;++i){
        cout<<(component[2*i]>component[2*i+1])<<(i+1==n?'\n':' ');
    }
}

Complexity analysis

There are 2n graph vertices and 2m implication edges. Building both directions, two DFS passes, contradiction checks and assignment take O(n+m) time and O(n+m) memory. Recursion depth can reach 2n. The program is suitable for moderate recursion depths (for example n≤2000); replace DFS recursion with explicit frames for very large instances.

Example input and output

Read n m (n≥1), followed by m pairs a b encoding clauses (a OR b). A positive i means xᵢ; negative −i means NOT xᵢ; 1≤|a|,|b|≤n. Print NO if unsatisfiable, otherwise YES and n Boolean values (0=false, 1=true).

Input

2 3
1 2
-1 2
1 -2

Output

YES
1 1

Each of the other three truth assignments violates one listed clause, so both variables must be true.

Practical applications

Use for binary choices with pairwise forbidden combinations, scheduling alternatives, orientation constraints and geometric nonintersection choices. Write a truth table for each constraint before adding edges. More-than-two-literal clauses generally leave the 2-SAT setting. SCC membership detects contradictions; topological SCC order recovers a witness assignment.

Check your understanding

What makes a 2-SAT instance impossible?

Put it into practice

Encode “exactly one of x and y is true” using two clauses and enumerate all assignments.