Boolean satisfiability asks whether some assignment of true and false to a set of variables makes a formula true. In general it is the canonical NP-complete problem, and with three literals per clause it stays NP-complete. Restrict every clause to at most two literals and the problem collapses into something a graph algorithm solves in linear time. That restricted problem is 2-SAT, and it turns up whenever a system makes many binary choices under pairwise rules: which of two zones a replica goes in, or whether a feature flag is on.
This article builds 2-SAT from first principles: clauses as implications, why strongly connected components decide satisfiability, how to read an assignment off the component numbering, and how to encode real constraints, with a tested Python solver and a worked example.
From clauses to an implication graph
A formula in 2-CNF is an AND of clauses, each an OR of at most two literals, where a literal is a variable or its negation. For example (A or B) and (not A or C) and (not B or not C). A clause with one literal, (A), is allowed: it is the same as (A or A) and forces A true.
The key observation is that a clause (a or b) is logically identical to two implications: not a -> b and not b -> a. If a is false, b must be true; if b is false, a must be true. So a 2-CNF formula over n variables becomes a directed implication graph with 2n vertices, one per literal, and two edges per clause. A unit clause (a) becomes the single edge not a -> a, which says that assuming a is false leads straight to a contradiction.
The graph has a symmetry that the whole algorithm leans on. Every edge u -> v has a mirror not v -> not u, because both come from the same clause. Call this skew symmetry: negate every vertex and reverse every edge and you get the same graph back. Paths inherit it, so a path from u to v always comes with a path from not v to not u.
Why strongly connected components decide it
A path in the implication graph is a chain of forced consequences. Two literals in the same strongly connected component (SCC) imply each other, so they must take the same value.
Theorem. The formula is unsatisfiable if and only if some variable x has x and not x in the same SCC. One direction is direct: if x and not x imply each other, setting x either way forces the opposite, a contradiction. The other direction is the interesting one, and its proof is constructive: if no variable shares a component with its negation, the next section builds a satisfying assignment.
The result goes back to Krom (1967); the linear-time SCC algorithm is due to Aspvall, Plass and Tarjan (1979). The graph has 2n vertices and 2m edges, so one SCC pass is O(n + m).
Reading off a satisfying assignment
Contract each SCC to a single node and you get the condensation, a directed acyclic graph. Skew symmetry carries over: each component C has a mirror component not C. To build an assignment, walk the condensation in reverse topological order, sinks first, and set each unassigned component true and its mirror false.
Why this works: an implication u to v is violated only when u is true and v is false. A sink has no outgoing edges, so making it true cannot violate anything. Its mirror is a source with no incoming edges, so nothing requires it to be true and making it false is equally safe. Remove both and repeat; the remaining graph is still skew symmetric, so the argument holds all the way down.
In code you never perform that walk explicitly. Tarjan's algorithm finishes components in reverse topological order, so its component numbers already encode the order: a smaller number means closer to the sinks. The rule becomes one comparison per variable: x is true when comp[x] < comp[not x] under Tarjan numbering. Kosaraju's algorithm numbers components in topological order instead, so with Kosaraju the comparison flips to comp[x] > comp[not x]. Mixing the two conventions is the single most common 2-SAT bug, and it still returns an assignment, just a wrong one.
A tested implementation
Encode literal xi as 2*i and not xi as 2*i+1, so negation is l ^ 1. The solver below uses an iterative Tarjan so deep implication chains cannot hit Python's recursion limit, which a recursive version reaches at around a thousand nested calls by default.
def solve_2sat(n, clauses):
"""n variables 0..n-1; literal 2*i is x_i, 2*i+1 is NOT x_i.
clauses: list of (a, b) literal pairs meaning (a OR b).
Returns a list of bools, or None if unsatisfiable."""
N = 2 * n
adj = [[] for _ in range(N)]
for a, b in clauses:
adj[a ^ 1].append(b) # NOT a -> b
adj[b ^ 1].append(a) # NOT b -> a
# Iterative Tarjan: components are numbered in reverse topological order.
index, low = [-1] * N, [0] * N
comp, on_stack = [-1] * N, [False] * N
stack, counter, ncomp = [], 0, 0
for root in range(N):
if index[root] != -1:
continue
work = [(root, 0)]
index[root] = low[root] = counter; counter += 1
stack.append(root); on_stack[root] = True
while work:
v, i = work[-1]
if i < len(adj[v]):
work[-1] = (v, i + 1)
w = adj[v][i]
if index[w] == -1:
index[w] = low[w] = counter; counter += 1
stack.append(w); on_stack[w] = True
work.append((w, 0))
elif on_stack[w]:
low[v] = min(low[v], index[w])
continue
work.pop()
if work:
parent = work[-1][0]
low[parent] = min(low[parent], low[v])
if low[v] == index[v]: # v is the root of an SCC
while True:
w = stack.pop(); on_stack[w] = False
comp[w] = ncomp
if w == v:
break
ncomp += 1
assignment = []
for i in range(n):
if comp[2 * i] == comp[2 * i + 1]:
return None # x and NOT x imply each other
assignment.append(comp[2 * i] < comp[2 * i + 1])
return assignment
def lit(var, positive=True):
return 2 * var + (0 if positive else 1)Test it against brute force: for random formulas with up to six variables, enumerate all 2n assignments and check that the solver agrees on satisfiability and that every returned assignment satisfies every clause. The version above passed 3,000 such instances.
Worked example: placing four services in two zones
Four services, A to D, each run in one of two zones: true means east, false means west. The operations team states five rules. A and B must not both be west, for latency: (A or B). If A is east, C must be east, because they share a cache: (not A or C). B and C must not both be east, for blast radius: (not B or not C). At least one of C and D must be east: (C or D). A and D must not both be east, for capacity: (not A or not D).
The ten implication edges are: not A to B and not B to A; A to C and not C to not A; B to not C and C to not B; not C to D and not D to C; A to not D and D to not A. Run Tarjan and the graph splits into exactly two components, shown in the diagram above: {A, not B, C, not D}, which is numbered 0, and its mirror {not A, B, not C, D}, numbered 1. No variable shares a component with its negation, so the rules are satisfiable.
Read the assignment off with the Tarjan rule. comp[A] = 0 is less than comp[not A] = 1, so A is east. comp[B] = 1 is greater than comp[not B] = 0, so B is west. Likewise C is east and D is west. Check each rule: A or B holds through A; not A or C holds through C; not B or not C holds through not B; C or D holds through C; not A or not D holds through not D. Every rule is satisfied.
Because every literal inside a component is equivalent to the others, these rules allow exactly two layouts: the one above and its mirror image. Add a sixth rule, B must be east, the unit clause (B). It adds the single edge not B to B, which runs from the first component into the second. The components do not merge, but the second is now the sink, Tarjan finishes it first, and the solver returns the mirror layout: A west, B east, C west, D east.
Add a seventh rule, A must be east, and the edge not A to A runs back the other way. Now each component reaches the other, they merge into one, and A shares it with not A, so the solver returns None. The useful report for the operations team is the cycle itself: A to C (rule 2), C to not B (rule 3), not B to B (rule 6), B to not C (rule 3), not C to not A (rule 2), not A to A (rule 7). It names exactly the rules in conflict.
Encoding real constraints
Most real constraints are not written as clauses. These encodings stay within 2-CNF:
| Constraint | Clauses | Notes |
|---|---|---|
| x must be true | (x) | Unit clause; edge not x -> x |
| x implies y | (not x or y) | Exactly one clause |
| x equals y | (not x or y), (x or not y) | Puts x and y in one SCC |
| x differs from y (XOR) | (x or y), (not x or not y) | Two-colouring constraints |
| at most one of x, y | (not x or not y) | Pairwise conflict |
| at most one of k items | pairwise: k(k-1)/2 clauses; sequential: about 3k clauses with k-1 helper variables | Sequential encoding keeps every clause binary |
| exactly one of k items, k at least 3 | needs a k-literal clause | Not 2-SAT; use a SAT solver |
The sequential encoding adds helpers si, meaning some item up to i is chosen, with binary clauses xi implies si, si-1 implies si, and si-1 implies not xi.
The boundary is the at-least-one clause. As soon as a rule needs three or more literals in a single OR, such as choosing one of three zones, you have left 2-SAT. Map labelling with two candidate positions per label stays inside it; three-colouring does not, which is why it is NP-complete while two-colouring is easy.
Variants: what stays easy and what does not
Several neighbouring problems look like 2-SAT and are much harder. MAX-2-SAT, satisfying as many clauses as possible when not all can hold, is NP-hard. Counting satisfying assignments of a 2-CNF formula is #P-complete, so you cannot cheaply ask how many valid deployments exist. Weighted versions, such as minimising the number of true variables, are also NP-hard in general.
Some variants stay easy. Forced literals: a literal x is forced true exactly when there is a path from not x to x, so a reachability pass tells you which choices are fixed and which are free, which is useful for explaining a configuration to a user. Preferences, such as preferring x1 true, can be handled by adding each preference as a unit clause and keeping it only if the formula stays satisfiable, at one solve per preference.
Failure modes
| Failure | Symptom | Fix |
|---|---|---|
| Kosaraju numbering with the Tarjan comparison | Assignment returned that violates clauses | Pick one SCC algorithm; assert every clause after solving |
| Only one implication added per clause | Unsatisfiable formulas reported satisfiable | Always add both edges; skew symmetry is the invariant |
| Unit clause dropped or encoded as x -> x | Forced variables come out false | Encode (x) as not x -> x |
| Recursive DFS on long chains | RecursionError or stack overflow | Iterative Tarjan or Kosaraju |
| A three-literal rule forced into pairs | Over-constrained, false unsatisfiable | Recognise when the problem is not 2-SAT |
The cheapest safeguard is an O(m) check of the returned assignment against every clause after every solve.
Trade-offs and related reading
Use 2-SAT when every decision is binary and every rule touches at most two decisions: you get linear time, a conflict certificate, and code short enough to audit. When rules grow wider or you need optimisation, use a general SAT or MaxSAT solver; if you already depend on one, it handles 2-CNF well and the custom solver may not be worth maintaining.
For background on the pieces used here, see Tarjan's strongly connected components and Kosaraju's algorithm for the two SCC methods and their numbering conventions, topological sort for the ordering the assignment rule depends on, BFS and DFS for the traversal underneath, and graph colouring for the problem family where two colours are easy and three are not.
What to do next
- Implement the solver above and a brute-force checker; run both on a few thousand random formulas before trusting either.
- Add a post-solve assertion that checks every clause, and keep it in production code.
- Write your constraints as a table of rules first, then translate each with the encoding table; flag any rule that needs three or more literals.
- When the solver returns unsatisfiable, extract the path from x to not x and back, and report the clauses along it as the conflict.
- If you need to maximise satisfied rules, count solutions or support wider clauses, move to a SAT or MaxSAT solver instead of extending this one.