SAT/SMT solving is a general technique for automatically finding solutions for a wide range of problems. In this talk some basics of the underlying techniques are presented. First we focus on SAT = satisfiability of pure propositional formulas. Next we see how the same techniques can be extended to SMT = satisfiability modulo theories, in particular for the theory of linear inequalities. That is, the formulas are not only composed from Boolean variables and propositional operations, but also from linear inequalities over numbers.