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.
A SAT solver, or satisfiability solver, is a computational tool used to determine the satisfiability of propositional logic formulas. More specifically, it assesses whether there exists an assignment of truth values (true or false) to the variables of a given boolean formula such that the entire formula evaluates to true.
New to topics? Read the docs here!