Case Study: Building a Tiny SAT-Based Scheduler

"Tell the computer what a correct answer looks like, and let it find one."

Executive Summary

In this build-focused case study you will encode a real constraint problem — assigning a handful of meetings to two time slots without conflicts — as a single compound proposition, and then solve it by the brute-force satisfiability search from §1.6. The deliverable is a small, honest tool: a function that turns constraints into a propositional formula and a search that returns a satisfying assignment (a valid schedule) or reports that none exists (the constraints are a contradiction). This is the constructive flip side of Case Study 1: there we audited one fixed condition; here we build a formula from moving parts and let the machine search all $2^n$ assignments for a solution. Along the way you will feel the exponential wall of §1.6 firsthand — and see exactly why the same truth-table machinery that is trivial at four variables becomes a monster at sixty. This is the seed of the dependency-resolution and scheduling solvers mentioned in §1.6, and it previews the SAT story that culminates in Chapter 37.

Skills applied

• Modeling a constraint problem with propositional variables, one per yes/no decision (§1.2).
• Encoding "must," "must not," and "exactly one" as conjunctions of clauses (§1.2, §1.4).
• Implementing brute-force satisfiability with itertools.product (§1.3, §1.6).
• Reading a satisfying assignment as a solution, and unsatisfiability as "no solution exists" (§1.6).
• Estimating cost and confronting the exponential wall (§1.6).

Background: from constraints to a formula

The scenario

A small team holds three recurring meetings — Standup (S), Design review (D), and Retro (R) — and has exactly two time slots, morning and afternoon. The constraints, gathered from the calendar invites, are:

1. Each meeting must be in exactly one slot (it can't be unscheduled, and it can't be in both).
2. Standup and Design review cannot share a slot (the same lead runs both).
3. Design review must be in the morning (a remote attendee is only available then).
4. Retro and Standup cannot both be in the afternoon (the room is double-booked then).

A human can solve this by hand. The exercise is to make a computer solve it the way a SAT solver does: turn every constraint into logic, conjoin them, and search for an assignment that makes the whole conjunction true.

💡 Intuition: Think of each yes/no decision as a switch — a propositional variable. A constraint is a proposition that must come out true. The full problem is the conjunction of all constraints: a single proposition that is true exactly for the schedules that satisfy every rule at once. Solving the problem is finding one input that lights it up — satisfiability (§1.6).

Why this matters

Configuration ("can these package versions all be installed together?"), scheduling ("can these exams be slotted with no student double-booked?"), and verification ("is there any input that drives this circuit into a bad state?") are all, underneath, satisfiability questions (§1.6). Industrial SAT solvers do exactly what you are about to build — encode constraints as a propositional formula and search for a satisfying assignment — only with decades of cleverness layered on top of the brute-force core. Building the toy now demystifies the giant later.

Phase 1: Choose the variables

The first modeling decision is the most important: what are the propositions? Each meeting goes in one of two slots, so a single Boolean per meeting suffices. Let

• $s$ = "Standup is in the morning" (so $\neg s$ = "Standup is in the afternoon"),
• $d$ = "Design review is in the morning,"
• $r$ = "Retro is in the morning."

Three variables, $2^3 = 8$ possible schedules. Because each variable already means "morning vs. afternoon," constraint 1 — exactly one slot — is automatically satisfied: a Boolean is true or false, never both and never neither. Choosing variables well made one constraint vanish. That is abstraction earning its keep (theme three): the right representation does work for you.

🔄 Check Your Understanding With this encoding, how would you express "Standup is in the afternoon"? How many distinct schedules are there in total, and why?

Answer

"Standup is in the afternoon" is $\neg s$. There are $2^3 = 8$ schedules: each of the three meetings independently goes morning ($T$) or afternoon ($F$), and $2 \times 2 \times 2 = 8$. This is the row count of a three-variable truth table (§1.3).

Phase 2: Encode each constraint as a clause

Now translate the remaining constraints (2–4) into propositions over $s, d, r$.

Constraint 2 — Standup and Design review cannot share a slot. "Share a slot" means both morning ($s \land d$) or both afternoon ($\neg s \land \neg d$). "Cannot share" is the negation of "share": $$c_2 \;\equiv\; \neg\big((s \land d) \lor (\neg s \land \neg d)\big).$$ By the chapter's exercise 1.11, "both agree" is exactly the biconditional, so $(s \land d) \lor (\neg s \land \neg d) \equiv (s \leftrightarrow d)$, and its negation is $s \oplus d$. So $c_2 \equiv s \oplus d$: Standup and Design review must be in different slots. (Either form is fine to code; the xor form is tidier.)

Constraint 3 — Design review must be in the morning. Directly, $c_3 \equiv d$.

Constraint 4 — Retro and Standup cannot both be in the afternoon. "Both afternoon" is $\neg r \land \neg s$. "Cannot" negates it: $c_4 \equiv \neg(\neg r \land \neg s)$, which by De Morgan (§1.4) is $r \lor s$. So at least one of Retro, Standup is in the morning.

