Engineering Blueprint: Literal Encoding & Constraint Gadgets
Given $N$ boolean variables $x_0, x_1, \dots, x_{N-1}$, we allocate $2N$ vertices in the implication graph. For each variable $i \in [0, N-1]$:
- Vertex $2i$ represents the positive literal $x_i$ (
isTrue = true). - Vertex $2i + 1$ represents the negated literal $\neg x_i$ (
isTrue = false). - Negating any literal vertex $u \in [0, 2N-1]$ is a single branchless bitwise XOR: $\neg u = u \oplus 1$.
Every binary boolean constraint over literals $a, b$ reduces to one or more base clauses $(p \lor q)$, each adding two directed edges $(\neg p \to q)$ and $(\neg q \to p)$:
- At least one true ($a \lor b$):
addClause(a, b)$\implies (\neg a \to b), (\neg b \to a)$. - Implication ($a \Rightarrow b$): Equivalent to $(\neg a \lor b) \implies$
addClause(a ^ 1, b). - Mutual Exclusion / At most one true ($\neg(a \land b)$): Equivalent to $(\neg a \lor \neg b) \implies$
addClause(a ^ 1, b ^ 1). - XOR / Exactly one true ($a \oplus b$): Combine $(a \lor b) \land (\neg a \lor \neg b)$.
- Equality ($a \iff b$): Combine $(\neg a \lor b) \land (a \lor \neg b)$.
- Force $a$ to be True (Unit Clause): Equivalent to $(a \lor a) \implies$ single edge $(\neg a \to a)$.
Step through 0-1 BFS deque relaxation (push_front for w=0, push_back for w=1), Tarjan’s undirected bridge/articulation criterion (low[v] > tin[u] / low[v] ≥ tin[u]), and Tarjan’s single-pass SCC condensation.
Invariant & State
Suppose a constraint requires at most one of $K$ literals $\{l_0, l_1, \dots, l_{K-1}\}$ to be true. Naive pairwise mutex adds $\binom{K}{2} = O(K^2)$ edges! Instead, introduce $K$ auxiliary prefix variables $p_0, \dots, p_{K-1}$ where $p_j$ means "$\bigvee_{r=0}^j l_r$ is true", adding implications $l_j \Rightarrow p_j$, $p_{j-1} \Rightarrow p_j$, and $p_{j-1} \Rightarrow \neg l_j$. This reduces the edge count from $O(K^2)$ to strictly $3K = O(K)$ linear edges!
Complexity Matrix
| Operation / Feature | Naive / Backtracking | Tarjan 2-SAT Engine | Memory Footprint |
|---|---|---|---|
| Solve $N$ Vars, $M$ Clauses | O(2^N) worst-case | O(N + M) | O(N + M) |
| At-Most-One of $K$ Literals | O(K²) pairwise clauses | O(K) with prefix vars | O(K) auxiliary literals |
| Condensation DAG Construction | O(V²) dense matrix | O(V + E) deduplicated | O(V + E) |
Complete Implementation: Linear-Time 2-SAT Solver & Condensation DAG Builder
#include <vector>
#include <algorithm>
#include <cstdint>
class TwoSatSolver {
public:
explicit TwoSatSolver(int numVars)
: n(numVars), adj(2 * numVars), tin(2 * numVars, 0),
low(2 * numVars, 0), comp(2 * numVars, -1),
onStack(2 * numVars, 0), assignment(numVars, false) {
st.reserve(2 * numVars);
}
static int lit(int var, bool isTrue) noexcept {
return 2 * var + (isTrue ? 0 : 1);
}
// Adds (u OR v) where u, v are literal indices in [0, 2n-1]
void addClause(int u, int v) {
adj[u ^ 1].push_back(v);
adj[v ^ 1].push_back(u);
}
void addXor(int u, int v) {
addClause(u, v);
addClause(u ^ 1, v ^ 1);
}
void addEq(int u, int v) {
addClause(u ^ 1, v);
addClause(u, v ^ 1);
}
bool solve() {
for (int i = 0; i < 2 * n; ++i) {
if (tin[i] == 0) dfs(i);
}
for (int i = 0; i < n; ++i) {
if (comp[2 * i] == comp[2 * i + 1]) return false;
// In Tarjan's SCC, smaller component ID means closer to a sink in the DAG
assignment[i] = (comp[2 * i] < comp[2 * i + 1]);
}
return true;
}
const std::vector<bool>& values() const noexcept { return assignment; }
private:
int n, timer = 0, sccCount = 0;
std::vector<std::vector<int>> adj;
std::vector<int> tin, low, comp, st;
std::vector<uint8_t> onStack;
std::vector<bool> assignment;
void dfs(int u) {
tin[u] = low[u] = ++timer;
st.push_back(u);
onStack[u] = 1;
for (int v : adj[u]) {
if (tin[v] == 0) {
dfs(v);
low[u] = std::min(low[u], low[v]);
} else if (onStack[v]) {
low[u] = std::min(low[u], tin[v]);
}
}
if (low[u] == tin[u]) {
while (true) {
int w = st.back();
st.pop_back();
onStack[w] = 0;
comp[w] = sccCount;
if (w == u) break;
}
++sccCount;
}
}
};< vs > Between Tarjan and KosarajuIn Tarjan's algorithm, SCCs are popped in post-order (sinks get ID $0$, sources get ID $K-1$), so the sink-most literal satisfies $\text{comp}[2i] < \text{comp}[2i+1]$. In Kosaraju's algorithm, the second pass discovers sources first (sources get ID $0$, sinks get ID $K-1$), so the inequality reverses to $\text{comp}[2i] > \text{comp}[2i+1]$. Mixing the two conventions sets every implied variable to False instead of True!