Checking is not finding

Consider

$$(a\lor b)\land(\neg a\lor c)\land(\neg b\lor c).$$

Someone hands you $a=true,b=false,c=true$. Checking requires three clause evaluations. Finding such an assignment without the hint may require choices and backtracking. This gap between a short certificate and the work of discovery defines the class NP: yes-instances have certificates verifiable in polynomial time.

SAT is decidable by enumerating all $2^n$ assignments. The concern is growth, not computability. No polynomial-time algorithm for all SAT instances is known, and no proof rules one out; that open question is the famous $P$ versus $NP$ problem.

One choice forces the next

A clause $(a\lor b\lor c)$ is satisfied when any literal is true. If $a=false$ and $b=false$, then $c$ is no longer a choice: it must be true. A clause with exactly one unassigned literal and all others false is a unit clause. Assigning its remaining literal is unit propagation.

Repeat until no unit clause remains or a clause becomes entirely false. One guessed value may cascade through thousands of forced values. The solver is not enumerating complete rows; it is asking the residual formula from Chapter 12 what remains after each assignment.

Pure propagation is incomplete: some satisfiable formulas need a choice. Choose a variable, assign a value, propagate, and if conflict appears, backtrack. This is the Davis–Putnam–Logemann–Loveland shape.

Contradictions should leave a scar

Suppose choices $a=true$ and $d=false$ propagate to a conflict. The naive solver flips the latest choice and may rediscover the same bad combination elsewhere. A conflict-driven clause-learning solver traces which assignments implied the conflict and records a clause forbidding that combination, perhaps $(\neg a\lor d)$.

The learned clause is not a heuristic guess. It is logically implied by the original formula, so adding it preserves all solutions while removing a region already proved impossible. Backjumping then returns to the earliest decision that can change the conflict.

This is induction's invariant and counterexample shrinking meeting search: every learned clause is a permanent proof fragment; every conflict makes the remaining search strictly better informed.

The universal adapter of finite search

In 1971 Stephen Cook proved that every problem whose yes-certificates can be verified in polynomial time can be translated, with polynomial overhead, into propositional satisfiability. SAT was the first NP-complete problem.

NP-complete does not mean “always exponential,” “unsolvable,” or “SAT solvers are pointless.” It means a polynomial algorithm for the problem would yield polynomial algorithms for every problem in NP. Structure in real instances—short implications, repeated subproblems, good variable choices—often makes them tractable.

Where search runs out

• A solver returning satisfiable should provide the assignment; an unsatisfiable claim needs a checkable proof trace when assurance matters.
• Heuristics change performance, not semantics. Their benchmark wins do not strengthen the answer.
• Encoding can dominate. A mathematically equivalent CNF may expose or hide propagation.
• Worst-case hardness and typical runtime are different claims; report both honestly.

Lessons

• Finding a satisfying assignment and checking one are different jobs.
• Unit propagation computes forced consequences of a partial assignment.
• Learned clauses turn conflicts into reusable proof and prevent repeated failure.
• NP-completeness makes SAT a universal target for efficiently verifiable finite search, not a declaration that every instance is hopeless.

Practice

1. Unit-propagate $(a)\land(\neg a\lor b)\land(\neg b\lor c)$.
2. Encode “exactly one of x, y, and =z=” in CNF.
3. Explain why a satisfying assignment is a proof of SAT but a timeout is not a proof of UNSAT.
4. One week later, reconstruct the solver loop: decide, propagate, conflict, learn, backjump.

The next question is about identical functions

Two formulas may look nothing alike yet compute the same Boolean function. Testing rows can establish equality for a few variables, but the table doubles with each new one. The next chapter chooses one shape for each function so equality becomes structural—and states the two round-trip laws that keep that shape honest.

References

1. Davis, Logemann, Loveland. “A Machine Program for Theorem-Proving.” Communications of the ACM, 1962. — the primary branching and propagation procedure
2. Cook. “The Complexity of Theorem-Proving Procedures.” STOC, 1971. — the primary NP-completeness result
3. Biere et al., eds.. “Handbook of Satisfiability, 2nd ed..” IOS Press, 2021. — modern algorithms, proof systems, and applications