Cook–Levin on a concrete NP language

For a specific NP language (HAMPATH), walk through the four clause families that build φ_x.

• The four families are not independent. Each constrains different aspects; the conjunction is the whole formula. Missing one breaks correctness.
• φ_cell uses both "at least one" and "at most one" clauses. The disjunction says the cell has some symbol; the pairwise-not-both clauses prevent multiple symbols at once.
• Variables are indexed by (row, col, symbol). O(n^k) rows × O(n^k) cols × O(1) symbols = O(n^2k) variables.

• Q1. Why is φ_cell needed?
  Without it, SAT variables could "claim" a cell holds multiple symbols simultaneously, which is meaningless as a TM tape state. φ_cell enforces exactly-one-symbol per cell.
• Q2. How big is the formula?
  O(n^2k) clauses for a TM running in time n^k. Polynomial in input size.
• Q3. Why is this a polynomial reduction?
  The formula is constructed by a procedure whose running time is polynomial in |x|. So if SAT were in P, every NP language would be too — proving SAT is NP-complete.
• Q4. How does the 2×3 window encode the transition?
  The window has 2 rows (consecutive configurations) and 3 columns (the head's cell plus neighbours). For each transition δ in M, the legal 2×3 patterns are enumerated; φ_move says every window matches one of them.

Sipser: Theorem 7.37 (Cook–Levin). Lecture notes: Module 5 slide 3. Companion problems: P25 (Cook-Levin tableau), P22 (SAT).