The full problem is the conjunction of all constraints: $$\Phi \;\equiv\; c_2 \land c_3 \land c_4 \;\equiv\; (s \oplus d) \land d \land (r \lor s).$$ A satisfying assignment of $\Phi$ is a valid schedule; if $\Phi$ is unsatisfiable, no schedule meets all the rules.

⚠️ Common Pitfall: When translating "cannot both," negate the conjunction and apply De Morgan; do not write $\neg r \lor \neg s$ by reflex without checking. Here $\neg(\neg r \land \neg s) \equiv r \lor s$ — the double negations cancel. Skipping the De Morgan step is how a "not both afternoon" constraint silently becomes "not both morning." Translate carefully, then simplify.

Phase 3: Build the solver

Now the code. We need two pieces: a function that evaluates $\Phi$ on an assignment (it is just the conjunction of the clauses), and the brute-force search first_satisfying from §1.6 that walks all $2^n$ assignments. We build the formula from small, named clauses so the encoding stays readable and auditable.

from itertools import product

def first_satisfying(fn, names):
    """Return the first assignment dict making fn true, or None if unsatisfiable.
    Walks all 2^n assignments in the chapter's row order (True before False)."""
    for row in product([True, False], repeat=len(names)):
        if fn(*row):
            return dict(zip(names, row))
    return None

# Each clause is a Boolean function of (s, d, r); Phi is their conjunction.
def phi(s, d, r):
    c2 = (s != d)            # s XOR d : Standup and Design in different slots
    c3 = d                   # Design review in the morning
    c4 = (r or s)            # Retro or Standup in the morning (not both afternoon)
    return c2 and c3 and c4

print("Schedule:", first_satisfying(phi, ["s", "d", "r"]))
# Expected output:
# Schedule: {'s': False, 'd': True, 'r': True}

Let us verify that expected output by hand, tracing the search in the chapter's row order ($T$ before $F$). We need the first row where phi is true.

The search scans rows 1–4 (all false), then hits row 5: $s=F, d=T, r=T$, where $\Phi = T$. That is the first satisfying assignment, so first_satisfying returns {'s': False, 'd': True, 'r': True} — matching the expected output. Decoded: Standup in the afternoon, Design review in the morning, Retro in the morning. Check it against the original constraints: Design is in the morning (3 ✓); Standup (afternoon) and Design (morning) differ (2 ✓); Retro is in the morning, so they are not both in the afternoon (4 ✓). The tool's answer is a genuinely valid schedule.

💡 Intuition: first_satisfying is a truth table that stops early. It builds the same $2^n$ rows as §1.3, but instead of printing them all it returns the moment it finds output $T$. "Build the table, scan for a $T$" is brute-force SAT.

Phase 4: Read unsatisfiability as "no schedule exists"

A good solver must also recognize when constraints cannot be met. Suppose the team adds one more rule:

5. Retro must be in the afternoon (the only time the whole company is free): $c_5 \equiv \neg r$.

Add it and re-solve:

def phi2(s, d, r):
    c2 = (s != d)
    c3 = d
    c4 = (r or s)
    c5 = not r          # NEW: Retro in the afternoon
    return c2 and c3 and c4 and c5

print("Schedule:", first_satisfying(phi2, ["s", "d", "r"]))
# Expected output:
# Schedule: None

Why None? Trace it. The only satisfying row of the old $\Phi$ was row 5 ($s=F, d=T, r=T$). But the new clause $c_5 = \neg r$ is false there (since $r = T$). Could another row work? We need $c_4 = r \lor s$ **and** $c_5 = \neg r$, i.e. $r = F$, which forces $s = T$ (so that $r \lor s$ holds). Then $c_2 = s \oplus d$ with $s = T$ forces $d = F$. But $c_3 = d$ demands $d = T$. Contradiction: $d$ cannot be both $F$ and $T$. So no assignment satisfies all of $c_2, c_3, c_4, c_5$ — $\Phi'$ is unsatisfiable, a contradiction (§1.6), and the search correctly returns None after checking all eight rows.

This is the payoff of the satisfiability framing: the same tool that finds a schedule also proves none exists. An over-constrained calendar isn't a crash or a guess — it is a propositional contradiction, and the solver certifies it by exhausting every possibility.

🔗 Connection. "$\Phi'$ is unsatisfiable" is precisely "$\neg \Phi'$ is a tautology" (§1.6). So our scheduler, asked an unsatisfiable problem, has proved a tautology — the negation of the constraints holds for every schedule. This is the loop the chapter closed: satisfiability and validity are two faces of one coin, which is why SAT solvers double as theorem provers (a thread Chapter 37 picks up in full).

Phase 5: Feel the exponential wall

