Search, with the lights on.

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

Constraint satisfaction with forward checking

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

Propositional resolution refutation

Reads a CNF knowledge base, negates the query, and applies the resolution rule iteratively until it derives the empty clause that proves unsatisfiability, printing the full trace step by step. Type your own clauses or pick a bundled sample.