Propositional logic and SAT problems
Boolean satisfiability as a knowledge representation method: from brute-force truth tables to CNF, DPLL, and stochastic SAT solvers.
Boolean satisfiability asks whether a propositional formula can be made true by some assignment of truth values to its variables. SAT solvers underpin hardware verification, automated planning, and constraint satisfaction at scale. Brute-force search over 2n combinations doesn't scale, so the challenge is avoiding most of that space.
The article covers Conjunctive Normal Form (CNF) as the standard input format, the DPLL algorithm with unit propagation and pure literal elimination as the classical complete solver, and stochastic approaches (GSAT, WalkSAT) for large instances where completeness matters less than speed. It also covers MAX-SAT, the optimisation variant for when a formula is unsatisfiable and the goal shifts to maximising satisfied clauses. Published on Medium, October 2020.