Case Study: Building a Two-Coloring Conflict Resolver

DataField.Dev

Case Study: Building a Two-Coloring Conflict Resolver

"A solution exists" and "here is the solution" are different promises. Engineering lives in the gap.

Executive Summary

You will build a small but real tool: a conflict resolver that decides whether a set of items can be split into two groups so that no pair of "conflicting" items lands in the same group — and, when it can, produces the split. Think of partitioning database transactions into two batches so that no two conflicting transactions run together, or assigning on-call engineers to two rotations so that no two people who must not share a shift do. The decision is the classic 2-coloring problem.

This is a build case study, the complement of the analysis-heavy compression study. There, we proved something impossible; here, we construct a working algorithm and then prove three things about it, each illustrating a different §5.3–§5.5 strategy:

an existence-or-counterexample result (a valid 2-coloring exists iff the resolver returns one),
a uniqueness result (when the conflict graph is connected, the 2-coloring is essentially the only one — proved with the §5.4 "assume two, force them equal" move),
an impossibility result for the failing case (an odd conflict cycle cannot be 2-colored — proved by contradiction, §5.1).

By the end you will have running code, three proofs matched to the code, and a feel for how the chapter's strategies divide the labor of a real design.

Skills applied

Building a constraint solver incrementally and stating a precise correctness claim for it.
A proof by cases on the parity of a cycle's length (§5.3) — the heart of why 2-coloring succeeds or fails.
An existence + uniqueness argument (§5.4): construct a coloring, then prove it is forced.
A proof by contradiction (§5.1) that odd cycles are not 2-colorable.
Using a counterexample search (§5.5, the Toolkit's find_counterexample) to distinguish "looks 2-colorable" from "is 2-colorable."

Background

The scenario

You are handed a list of items and a list of conflict pairs — unordered pairs $\{u, v\}$ meaning "$u$ and $v$ must be in different groups." You must either output a valid assignment of each item to group 0 or group 1 with every conflict pair split across the two groups, or report that no such assignment exists.

Model this as a graph (we will lean on the everyday picture; the formal apparatus arrives in Part V). Items are vertices; each conflict pair is an edge between two vertices. A valid assignment is a function $c \colon V \to \{0, 1\}$ such that for every edge $\{u, v\}$ we have $c(u) \ne c(v)$. Such a $c$ is a proper 2-coloring, and a graph that has one is bipartite.

💡 Intuition: Picture the conflict graph and try to paint it with two colors so that no edge joins two same-colored vertices. Start anywhere, color it 0, color all its conflict-neighbors 1, their neighbors 0, and so on — the colors are forced as you walk outward. Either the forcing completes consistently (success) or it tries to paint some vertex both colors at once (failure). The algorithm is just that walk; the proofs explain exactly when the forcing can fail.

Why this matters

Two-coloring is the simplest constraint-satisfaction problem with a clean yes/no boundary, and it shows up constantly: register allocation with two registers, splitting a circuit across two chips, scheduling into two non-overlapping slots, detecting whether a "friend/enemy" network can be cleanly polarized. More importantly for this chapter, it is a setting where all three questions a designer asks — does a solution exist? is it unique? when is it impossible? — have crisp, provable answers. We will get each one.

Phase 1: Build the resolver

We build the forcing walk as a breadth-first assignment. Color the start vertex 0; whenever we reach a vertex with an assigned color, every neighbor must get the opposite color. If we ever try to assign a vertex a color different from one it already has, the graph is not 2-colorable.

from collections import deque

def two_color(graph, start):
    """graph: dict vertex -> set of neighbors (an undirected conflict graph).
    Returns a dict vertex -> {0,1} coloring of start's component, or None if
    that component has no proper 2-coloring."""
    color = {start: 0}
    queue = deque([start])
    while queue:
        u = queue.popleft()
        for v in graph[u]:
            if v not in color:
                color[v] = 1 - color[u]      # forced: opposite of u
                queue.append(v)
            elif color[v] == color[u]:       # conflict: same color on an edge
                return None
    return color

g = {0: {1, 3}, 1: {0, 2}, 2: {1, 3}, 3: {0, 2}}   # a 4-cycle 0-1-2-3-0
print(two_color(g, 0))
# Expected output:
# {0: 0, 1: 1, 2: 0, 3: 1}

Hand-trace the 4-cycle 0-1-2-3-0. Start color={0:0}. Pop 0: neighbors 1, 3 get 1. Pop 1: neighbor 0 already 0 (opposite of 1, fine), neighbor 2 gets 0. Pop 3: neighbor 0 fine, neighbor 2 already 0 — and color[2]==0 != color[3]==1, fine. Pop 2: both neighbors already colored and opposite. Queue empties; return {0:0, 1:1, 2:0, 3:1}. The even cycle colors cleanly.

🔄 Check Your Understanding In the line color[v] = 1 - color[u], why is the new color forced rather than chosen? What earlier §5.4 idea does "forced" foreshadow?

Answer

The edge $\{u, v\}$ demands $c(u) \ne c(v)$, and there are only two colors, so once $c(u)$ is fixed, $c(v)$ has exactly one legal value: $1 - c(u)$. There is no freedom. This forcing is the seed of the uniqueness argument in Phase 3 — when every color is forced, at most one coloring can exist (up to swapping the two color names).

Phase 2: Existence — the resolver succeeds exactly when a coloring exists

The first correctness obligation is an existence claim with a counterexample flavor: the resolver finds a coloring precisely when one is possible.

The strategy first. This is an "if and only if," so two directions. ($\Rightarrow$) If two_color returns a coloring, that object is a witness that a proper 2-coloring exists — a constructive existence proof, in the §5.4 sense. ($\Leftarrow$) If a proper 2-coloring exists, we must argue the forcing walk cannot wrongly report None. We show the contrapositive: if the walk returns None, no coloring exists — because the walk only returns None when two endpoints of an edge are forced to the same color, and forced means unavoidable.

Claim (existence). two_color(graph, start) returns a proper 2-coloring of start's component if and only if that component has one.

Proof. ($\Rightarrow$) Suppose the function returns a dictionary color. It only returns a (non-None) dictionary after the queue empties without ever hitting the color[v] == color[u] branch. Every edge inside the component was examined (BFS visits every vertex of the component and scans its neighbors), and none triggered the conflict branch, so every edge $\{u, v\}$ satisfies color[u] != color[v]. Thus color is a proper 2-coloring — an explicit witness that one exists. (Constructive existence.)

($\Leftarrow$) We prove the contrapositive: if the function returns None, the component has no proper 2-coloring. The function returns None only when it finds an edge $\{u, v\}$ with color[v] == color[u] where both colors were forced. Trace why each was forced: every assigned color other than the start's is determined by color[w] = 1 - color[parent] along the BFS tree, and the start is 0. So the colors of u and v are not free choices — they are dictated by the path from start. If two forced-opposite chains meet at an edge with equal colors, then any proper coloring, which must also respect those same forcing constraints, would face the identical clash. Hence no proper coloring exists. (We make the "forced along a path" idea fully rigorous in Phase 4 via parity.) $\blacksquare$

🔗 Connection. Part ($\Rightarrow$) is exactly a constructive existence proof: we did not argue abstractly that a coloring is out there — we produced one and checked it. Contrast the non-constructive existence proof in §5.4 ($a^b$ rational), which guarantees a witness without naming it. A programmer almost always wants the constructive kind, because you can return color.

Phase 3: Uniqueness — connected conflict graphs force the coloring

Now a uniqueness question a scheduler cares about: if the resolver succeeds, is the grouping the only one? Not literally — you can always swap the names of the two groups. But that is the only freedom.

The strategy first. Uniqueness, §5.4 style: assume two proper 2-colorings $c$ and $c'$ of a connected graph and force them to agree (up to swapping the color names). The lever is the forcing from Phase 1: once you fix the color of a single vertex, connectivity propagates that choice to every other vertex with no freedom left.

Claim (uniqueness up to swap). If the conflict graph is connected and has a proper 2-coloring, then it has exactly two proper 2-colorings, and they differ only by swapping 0 and 1.

Proof (existence + uniqueness). Existence: by Phase 2, a proper 2-coloring $c$ exists (the resolver builds one). Uniqueness: let $c$ and $c'$ be any two proper 2-colorings. Consider the start vertex $s$. Either $c'(s) = c(s)$ or $c'(s) \ne c(s)$ — two exhaustive cases.

Case 1: $c'(s) = c(s)$. We show $c' = c$ everywhere. Take any vertex $w$. Because the graph is connected, there is a path $s = v_0, v_1, \dots, v_m = w$. Along each edge $\{v_i, v_{i+1}\}$, both colorings are proper, so each flips: $c(v_{i+1}) = 1 - c(v_i)$ and $c'(v_{i+1}) = 1 - c'(v_i)$. Since $c'(v_0) = c(v_0)$, an easy induction on $i$ (Chapter 6) gives $c'(v_i) = c(v_i)$ for all $i$, so $c'(w) = c(w)$. As $w$ was arbitrary, $c' = c$.

Case 2: $c'(s) \ne c(s)$. Apply Case 1 to $c$ and the swapped coloring $\overline{c'}$ defined by $\overline{c'}(v) = 1 - c'(v)$ (still proper, since swapping both endpoints of every edge preserves "different"). Now $\overline{c'}(s) = 1 - c'(s) = c(s)$, so Case 1 yields $\overline{c'} = c$, i.e. $c'$ is exactly $c$ with the two colors swapped.

So every proper 2-coloring is either $c$ or its swap — exactly two, differing only by the name swap. $\blacksquare$

⚠️ Common Pitfall: The uniqueness claim needs connectivity. Drop it and the claim is false: a graph with two separate components can color each independently, giving $2 \times 2 = 4$ colorings, not 2. This is the §5.4 lesson that you must match the proof's hypotheses to the exact claim — and a reminder that a uniqueness statement quietly assuming the wrong precondition "proves" something false.

🔄 Check Your Understanding The proof split on whether $c'(s) = c(s)$. Why are those two cases exhaustive, and where did the proof use the §5.3 obligation that cases must cover everything?

Answer

$c'(s)$ is a color, hence either equal to $c(s)$ or not — there is no third possibility, so the two cases are exhaustive (the §5.3 completeness obligation). Case 1 handles agreement; Case 2 reduces to Case 1 by swapping. Every proper $c'$ falls into one case, so the conclusion covers all of them.

Phase 4: Impossibility — odd cycles cannot be 2-colored (by contradiction)

The resolver returns None on some graphs. Which ones, and can we prove the None is deserved? The cleanest culprit is an odd cycle — a loop through an odd number of vertices, like a 3-cycle (triangle) or 5-cycle.

The strategy first. "An odd cycle has no proper 2-coloring" is an impossibility claim — an absence — so we reach for contradiction (§5.1, §5.6). Assume a proper 2-coloring of an odd cycle exists, walk around the loop watching the color flip on every edge, and discover the start vertex is forced to disagree with itself. The flip-counting is a proof by cases on parity (§5.3) wearing a contradiction's clothes.

Theorem. A cycle $v_0, v_1, \dots, v_{n-1}, v_0$ of odd length $n$ has no proper 2-coloring.

Proof (by contradiction). Suppose, for contradiction, that $c$ is a proper 2-coloring of the odd cycle. Walk around it. Each edge $\{v_i, v_{i+1}\}$ forces a color flip, so $$c(v_i) = c(v_0) \oplus (i \bmod 2)$$ — that is, $c(v_i)$ equals $c(v_0)$ when $i$ is even and the opposite when $i$ is odd. (This is a tiny induction: each step toggles the color, so after $i$ steps the color has toggled $i$ times, and toggling $i$ times returns to the start iff $i$ is even — a case split on the parity of $i$.)

Now close the loop. The last edge is $\{v_{n-1}, v_0\}$, which also demands a flip: $c(v_{n-1}) \ne c(v_0)$. But by the formula, $c(v_{n-1}) = c(v_0) \oplus ((n-1) \bmod 2)$. Since $n$ is odd, $n - 1$ is even, so $(n-1) \bmod 2 = 0$ and therefore $c(v_{n-1}) = c(v_0)$. The closing edge thus requires $c(v_{n-1}) \ne c(v_0)$ while the walk forces $c(v_{n-1}) = c(v_0)$ — a contradiction. Hence no proper 2-coloring exists. $\blacksquare$

💡 Intuition: Going around a cycle, the color flips once per edge. To come home consistent, you need an even number of flips — flip-flip-...-flip an even number of times and you're back where you started. An odd cycle has an odd number of edges, so you arrive home flipped, clashing with the start. Even cycles (like the 4-cycle in Phase 1) have an even number of edges and close perfectly. The whole theorem is "even vs. odd," which is why it is a parity case split at heart.

Let us confirm the boundary on small cycles — triangle (odd, must fail) versus square (even, must succeed).

def cycle_graph(n):
    """Undirected cycle on vertices 0..n-1."""
    return {i: {(i - 1) % n, (i + 1) % n} for i in range(n)}

for n in [3, 4, 5, 6]:
    result = two_color(cycle_graph(n), 0)
    print(f"{n}-cycle ({'odd' if n % 2 else 'even'}): "
          f"{'2-colorable' if result else 'NOT 2-colorable'}")
# Expected output:
# 3-cycle (odd): NOT 2-colorable
# 4-cycle (even): 2-colorable
# 5-cycle (odd): NOT 2-colorable
# 6-cycle (even): 2-colorable

The odd cycles return None; the even cycles color. The code agrees with the theorem on four cases — encouraging, but (theme two) it is the proof that guarantees every odd cycle fails, not these four checks.

🐛 Find the Error. A teammate "proves" the converse too hastily: "Since odd cycles aren't 2-colorable, only graphs without any cycle at all are 2-colorable." Find the flaw with a single counterexample from this case study.

Answer

False. The 4-cycle of Phase 1 contains a cycle yet is perfectly 2-colorable ({0:0,1:1,2:0,3:1}). The correct theorem (König's, formalized later) is that a graph is 2-colorable iff it has no odd cycle — even cycles are fine. The teammate over-generalized "odd cycle bad" to "any cycle bad," exactly the §5.5 hazard of extrapolating from one case to a universal claim.

Phase 5: Triage with a counterexample search

Finally, wire in the chapter's Toolkit to triage a conjecture before proving it — theme four in action. Suppose someone conjectures "every graph on $\le 4$ vertices is 2-colorable." Use find_counterexample over a small family of graphs to refute it instantly with the triangle.

from dmtoolkit.logic import find_counterexample

def is_two_colorable(graph):
    # 2-colorable iff every component colors; here graphs are connected.
    start = next(iter(graph))
    return two_color(graph, start) is not None

family = [cycle_graph(3), cycle_graph(4)]    # triangle, square
bad = find_counterexample(is_two_colorable, family)
print("counterexample graph (vertices):", None if bad is None else sorted(bad))
# Expected output:
# counterexample graph (vertices): [0, 1, 2]

The search returns the triangle (vertices [0, 1, 2]) — a complete disproof of "every small graph is 2-colorable" in one call, exactly as §5.5 promises. Point the same search at a family of even cycles and it returns None: no counterexample in that family, which is encouragement to prove the even-cycle theorem, not a proof of it.

Phase 6: Return the proof, not just the verdict

A resolver that says only None is unsatisfying in production: a teammate will ask why. The §5.4 lesson is that a constructive result — handing back the actual object — beats a bare existence (or non-existence) verdict. So let us upgrade the resolver to return, on failure, the odd cycle that makes 2-coloring impossible. That cycle is a self-contained, checkable proof that no coloring exists — the constructive partner of the Phase 4 contradiction.

The strategy first. Track a BFS parent and depth for every vertex. When the conflict branch fires on an edge $\{u, v\}$, both endpoints sit at the same color, hence (since color = depth parity) the same depth parity. Walk $u$ and $v$ back up the BFS tree to their meeting point; the loop "down to $u$, across the conflict edge to $v$, up to the meeting point" closes a cycle. Its length is even-plus-one — odd — so by Phase 4 it cannot be 2-colored. We construct the witness rather than merely asserting one exists.

from collections import deque

def find_odd_cycle(graph, start):
    """Return an odd cycle (list of vertices) in start's component, or None."""
    color, parent, depth = {start: 0}, {start: None}, {start: 0}
    queue = deque([start])
    while queue:
        u = queue.popleft()
        for v in graph[u]:
            if v not in color:
                color[v], parent[v], depth[v] = 1 - color[u], u, depth[u] + 1
                queue.append(v)
            elif color[v] == color[u]:           # conflict edge u--v
                pu, pv = [u], [v]                # climb to equal depth
                while depth[pu[-1]] > depth[pv[-1]]: pu.append(parent[pu[-1]])
                while depth[pv[-1]] > depth[pu[-1]]: pv.append(parent[pv[-1]])
                while pu[-1] != pv[-1]:          # climb together to meeting point
                    pu.append(parent[pu[-1]]); pv.append(parent[pv[-1]])
                return pu + pv[-2::-1]           # u..meet + meet..v (no repeat)
    return None

print(find_odd_cycle({0: {1, 2}, 1: {0, 2}, 2: {0, 1}}, 0))   # triangle
# Expected output:
# [1, 0, 2]

Hand-trace the triangle {0:{1,2}, 1:{0,2}, 2:{0,1}}. BFS from 0: color 0→0, depth 0. Pop 0: color 1 and 2 both 1, parent 0, depth 1. Pop 1: neighbor 0 is colored opposite (fine); neighbor 2 is colored 1, equal to color[1]==1 — conflict on edge 1--2. Both 1 and 2 are at depth 1 (equal), so we skip the depth-matching loops. They differ, so climb together: parent[1]=0, parent[2]=0 — both reach 0, the meeting point. Now pu=[1,0], pv=[2,0], and we return pu + pv[-2::-1] = [1,0] + [2] = [1, 0, 2]. That is the cycle $1 \to 0 \to 2 \to 1$ of length 3, odd — a constructive certificate that the triangle has no 2-coloring.

🔗 Connection. Phase 4 proved odd cycles aren't 2-colorable by contradiction (a non-constructive style — "assume a coloring, derive absurdity"). Phase 6 exhibits the odd cycle — the constructive style of §5.4. Both establish "no coloring exists," but the constructive version hands the caller something to inspect and verify, which is almost always what a real system wants. This is the §5.4 constructive-vs-non-constructive contrast, now playing out inside one tool.

🔄 Check Your Understanding Why is the returned cycle guaranteed to have odd length, given that the conflict fired on $\{u, v\}$ with color[u] == color[v]?

Answer

Equal color means equal depth parity (color is depth mod 2). If the climbs meet at depth $d$, the cycle has $(\text{depth}(u) - d)$ edges up from $u$, $(\text{depth}(v) - d)$ edges up from $v$, plus the one conflict edge $\{u, v\}$ — a total of $(\text{depth}(u) - d) + (\text{depth}(v) - d) + 1$ edges. Since $\text{depth}(u) \equiv \text{depth}(v) \pmod 2$, the sum $\text{depth}(u) + \text{depth}(v) - 2d$ is **even**, so adding $1$ makes the cycle length odd.

Discussion Questions

Phase 2's ($\Leftarrow$) direction was proved by contraposition (Chapter 4), while Phase 4 was proved by contradiction (§5.1). Both involve "assume the bad thing." Explain the precise difference between the two techniques as used here, and why each fit its claim's shape.
The uniqueness proof (Phase 3) required connectivity. State exactly how many proper 2-colorings a graph with $k$ connected components (each 2-colorable) has, and prove your count.
The odd-cycle proof used a parity case split disguised inside a contradiction. Rewrite the core step as an explicit proof by cases on whether $n$ is even or odd, with no contradiction at all, and compare clarity (a §5.6 strategy-selection judgment).
The resolver assigns the start vertex color 0. Does the output depend on that choice? Tie your answer to the Phase 3 "unique up to swap" result.
Where would the entire construction break if conflicts allowed three groups instead of two (proper 3-coloring)? Which of the three proofs (existence, uniqueness, odd-cycle impossibility) survives, and which collapses? (3-coloring is genuinely harder — a hint of Chapter 30/37's complexity themes.)

Your Turn: Extensions

Option A (full-graph wrapper). Extend two_color to color a possibly disconnected graph by looping over uncolored vertices and coloring each component. Prove your wrapper returns a proper coloring iff every component is 2-colorable.
Option B (odd-cycle witness). When two_color returns None, modify it to return the offending odd cycle as evidence (track BFS parents and reconstruct the loop at the clashing edge). Argue that the returned cycle has odd length — a constructive disproof, the §5.4 partner of the Phase 4 contradiction.
Option C (uniqueness experiment). Write a function that enumerates all proper 2-colorings of a small connected graph by brute force, and check it always returns exactly two. Explain why this experiment supports — but does not replace — the Phase 3 proof (theme two).
Option D (model a real conflict). Encode a real "must be apart" scenario of your own (e.g. seating guests who feud, or scheduling exams that share students) as a conflict graph, run the resolver, and report whether a valid split exists. If it returns None, exhibit the odd cycle that makes the split impossible.

Key Takeaways

Three design questions, three strategies. Does a solution exist? → constructive existence (build it). Is it unique? → assume two, force them equal (§5.4). When is it impossible? → contradiction (§5.1). One small tool exercised all three.
Forcing drives both uniqueness and impossibility. Because two colors leave no freedom once one is fixed, connectivity forces the coloring (uniqueness) and an odd cycle forces a self-clash (impossibility).
Odd vs. even is a parity case split. The deepest fact here — 2-colorable iff no odd cycle — reduces to counting flips around a loop, the §5.3 even/odd dichotomy.
Build constructively when you can. Returning an explicit coloring (constructive existence) is worth far more to a caller than a non-constructive guarantee — you can return color.
Code triages; proof certifies. find_counterexample killed a false conjecture in one call, but only the proofs guarantee the resolver is right on every graph, forever (themes two and four).