Basically, it solves the problem of finding a setting of variables that is compatible with some set of constraints. This is NP-hard but Z3 is in practice very fast nonetheless.
A case study/glowing review from a programmer at Microsoft is here:
That actually depends on the logic being used. Some of the logics supported by Z3 are not even decidable. In fact, even solving quantifier-free bit-vector formulas is NEXPTIME-complete [0] when using a binary encoding.