Formal Methods

SMT solver has some common looks with SAT solver -- he also handles satisfyability in a really similar way

He is younger than SAT solver and only around since decision procedures involving more complex datatypes like real numbers or arrays were available

His wide shoulders symbolize strength to handle also industrial problems well

SMT solver wears sunglasses since his character is much more complicated than revealed from the first look -- many decision procedures of the underlying theories are quite complex