A SAT solver takes a Boolean expression and finds out if the variables can be replaced by true or false so that the formula evaluates to true. SAT is a problem that belongs in the NP-complete class of problems and was in fact the first ever problem proven to belong to that class. This means that there are no known algorithms that can efficiently and correctly solve all possible input instances. In practical terms, this means that it is not known how long it will take to find a solution, but many problems will be solved in a much shorter timeframe.
This limitation has not stopped it from being used to solve many complex problems in formal verification, instead using ever more efficient heuristic approaches. Within EDA, SAT solvers are used for such disparate tasks as test pattern generation, circuit delay computation, logic optimization, combinational equivalence checking, bounded model checking and functional test vector generation. The heuristics make use of some of the underlying structures typically found in digital systems.