Search, with the lights on.

Two classical search based AI techniques implemented in Java for a UT Dallas AI course. Ported to TypeScript with interactive editors so you can feed them your own problems. Backtracking with forward checking for constraint satisfaction. Resolution refutation for propositional SAT.

Constraint satisfaction with forward checking

A backtracking search over a constraint graph using minimum remaining values, degree tie break, and least constraining value heuristics. Forward checking prunes inconsistent values from neighbor domains as the search progresses. Four bundled example problems. Paste your own variable domain and constraint files or pick from the dropdown.

Propositional resolution refutation

Reads a CNF knowledge base. Negates the final query. Applies the resolution rule iteratively to derive new clauses. Detects the empty clause as proof of unsatisfiability. Prints the proof trace step by step. Type your own clauses or pick a bundled sample.