SAT solving
Boolean satisfiability
Abbreviated SAT
The problem of deciding whether a Boolean formula has a satisfying assignment.
Definition
Boolean satisfiability
Boolean satisfiability (SAT) asks whether any assignment makes a Boolean formula true.
SAT is a basic decision problem in computer science. Modern solvers can decide formulas with millions of literals by combining propagation, decisions, conflict analysis, and learned clauses.
01
Example
The formula (a or b) and (not a or b) is sat because b = true satisfies both clauses.
02
Important distinction
SAT variables are Boolean. Arithmetic structure must be encoded into Boolean constraints or handled by an SMT solver.
After reading this article, you should be able to
- Define SAT in the sense used on this site.
- State a SAT problem and interpret sat, unsat, and unknown without confusing them.