SAT solver
= SAT solver
{c}
An <algorithm> or software system that decides whether a <Boolean formula> has a <satisfying assignment>, usually returning one when it exists. <Unit propagation> and <clause learning> are important mechanisms in modern <SAT solvers>. A reduction must be correct and its representation costs counted before the performance of the downstream <SAT solver> is relevant.