Logic in Practice

SAT solving, logic circuits, and Sudoku as logic

Logic in Practice

Logic runs real machines: solvers that check chips, gates that do arithmetic, and the reasoning behind every Sudoku.

SAT Solver Visualizer

Pick a formula and step through the DPLL search. Clauses turn blue when satisfied and red on a conflict, which forces a backtrack.

Step 0/1

Result: SATISFIABLE

Go deeper:The satisfiability problem

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.

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.

Logic Circuit Builder

Choose a circuit and toggle the inputs to watch signals propagate. Try the Half Adder: an XOR gives the sum and an AND gives the carry.

Output: 0 (false)

Go deeper:Circuits compute truth functions

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.

Sudoku as Logic

Click a cell to cycle its value, or press Auto-Solve. Every row, column, and box has to end up holding each value once.

Constraints satisfied: 0/13

○ All cells filled

○ Row 1 has {1,2,3,4}

○ Row 2 has {1,2,3,4}

○ Row 3 has {1,2,3,4}

○ Row 4 has {1,2,3,4}

○ Col 1 has {1,2,3,4}

○ Col 2 has {1,2,3,4}

○ Col 3 has {1,2,3,4}

○ Col 4 has {1,2,3,4}

○ Box (1,1) has {1,2,3,4}

○ Box (1,2) has {1,2,3,4}

○ Box (2,1) has {1,2,3,4}

○ Box (2,2) has {1,2,3,4}

Go deeper:Sudoku as constraint satisfaction

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.

Key Takeaways

SAT solvers turn the theory of propositional logic into a practical tool for millions-variable problems.
Logic gates are the physical realization of boolean algebra -- the foundation of all digital hardware.
Constraint satisfaction problems (like Sudoku) are logic problems in disguise.
The bridge between mathematical logic and practical computation is direct and deep.

Spot a mistake or have an idea?