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.
Deriving additional Boolean clauses implied by the original Boolean formula, usually after analyzing a conflict in search. A learned Boolean clause excludes a failed combination of choices on subsequent branches without removing any satisfying assignment.
If all but one literal of a Boolean clause are false under a partial Boolean valuation, the remaining literal must be true in any extension satisfying the clause. Repeatedly make such forced assignments, remove satisfied Boolean clauses and remove false literals from the others. An empty Boolean clause proves that the current partial Boolean valuation has no satisfying extension. This is sound because every step is forced by an original or already implied Boolean clause; it is not by itself a complete SAT decision procedure.
Articles by others on the same topic
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.