Flip variables and visually verify or break clauses.
CLO-3R2·30 ptsL10
🔊 Listen
1 · SAT, formally
SAT = {⟨φ⟩ : φ is a satisfiable Boolean formula in conjunctive normal form (CNF)}. A CNF formula is a conjunction of clauses; each clause is a disjunction of literals; a literal is either a variable xi or its negation ¬xi. The formula is satisfiable if there exists an assignment of true/false to the variables that makes every clause true.
SAT ∈ NP (the easy direction)
Certificate: a satisfying assignment τ ∈ {0,1}n. Verifier: for each clause, check whether at least one literal evaluates to true under τ. Total time: O(m) where m is the number of literal-occurrences. Polynomial in |φ|.
Cook–Levin (Sipser 7.37)
SAT is NP-complete. Every problem in NP reduces to SAT in polynomial time. So SAT is "as hard as anything in NP" and is the canonical starting point for the NP-complete chain.
🔊 Listen
2 · How a clause becomes green
🔊 Listen
3 · Animated demo · auto-plays · loops
Auto-solver tries assignments in order Auto-plays
🔊 Listen
4 · Pitfalls
Negation flips the literal, not the variable. ¬x is a literal — true when x is false. The variable x itself doesn't change; the literal's truth value does.
A clause needs only one true literal. Don't accidentally require all literals to be true — that's an AND, not an OR. Clauses are ORs.
An empty clause is unsatisfiable. A clause with zero literals is false by convention. Some encodings produce empty clauses; recognise them as immediate "no."
Practical SAT solvers ≠ worst-case SAT. DPLL and CDCL solve most natural SAT instances in seconds. The worst case (2ⁿ) is real and engineered by adversarial inputs, but it isn't the typical case.
🔊 Listen
5 · Q&A defence notes
Q1. What's the worst-case running time of brute-force SAT?
2n assignments to try, each checked in O(m). Total O(m · 2n). For n=20 that's ≈ 10⁶, for n=30 ≈ 10⁹, for n=60 ≈ 10¹⁸.
Q2. Are there smarter SAT algorithms?
Yes — DPLL (1962) uses unit propagation and backtracking; CDCL (modern) adds conflict-driven clause learning. Practically fast, but worst-case still exponential. No polynomial-time algorithm is known.
Q3. How does a verifier differ from a solver?
A verifier receives both the formula and a candidate assignment. It just plugs in and checks. A solver receives only the formula and must search for an assignment. The verifier runs in O(m); the solver currently needs exponential time in the worst case.
Q4. Is 2SAT also NP-complete?
No — 2SAT (clauses with ≤ 2 literals) is in P. It reduces to strongly-connected components in an implication graph. The 2-vs-3 boundary is the precise place where SAT becomes hard.