ssats Program to determine whether a given Boolean formula, represented in Conjunctive Normal Form, can be satisfied. DPLL (Davis-Putnam-Logemann-Loveland) Algorithm Unit Propagation Pure Literal Elimination Recursive Splitting