Our problem had three variables and eight rows — instant. But the brute-force search is for row in product([True, False], repeat=n), which is $2^n$ iterations. Watch how fast that grows as the calendar does. Suppose instead of two slots we have many meetings, each a Boolean, and $n$ of them:

The doubling per variable that looked harmless in §1.3 is, from here, an exponential cliff. Our solver is correct for any number of meetings — it will eventually find a schedule or prove none exists — but "eventually" can outlast the universe. And the unsettling fact from §1.6 stands: nobody knows a method guaranteed to be dramatically faster than this on every input. That open question is P vs. NP, and your three-line first_satisfying is brushing right up against it.

🚪 Threshold Concept. You have now built the thing §1.6 only described: a SAT solver. It is a few lines, it is correct, and it is exponential. The gap between "I can specify a correct answer" and "I can find one efficiently" — easy to check, maybe hard to find — is the most important open problem in computer science. Real solvers beat the table with heuristics, but the worst case still looms. Once you have written the loop and watched the row count explode, the P-vs-NP boundary stops being abstract.

🐛 Find the Error: A teammate encodes constraint 4 ("Retro and Standup not both in the afternoon") as c4 = (not r) or (not s) and is surprised the scheduler now puts both in the morning-forbidden arrangement. Which step did they skip, and what does (not r) or (not s) actually forbid?

Answer

They negated "both afternoon" incorrectly. "Both afternoon" is $\neg r \land \neg s$; its negation is $\neg(\neg r \land \neg s) \equiv r \lor s$ (De Morgan + double negation), i.e. "at least one in the morning." The teammate instead wrote $\neg r \lor \neg s$, which is the negation of $r \land s$ ("both morning") — so they accidentally forbade both meetings being in the morning. Apply De Morgan to the correct conjunction.

Discussion Questions

1. We made constraint 1 ("exactly one slot") vanish by choosing one Boolean per meeting. If instead you used two Booleans per meeting — $m_S$ = "Standup in morning," $a_S$ = "Standup in afternoon" — how would you have to encode "exactly one slot" as explicit clauses? Why is the one-variable encoding better here? (This is the modeling lesson of Phase 1.)
2. With three slots instead of two, a single Boolean per meeting no longer suffices. Propose a variable scheme and write the "exactly one of three slots" constraint for one meeting. (You are rediscovering why real SAT encodings of scheduling grow quickly in variable count.)
3. first_satisfying returns the first solution in the chapter's row order. How would you modify it to return all satisfying assignments, and what is the worst-case number it might return for $n$ variables?
4. In Phase 4 the unsatisfiability had a short hand-proof (a chain forcing $d = F$ and $d = T$). For a $60$-variable problem you could not enumerate the rows. What does that tell you about the difference between finding a satisfying assignment and proving unsatisfiability? (Both are hard in the worst case; this previews Chapter 37.)
5. Argue why "the schedule the tool returned satisfies every constraint" is something you can verify quickly (in one pass), even though the tool may have searched exponentially many rows to find it. Connect this to the "easy to check, hard to find" asymmetry of §1.6.

Your Turn: Extensions

• Option A (count solutions). Modify first_satisfying into count_satisfying(fn, n) that returns how many of the $2^n$ assignments satisfy fn (reuse is_tautology's all-over-product idea, but sum instead). Run it in your head on the Phase 3 $\Phi$ and confirm it returns $1$. State the expected output. (Counting satisfying assignments — "#SAT" — is even harder than SAT; you are touching a deep problem.)
• Option B (a real mini constraint). Encode this puzzle and solve it with your tool: three friends — Ana, Ben, Cy — must each be assigned to "frontend" or "backend"; Ana and Ben must be on different teams; Cy refuses to be on backend; and at least two people must be on frontend. Choose variables, write the clauses, and hand-trace first_satisfying to find an assignment (or show there is none).
• Option C (toward dependency resolution). Recall §1.6's package example. Encode: "install $A$ only if $B$ is installed" ($A \rightarrow B$) and "$A$ and $C$ conflict" ($\neg(A \land C)$). Add "$C$ is required" ($C$). Build $\Phi$, solve it, and report which packages get installed. Then add "$A$ is required" ($A$) and explain, via a short hand-argument, why $\Phi$ becomes unsatisfiable.

Key Takeaways

1. Modeling is choosing variables. One Boolean per meeting made "exactly one slot" free; a worse encoding would have needed extra clauses. The representation does work for you (theme three).
2. A constraint problem is one big conjunction. Each rule becomes a clause; the whole problem is their and. Solving it is satisfiability — find an input that makes the conjunction true.
3. The same tool finds solutions and proves their absence. A satisfying assignment is a schedule; None (unsatisfiability) is a proof that no schedule exists — a contradiction in the constraints.
4. You built a SAT solver, and it is exponential. for row in product(...) is $2^n$ rows. Correct for any size, hopeless past sixty-odd variables — the exponential wall behind P vs. NP that Chapter 37 confronts head-on.