SAT solving, logic circuits, and Sudoku as logic
Mathematical logic is not just theory -- it powers real technology. SAT solvers verify hardware and software, logic gates are the physical substrate of computation, and constraint satisfaction underlies everything from scheduling to puzzle solving.
In this lesson, you will watch a SAT solver search for solutions, build logic circuits from gates, and see how even a simple Sudoku puzzle is a logic problem in disguise.
The Boolean satisfiability problem (SAT) asks whether a CNF formula has a satisfying assignment. Despite being NP-complete, modern SAT solvers handle formulas with millions of variables using clever techniques: unit propagation, pure literal elimination, and systematic backtracking (DPLL algorithm).
Key insight: SAT solvers are the engine behind hardware verification, software testing, AI planning, and cryptanalysis. The gap between NP-completeness in theory and practical efficiency is one of the great success stories of computer science.
Every boolean function has a circuit implementation. AND, OR, NOT, and XOR gates combine to compute any truth function. Toggle the inputs and watch signals propagate through the wires. The half adder -- which computes a one-bit sum and carry -- is the building block of every CPU's arithmetic unit.
Key insight: The correspondence between boolean algebra and digital circuits is exact. Circuit optimization is literally boolean simplification -- the Karnaugh maps from the previous lesson directly reduce gate count.
A Sudoku puzzle is a constraint satisfaction problem: each cell must have exactly one value, and each row, column, and box must contain all values. These constraints can be expressed as propositional formulas. Solving the puzzle is equivalent to finding a satisfying assignment -- logic in action.
Key insight: Constraint propagation (if a cell must be 3, eliminate 3 from its row, column, and box) is exactly unit propagation in the corresponding SAT encoding. The techniques of logic directly solve the puzzle.