Discrete Mathematics — Guided Project · builds on Lab 1
★ ProjectPr. El Hadiq Zouhair
This project builds on your Lab 1 functions (add_edge, build_graph, num_edges). The Setup cell on the next slide provides everything you need, so the project is self-contained — you can run it in a fresh notebook.
x or its negation ~x. A clause is an OR of three literals, e.g. $(x \lor \lnot y \lor z)$. A formula is an AND of clauses.
The 3-SAT decision problem: is there a True/False assignment of the variables making the whole formula true?
This is a famously hard problem — and it can be encoded as graph 3-coloring: from any formula $\varphi$ we build a graph $G_\varphi$ that is 3-colorable if and only if $\varphi$ is satisfiable. Translating one problem into another like this is called a reduction, and it is the standard tool for comparing the difficulty of problems.
New to all this? The next four slides explain every word from scratch, with pictures. If you already know SAT and graph coloring, skip to The three colors.
Everything here is built from True / False values. Just three words to learn:
x, y, z.x (read "x is true") or ~x (read "x is false").~y is true exactly when y is false.Think of it like a checklist: OR is forgiving (one true literal satisfies a clause), AND is strict (every clause must be satisfied).
Real Boolean formulas use ¬ (not), ∧ (and), ∨ (or), → (implies), ↔ (iff) and nested parentheses — they rarely look like a tidy AND of 3-literal clauses. So why does this project only deal with that special shape?
That is why the rest of this project assumes the formula already arrives as a list of 3-literal clauses: any formula you start with can be put into this form first.
A formula is satisfiable if some assignment of True/False to the variables makes the whole thing true. "Solving" 3-SAT means finding such an assignment — or proving that none exists.
x, y:Two assignments work, so this formula is satisfiable.
x to be true and false at the same time — impossible, so it is unsatisfiable.With $n$ variables there are $2^n$ possible assignments — far too many to try one by one for large $n$. That difficulty is what makes 3-SAT famous (it is NP-complete).
A proper coloring of a graph gives every vertex a color so that no edge joins two vertices of the same color. A 3-coloring is one that uses (at most) three colors.
Deciding whether an arbitrary graph can be 3-colored is itself a hard problem — and that is exactly the bridge we cross from 3-SAT.
We translate a formula $\varphi$ into a graph $G_\varphi$ so cleverly that the graph and the formula become two faces of the same question:
Turning one problem into another like this is called a reduction. Here is the whole pipeline on a tiny one-clause formula $\varphi = (x \lor y \lor z)$ — this is its graph $G_\varphi$, already properly 3-colored (green = the T color, red = F, blue = B):
How to read it. A variable is True when its vertex has the same color as the T vertex (green). Here x, y, z are all green, so the coloring says x = y = z = True — and indeed that makes $(x \lor y \lor z)$ true. The coloring solved the formula!
The little vertices labelled a₁ b₁ o₁ a₂ b₂ o₂ are the "gadgets" that wire the clause together — the rest of this project explains exactly how $G_\varphi$ is built (base triangle, one triangle per variable, OR gadgets per clause) and asks you to build and color it yourself.
These are the Lab 1 helpers this project needs, plus a draw_graph tuned for the larger SAT graph (it has $3 + 2V + 6C$ vertices — 33 already for the test formula — so the figure is bigger and the nodes smaller than in Lab 1).
T, F, B (added once for the whole graph).x and ~x; with $V$ variables that is $2V$.a, b, o), so $2 \times 3 = 6$ per clause; with $C$ clauses that is $6C$.~ for negation: [("x","y","z"), ("~x","~y","z"), ("x","~y","~z"), ("~x","y","~z")]. It has $V = 3$ variables (x, y, z) and $C = 4$ clauses, so $3 + 2{\cdot}3 + 6{\cdot}4 = 3 + 6 + 24 = \mathbf{33}$ vertices. (Counting the edges the same way is left to you — it is part of "What to hand in" at the end.)import networkx as nx
import matplotlib.pyplot as plt
def add_vertex(G, v):
if v not in G:
G[v] = []
def add_edge(G, u, v):
"""Add the undirected edge {u, v} (and its endpoints if needed); no duplicates."""
add_vertex(G, u); add_vertex(G, v)
if v not in G[u]: G[u].append(v)
if u not in G[v]: G[v].append(u)
def build_graph(vertices, edges):
G = {}
for v in vertices: add_vertex(G, v)
for u, v in edges: add_edge(G, u, v)
return G
def num_edges(G):
"""Half the degree sum (handshake lemma)."""
return sum(len(G[v]) for v in G) // 2
def to_nx(G):
H = nx.Graph(); H.add_nodes_from(G)
for u in G:
for v in G[u]: H.add_edge(u, v)
return H
def draw_graph(G, coloring=None, pos=None, title=""):
H = to_nx(G)
if pos is None:
pos = nx.spring_layout(H, seed=7)
palette = ["#2a9d8f", "#e63946", "#457b9d", "#e9c46a", "#f4a261", "#9b5de5"]
node_color = "#a8dadc" if coloring is None else [palette[coloring[v] % len(palette)] for v in H.nodes()]
plt.figure(figsize=(6.5, 5.0))
nx.draw(H, pos, with_labels=True, node_color=node_color,
node_size=600, font_weight="bold", font_size=8, edge_color="#666666")
plt.title(title); plt.show()
print("Setup OK — networkx", nx.__version__)Fix three colors with intended meanings True, False, Base. A base triangle T – F – B forces those three vertices to receive three different colors, so we can talk about "the T color", "the F color", "the B color" everywhere else.
T, F, B are mutually adjacent, they are forced to take three different colors; we then simply name them — the color the T vertex receives is "the T color," and so on. That anchor gives every other vertex a meaning: a vertex colored like T reads as true, like F as false, like B as neither.The base triangle: three mutually-joined vertices forced onto three different colors — our T, F, B anchors.
B is a deliberately neutral, "non-truth" color, and it does three jobs:
B, so it cannot be the B color — only the T or F color is left. This is the trick that turns an arbitrary 3-coloring into a clean truth value: a literal is never "Base," always True or False.F and B, leaving only the T color — that is how we demand "this clause is satisfied."B never means a truth value; it is the spare anchor color we use to push literals onto exactly two options and to force outputs to True.For each variable x we add two vertices — one for the literal x, one for its negation ~x — wired into a variable triangle x – ~x – B with edges x–~x, x–B and ~x–B. Those three edges pin down both literals:
x and ~x are joined to B, so neither can take the B color — only the T color or the F color is left.x and ~x are also joined to each other, so they must differ — one gets the T color, the other the F color.One valid coloring of a variable gadget: x and ~x avoid B's color and land on opposite truth values (here x true, ~x false).
x and ~x true, mirroring the fact that x and ¬x cannot both hold. The OR gadgets (next) then wire these literal vertices together to demand that every clause has at least one true literal.The coloured dots above are only a legend for the three colour classes; in an actual solution the x / ~x vertices take whichever of the T / F colours the search happens to assign.
For two inputs u, v: a fresh triangle a – b – out, plus the wires a – u and b – v.
u and v are the two INPUTS. They are existing vertices that already live in the graph — a literal like x or ~y, or the output of a previous gadget. They are the two things we want to OR together.a, b, out are three NEW vertices the gadget creates. a and b are internal helpers (just machinery); out is the result vertex.u ∨ v (the inputs), and the answer is read off the color of out: out can be colored T exactly when u ∨ v can be true. There is no "a ∨ b" — a and b are not variables of the formula, they only exist to force out to behave like an OR. In short: out = OR(u, v).↑ Colours here show each vertex's role (purple = input · orange = gadget · teal = output), not a 3-colouring — that is why adjacent a and b share the same orange. In a real 3-colouring they must differ, as shown next.
Take both inputs colored F (red). The triangle then forces a and b onto the two remaining colors T (green) and B (blue) — necessarily different — so out is forced to F. Legend: ● T ● F ● B.
Check the edges: a–u (green≠red ✓), b–v (blue≠red ✓), and the triangle a–b–out uses three distinct colours ✓. Both inputs F ⟹ out = F, exactly as the rule below states.
Now color both inputs T (green). Then a ≠ T and b ≠ T push a and b onto F and B — so the triangle's third vertex out is forced to T. Both inputs true ⟹ the OR is true:
Check the edges: a–u (red≠green ✓), b–v (blue≠green ✓), triangle uses three distinct colours ✓. Both inputs T ⟹ out = T (here it is even forced).
If just one input is true — say u = T (green), v = F (red) — then out is allowed to be T, though not forced. One valid coloring puts a = F, b = B, leaving out = T:
Check the edges: a–u (red≠green ✓), b–v (blue≠red ✓), triangle uses three distinct colours ✓. At least one input T ⟹ out can be T. (By symmetry u = F, v = T behaves the same.)
out was not forced — we chose to color it T. The exact same gadget (still u = T, v = F) also has a perfectly valid coloring with out = F, for instance a = B, b = T:Check the edges: a–u (blue≠green ✓), b–v (green≠red ✓), triangle uses three distinct colours ✓. So with one input T, out may be T or F — it is only forced to F when both inputs are F.
F and B, so only the T color is left). That forcing is possible only when the gadget allows out = T — i.e. when at least one input is True. If both inputs were False, out would be forced to F, clashing with the external "must be T," and the whole graph would become uncolorable. So a proper coloring exists exactly when every clause has at least one true literal.u and v are both colored F, then a and b must use the colors of T and B, forcing out to be colored F. If at least one input is colored T, out can be colored T.
u and v, and check which color out is forced into or allowed to take.Keep two facts in mind: the triangle a–b–out forces a, b, out onto three different colors (T, F, B in some order); and the wires force a ≠ color of u, and b ≠ color of v. The inputs u, v are each already colored T or F. Now walk through every possibility:
a ≠ F and b ≠ F, so a and b grab the colors T and B (in some order). The triangle's third vertex out must be the leftover color — forced to F.a ≠ T leaves a ∈ {F, B}; choose a = F, b = B, and out is free to be T. (It could also be F — the key point is that T is now allowed.)a ≠ T and b ≠ T, so a and b are F and B, and out is forced to T.| u | v | color of out |
|---|---|---|
| F | F | forced to F |
| T | F | can be T |
| F | T | can be T |
| T | T | forced to T |
Read the right column as the truth value of out: it is forced to F only when both inputs are F, and it can be T whenever at least one input is T. That is exactly the truth table of OR (false only when both inputs are false).
a and b depend on the inputs. The whole thing is tuned so that only the all-False case squeezes a, b onto {T, B} and pushes out to F — every other case leaves out free to be T. That single asymmetry is what encodes OR.For a 3-literal clause $(\ell_1 \lor \ell_2 \lor \ell_3)$, chain two OR gadgets — o1 = OR(l1, l2), then o2 = OR(o1, l3) — and force o2 to be colored T by joining it to both F and B. Here is what the whole clause gadget looks like:
Left to right: the three literals ℓ₁, ℓ₂, ℓ₃ feed two chained OR gadgets — first o₁ = OR(ℓ₁, ℓ₂), then o₂ = OR(o₁, ℓ₃) — and o₂ is joined to F and B, which leaves only the T color for it. Colours show each vertex's role (purple = literal, orange = gadget helper, teal = output); F and B are the fixed base anchors. One whole clause adds the 6 helper/output vertices a₁ b₁ o₁ a₂ b₂ o₂ — that is the 6C in the vertex count.
o2 would be forced to F — impossible. So any proper 3-coloring of $G_\varphi$ hands us a satisfying assignment: read off which literals share T's color.Negation of a literal. (No work to do here.)
def neg(lit):
"""Negation of a literal: 'x' <-> '~x'."""
return lit[1:] if lit.startswith("~") else "~" + lit
assert neg("x") == "~x" and neg("~x") == "x"The construction is mechanical: scan the formula and glue together three kinds of pieces. Here is the whole recipe, with the running example $\varphi = (x \lor y \lor z)$ so you can match every edge to the drawing earlier.
Add vertices T, F, B and join all three pairs:
T – F T – B F – B
This fixes what the three colors mean (already written for you in the skeleton).
Collect the variables of the formula (here x, y, z). For each variable v add v and ~v with the edges v–~v, v–B, ~v–B. For the example:
x – ~x x – B ~x – B | y – ~y y – B ~y – B | z – ~z z – B ~z – B
Each literal is now forced to the T or F color, and v, ~v always end up opposite (also given in the skeleton).
A clause $(\ell_1 \lor \ell_2 \lor \ell_3)$ becomes two chained OR gadgets, then a "force True" step. For the clause $(x \lor y \lor z)$, with $\ell_1=x,\ \ell_2=y,\ \ell_3=z$:
o₁ = OR(x, y) — fresh vertices a₁, b₁, o₁: triangle a₁–b₁, a₁–o₁, b₁–o₁, plus input wires a₁–x and b₁–y.o₂ = OR(o₁, z) — fresh vertices a₂, b₂, o₂: triangle a₂–b₂, a₂–o₂, b₂–o₂, plus wires a₂–o₁ (the previous output) and b₂–z (the third literal).o₂–F and o₂–B, so o₂ can only take the T color.add_edge calls (write or_gadget, call it twice per clause, then add the two "force" edges).T. Each clause's forced-T output o₂ guarantees that clause has at least one true literal — which is why a valid coloring exists exactly when the formula is satisfiable.or_gadget (5 calls to add_edge, then return the output vertex), then chain two OR gadgets per clause and force the final output to color T.def build_sat_graph(formula):
"""Graph that is 3-colorable iff `formula` (a list of 3-literal clauses) is satisfiable."""
G = {}
# base triangle
add_edge(G, "T", "F"); add_edge(G, "T", "B"); add_edge(G, "F", "B")
# one triangle x -- ~x -- B per variable
variables = {lit.lstrip("~") for clause in formula for lit in clause}
for x in sorted(variables):
add_edge(G, x, neg(x))
add_edge(G, x, "B")
add_edge(G, neg(x), "B")
def or_gadget(u, v, tag):
"""Create fresh vertices tag+'a', tag+'b', tag+'o' and return tag+'o'.
Wiring: triangle a-b-o, plus a-u and b-v."""
# TODO — 5 calls to add_edge, then return the output vertex
raise NotImplementedError
for i, (l1, l2, l3) in enumerate(formula):
# TODO — chain two OR gadgets (tags f"c{i}_1" and f"c{i}_2"),
# then force the final output to be colored T
# by joining it to "F" and to "B".
raise NotImplementedError
return GRun this cell to check your build_sat_graph — it tests the graph's structure only, so you can verify Task 1 before doing Task 2. It assumes the tag naming from the comments (tag+'a', tag+'b', tag+'o'; clause tags f"c{i}_1", f"c{i}_2").
def _adj(G, a, b): # undirected edge present?
return b in G.get(a, []) and a in G.get(b, [])
PHI1 = [("x", "y", "z")]
G1 = build_sat_graph(PHI1)
# 1) base triangle T - F - B
assert _adj(G1, "T", "F") and _adj(G1, "T", "B") and _adj(G1, "F", "B"), "base triangle missing"
# 2) a variable triangle x -- ~x -- B for every variable
for x in ("x", "y", "z"):
assert _adj(G1, x, neg(x)) and _adj(G1, x, "B") and _adj(G1, neg(x), "B"), f"variable triangle for {x} is wrong"
# 3) number of vertices = 3 (base) + 2*V (literals) + 6*C (two OR gadgets per clause)
V, C = 3, 1
assert len(G1) == 3 + 2*V + 6*C, f"expected {3 + 2*V + 6*C} vertices, got {len(G1)}"
# 4) first OR gadget of clause 0: triangle a-b-o, wires a-l1 and b-l2
a, b, o = "c0_1a", "c0_1b", "c0_1o"
assert _adj(G1, a, b) and _adj(G1, a, o) and _adj(G1, b, o), "OR-gadget triangle a-b-o is broken"
assert _adj(G1, a, "x"), "wire a-u missing (first input l1)"
assert _adj(G1, b, "y"), "wire b-v missing (second input l2)"
# 5) second gadget chains the first output, takes l3, output forced toward T (joined to F and B)
assert _adj(G1, "c0_2a", "c0_1o"), "second gadget not chained to the first output o1"
assert _adj(G1, "c0_2b", "z"), "third literal l3 not wired into the second gadget"
assert _adj(G1, "c0_2o", "F") and _adj(G1, "c0_2o", "B"), "clause output must be joined to F and B"
# 6) no duplicated neighbours (add_edge must not double-insert)
for u in G1:
assert len(G1[u]) == len(set(G1[u])), f"duplicate neighbour stored for {u}"
# 7) vertex-count formula on a 2-clause formula
G2 = build_sat_graph([("x", "y", "z"), ("~x", "~y", "z")])
assert len(G2) == 3 + 2*3 + 6*2 # V=3, C=2 -> 21 vertices
print("Task 1 ✔ build_sat_graph has the right structure")The 3-coloring solver is recursive, not a plain loop: it is a backtracking search. It colors the vertices one at a time, and whenever it gets stuck it undoes its last choice and tries another. The idea, step by step:
nodes[i], try each colour c ∈ {0, 1, 2} in turn.c is allowed only if no already-coloured neighbour of nodes[i] already uses c.c is safe, set color[nodes[i]] = c and call backtrack(i + 1) to colour the next vertex.del color[nodes[i]]) and try the next colour. If no colour works, return False — and the caller backtracks in turn.i == len(nodes), every vertex is coloured — return True.backtrack(0) returns True exactly when a full proper 3-colouring exists — and then the color dict holds it. If the search exhausts every option, the graph is not 3-colourable and three_color returns None.three_color: when i == len(nodes) you are done; otherwise try each color c in 0, 1, 2 that no already-colored neighbor of nodes[i] uses, assign it, recurse, and undo on failure.def three_color(G):
"""A proper 3-coloring of G as a dict {vertex: 0, 1 or 2}, or None if impossible.
Backtracking: order the vertices (decreasing degree works well), then try
each color in turn for the current vertex and recurse."""
nodes = sorted(G, key=lambda v: -len(G[v]))
color = {}
def backtrack(i):
# TODO — if i == len(nodes): done. Otherwise try each color c in 0,1,2
# that no already-colored neighbor of nodes[i] uses.
raise NotImplementedError
return color if backtrack(0) else NoneRun this to check three_color on small graphs (no SAT construction needed): a triangle, a non-3-colourable K₄, a path, and a satisfiable formula's graph.
def _proper(G, c): # proper colouring? (and not None)
return c is not None and all(c[u] != c[v] for u in G for v in G[u])
# a triangle IS 3-colourable, and uses all three colours
tri = {}
add_edge(tri, "p", "q"); add_edge(tri, "p", "r"); add_edge(tri, "q", "r")
c = three_color(tri)
assert _proper(tri, c), "the triangle should be properly 3-coloured"
assert len(set(c.values())) == 3, "a triangle needs all three colours"
# K4 (every pair joined) is NOT 3-colourable -> None
K4 = {}
vs = ["a", "b", "c", "d"]
for i in range(4):
for j in range(i + 1, 4):
add_edge(K4, vs[i], vs[j])
assert three_color(K4) is None, "K4 cannot be 3-coloured"
# a path (bipartite) is 3-colourable
path = {}
add_edge(path, 1, 2); add_edge(path, 2, 3); add_edge(path, 3, 4)
assert _proper(path, three_color(path))
# on the SAT graph of a satisfiable formula, a proper colouring must exist
Gs = build_sat_graph([("x", "y", "z")])
assert _proper(Gs, three_color(Gs)), "satisfiable formula -> a 3-colouring must exist"
print("Task 2 ✔ three_color gives proper 3-colourings (and None when impossible)")decode does — preciselydecode(coloring, formula) turns a finished 3-coloring back into a True/False assignment of the variables.
coloring — a dict {vertex: 0 / 1 / 2} (a proper 3-coloring of the SAT graph) — and the formula it was built from.{variable: bool}, one True/False value per variable.x is True if and only if its vertex has the same color as the vertex 'T' — that is, coloring[x] == coloring["T"]; otherwise it is False.How it computes that, step by step:
~ off every literal in every clause (lit.lstrip("~")) and keep the distinct names — these are the variables x, y, z, … (with no negation).x, set assignment[x] = (coloring[x] == coloring["T"]).{x: True/False, …}.x's color is exactly one of those two, and comparing it to coloring["T"] reads off its truth value. Only the positive vertex x is needed — its partner ~x automatically received the opposite color.coloring["T"], not the literal number 0 — the solver may assign the colors 0/1/2 to T, F, B in any order. (2) The keys of the returned dict are variable names without ~, and the values are Python booleans (True/False).decode: a variable is True iff its vertex has the same color as vertex 'T'. Return a dict {variable: bool}. (evaluate is provided — no work there.)def decode(coloring, formula):
"""Read the truth assignment off a 3-coloring of the SAT graph:
a variable is True iff its vertex has the same color as vertex 'T'."""
# TODO — return a dict {variable: bool}
raise NotImplementedError
def evaluate(formula, assignment):
"""Truth value of the formula under the assignment (provided)."""
def value(lit):
return not assignment[lit[1:]] if lit.startswith("~") else assignment[lit]
return all(any(value(lit) for lit in clause) for clause in formula)Run this to check decode: first on a hand-made colouring with a known answer, then end-to-end (build → colour → decode → the assignment must satisfy the formula).
# a hand-made colouring (take T=0, F=1, B=2): x shares T, y shares F, z shares T
fake = {"T": 0, "F": 1, "B": 2, "x": 0, "~x": 1, "y": 1, "~y": 0, "z": 0, "~z": 1}
PHI_d = [("x", "y", "z"), ("~x", "y", "z")]
asg = decode(fake, PHI_d)
assert asg == {"x": True, "y": False, "z": True}, f"decode misread the colouring: {asg}"
assert set(asg) == {"x", "y", "z"}, "keys must be the variables (no '~')"
assert all(isinstance(b, bool) for b in asg.values()), "values must be True / False"
# end to end: build -> colour -> decode -> the assignment must satisfy the formula
G_d = build_sat_graph(PHI_d)
col_d = three_color(G_d)
assert col_d is not None, "PHI_d is satisfiable, so a colouring must exist"
assert evaluate(PHI_d, decode(col_d, PHI_d)), "decoded assignment must satisfy the formula"
print("Task 3 ✔ decode reads a satisfying assignment off the colouring")Run this once all three tasks are done. A satisfiable formula must yield a proper 3-coloring whose decoded assignment satisfies it.
PHI = [("x", "y", "z"),
("~x", "~y", "z"),
("x", "~y", "~z"),
("~x", "y", "~z")]
G_sat = build_sat_graph(PHI)
print("SAT graph:", len(G_sat), "vertices,", num_edges(G_sat), "edges")
col = three_color(G_sat)
assert col is not None, "PHI is satisfiable, so a 3-coloring must exist"
assert all(col[u] != col[v] for u in G_sat for v in G_sat[u]) # proper
assignment = decode(col, PHI)
print("assignment read off the coloring:", assignment)
assert evaluate(PHI, assignment), "the decoded assignment must satisfy PHI"
print("Challenge ✔ — the coloring solved the formula!")
draw_graph(G_sat, coloring=col, title="The 3-SAT graph of PHI, properly 3-colored")The formula below contains all $8$ possible clauses on x, y, z, so every assignment falsifies one of them: it is unsatisfiable, and its graph should therefore not be 3-colorable. Uncomment and run — the backtracking has to exhaust the search space, so it takes noticeably longer than the satisfiable case.
UNSAT = [(a, b, c) for a in ("x", "~x") for b in ("y", "~y") for c in ("z", "~z")]
# print(three_color(build_sat_graph(UNSAT))) # expected: NoneWrite a tiny brute-force solver that tries all $2^n$ assignments, then confirm on many random formulas that your graph is 3-colorable exactly when the formula is satisfiable. If the two ever disagree, your gadget wiring has a bug.
import itertools, random
def brute_force_sat(formula):
variables = sorted({lit.lstrip("~") for clause in formula for lit in clause})
return any(evaluate(formula, dict(zip(variables, bits)))
for bits in itertools.product([False, True], repeat=len(variables)))
rng = random.Random(0)
for _ in range(100):
vs = [chr(ord("a") + i) for i in range(rng.randint(2, 4))]
phi = [tuple(("~" if rng.random() < .5 else "") + rng.choice(vs) for _ in range(3))
for _ in range(rng.randint(1, 6))]
assert (three_color(build_sat_graph(phi)) is not None) == brute_force_sat(phi)
print("Reduction matches a brute-force solver on 100 random formulas ✔")build_sat_graph, three_color and decode, with the test cell printing Challenge ✔.Before moving on, write a few sentences on each prompt below. There is no single right answer — the point is to connect this one project to the bigger picture.