A small CNF-SAT solver implementing simple conflict driven clause learning (CDCL) and a simple branching heuristic.