2-SAT
Reduce two-literal clauses to an implication graph, then solve satisfiability with SCC decomposition.
2-SAT
The main note is rendered from the TeX source. Code lives in a separate C++ file so the write-up stays readable.
Overview
2-SAT is the point where Boolean satisfiability stops feeling like brute force and starts feeling like graph theory. Once every clause has exactly two literals, the whole problem becomes an implication graph plus strongly connected components.
Problem-Driven Motivation
Many contest statements look like this after modeling:
each object has exactly two possible states,
some pairs of chosen states are incompatible,
some pair of states must contain at least one true choice.
The naive space is \(2^n\), which is hopeless once \(n\) reaches \(10^5\). But the constraints are not arbitrary SAT clauses. They are pairwise logical constraints, and that extra structure is enough to solve them in linear time.
Recognition Pattern
2-SAT is the right direction when:
every decision is binary,
constraints can be written as clauses \((a \lor b)\),
the problem contains implications like ``if this state is chosen, that state is forbidden / forced,''
the intended model is a large compatibility system rather than a numeric optimization.
Classic signals are:
choose one of two colors / directions / schedules,
at least one of two options must be taken,
two specific literal choices cannot both happen.
Derivation
The key equivalence is: \[ (a \lor b) \iff (\lnot a \Rightarrow b)\ \text{and}\ (\lnot b \Rightarrow a). \]
So instead of treating clauses directly, build a directed graph on literals:
one node for each variable being true,
one node for each variable being false.
Then every clause adds two implications.
Why do SCCs solve the problem?
If \(x\) and \(\lnot x\) lie in the same SCC, then each implies the other, so the formula forces \(x\) to be simultaneously true and false. That is impossible.
Otherwise, the SCC condensation graph is a DAG. Processing SCCs in reverse topological order lets us choose a literal before its negation whenever possible, producing a valid assignment.
Worked Problem
Problem.
Each worker must be assigned to one of two shifts: day or night. Some pairs of concrete choices are incompatible. For example:
if worker \(u\) takes day, worker \(v\) cannot take night,
at least one of worker \(a\) taking day or worker \(b\) taking day must happen.
Why naive fails.
Trying all shift assignments is \(2^n\).
Modeling.
Let variable \(x_i\) mean ``worker \(i\) takes day.'' Then:
``worker \(u\) day and worker \(v\) night cannot both happen'' becomes \[ (\lnot(x_u \land \lnot x_v)) \iff (\lnot x_u \lor x_v), \]
``at least one of \(x_a\) or \(x_b\)'' is already a 2-SAT clause: \[ (x_a \lor x_b). \]
Graph construction.
Every clause \((p \lor q)\) contributes: \[ \lnot p \Rightarrow q,\qquad \lnot q \Rightarrow p. \]
Final algorithm.
build the implication graph,
compute SCCs,
reject if any variable and its negation share an SCC,
otherwise assign values by SCC order.
Implementation Reasoning
The only implementation detail that really matters is a clean literal encoding.
The code uses:
node \(2x\) for ``variable \(x\) is true,''
node \(2x+1\) for ``variable \(x\) is false,''
negation by \(\texttt{literal} \oplus 1\).
That makes the clause and implication helpers short and hard to misuse.
The solver exposes:
add_or,add_implication,force_true,satisfiable().
Correctness Intuition
The implication graph captures the exact situations where one false literal forces another literal to become true. SCCs detect contradictions because mutual reachability means mutual forcing. Once contradictions are gone, assigning literals in reverse SCC topological order guarantees that choosing a literal never violates an implication to an already-fixed literal.
Complexity Analysis
For \(n\) variables and \(m\) clauses:
vertices: \(2n\),
edges: \(2m\) plus any extra forced implications,
total time: \(O(n+m)\),
memory: \(O(n+m)\).
Common Pitfalls
Mixing variable indices with literal indices.
Extracting the assignment from DFS order instead of SCC order.
Forgetting that ``not both'' is a clause, not a direct edge, until translated correctly.
Trying to force constraints that are not reducible to 2-literal clauses.
Variants and Failure Modes
``At most one'' over many choices needs extra encoding; it is not one 2-SAT clause by itself.
General SAT does not collapse to SCCs.
Sometimes a graph-coloring or bipartite formulation is simpler than 2-SAT, even if 2-SAT is possible.
Practice Problems
Binary scheduling with pairwise incompatibilities.
Orientation or color choices with logical constraints.
Giant Pizza and similar implication-graph problems.
References
Code
Contest-ready reference implementation for the idea explained above.
#include <bits/stdc++.h>
using namespace std;
struct TwoSat {
int n;
vector<vector<int>> graph;
vector<vector<int>> reverse_graph;
vector<int> comp;
vector<int> order;
vector<int> assignment;
explicit TwoSat(int n)
: n(n),
graph(2 * n),
reverse_graph(2 * n),
comp(2 * n, -1),
assignment(n, 0) {}
int literal(int variable, bool is_true) const {
return 2 * variable + (is_true ? 0 : 1);
}
int neg(int lit) const {
return lit ^ 1;
}
void add_implication(int from, int to) {
graph[from].push_back(to);
reverse_graph[to].push_back(from);
}
void add_or(int x, bool x_true, int y, bool y_true) {
int a = literal(x, x_true);
int b = literal(y, y_true);
add_implication(neg(a), b);
add_implication(neg(b), a);
}
void force_true(int x, bool value) {
int lit = literal(x, value);
add_implication(neg(lit), lit);
}
void dfs1(int v, vector<int>& seen) {
seen[v] = 1;
for (int to : graph[v]) {
if (!seen[to]) dfs1(to, seen);
}
order.push_back(v);
}
void dfs2(int v, int id) {
comp[v] = id;
for (int to : reverse_graph[v]) {
if (comp[to] == -1) dfs2(to, id);
}
}
bool satisfiable() {
vector<int> seen(2 * n, 0);
fill(comp.begin(), comp.end(), -1);
order.clear();
for (int v = 0; v < 2 * n; ++v) {
if (!seen[v]) dfs1(v, seen);
}
reverse(order.begin(), order.end());
int id = 0;
for (int v : order) {
if (comp[v] == -1) dfs2(v, id++);
}
for (int x = 0; x < n; ++x) {
int t = literal(x, true);
int f = literal(x, false);
if (comp[t] == comp[f]) return false;
assignment[x] = comp[t] > comp[f];
}
return true;
}
};
// Example application:
// each clause is (x is x_true) OR (y is y_true).
vector<int> solve_clause_system(
int variables,
const vector<tuple<int, bool, int, bool>>& clauses,
const vector<pair<int, bool>>& forced_literals = {}
) {
TwoSat solver(variables);
for (const auto& clause : clauses) {
int x = get<0>(clause);
bool x_true = get<1>(clause);
int y = get<2>(clause);
bool y_true = get<3>(clause);
solver.add_or(x, x_true, y, y_true);
}
for (const auto& literal : forced_literals) {
solver.force_true(literal.first, literal.second);
}
if (!solver.satisfiable()) return {};
return solver.assignment;
}
Source Files and Assets
Raw files are still available here when you want the original TeX, C++, or statement assets.