SAT solver

A program that determines whether a Boolean formula is satisfiable and can produce a satisfying assignment. Modern solvers often combine search with techniques that learn from conflicts.

DPLL algorithm: A recursive SAT-solving algorithm that branches on variables and propagates forced assignments. It provides the search-and-propagation framework underlying many complete solvers.
Boolean satisfiability problem: The decision problem of whether a Boolean formula has an assignment that makes it true. A SAT solver is an algorithmic tool for this decision problem.
Bounded model checking: A verification method that encodes executions up to a fixed length as a satisfiability problem. A SAT solver checks whether a bounded execution reaches an error state.
Stochastic local search: A family of randomized search methods that repeatedly modify candidate solutions to improve them. Unlike complete SAT search, these methods can find solutions quickly but generally cannot prove unsatisfiability.
Davis–Putnam algorithm: A 1960 algorithm for deciding propositional satisfiability by eliminating variables through resolution. It established an early systematic approach to SAT before the later DPLL search method.
Unit propagation: A procedure that assigns a literal when a clause has only one unassigned literal remaining. It exposes forced choices after each decision or learned clause.
Conjunctive normal form: A Boolean formula written as a conjunction of clauses, each clause being a disjunction of literals. Many solvers accept formulas in this standard clause-based representation.
Software verification: The process of establishing whether software satisfies specified correctness properties. SAT solving supports automated checks of program behavior and constraints.
Binary decision diagram: A directed acyclic graph representing a Boolean function through variable tests and shared subgraphs. Decision diagrams represent functions canonically under an ordering, while SAT solvers search for assignments.
Davis–Putnam–Logemann–Loveland algorithm: A 1962 recursive procedure for SAT based on splitting and unit propagation. Its core ideas became the foundation of practical complete SAT solving.

Linked from 16 pages