The tutorial is directed to a rather general audience in the field of Automated Reasoning, like SAT, decision procedures, reasoning in modal and description logics, planning, temporal reasoning, and also to those people interested in applications of AR techniques to formal verification. The tutorial assumes only a basic knowledge of logic and AR topics. A background on SAT is of help, but not strictly necessary.