SAT solver
Beginner
A program that solves giant logic puzzles. It finds a way to make every condition true, or proves there is no way.
Novice
A program that, given a logic formula, either finds values for its variables that make the formula true or proves that no such values exist. Many formal tools work by turning a question about the design into such a formula.
Expert
Modern solvers learn a new clause from every dead end (conflict-driven clause learning) and can be called again and again with small changes (incremental solving). They power BMC, k-induction, IC3, equivalence checking and stimulus generation. SMT solvers extend SAT with arithmetic on bit-vectors and other theories.
Explained in Verification (Design Flow).
See also: BDD (binary decision diagram), Bounded model checking (BMC).