Search, with the lights on.

Backtracking with forward checking for constraint satisfaction. Resolution refutation for propositional SAT. Java solvers ported to TypeScript with editors for your own problems and a visualizer that traces the search.