The tutorial will start covering the basic reasoning techniques for propositional
reasoning (SAT), focussing in particular to those that are at the basis of current state
of-the-art SAT solvers. Then, we will move in order to deal with extensions of propositional
reasoning, in order to deal with preferences and quantifiers. Applications of the proposed 
formalisms (in particular in the areas of automated planning and formal verification) will 
be presented and discussed.