SAT Solving

Algorithms, data structures and procedures for determining whether a propositional Boolean formula (typically in CNF) is satisfiable, and for producing a satisfying assignment when one exists; modern SAT solving includes DPLL, CDCL, heuristics, clause learning, restarts and preprocessing.