Its a nice and short introduction to SAT and especially SMT with a real world example written in SMTLIB. If anybody is interested or has any questions, let me know. We are planning to post more about SAT and SMT as they are part of our core technology.