Tutorial presentations at the twelfth international conference on principles of knowledge representation and reasoning
Leonardo de Moura, Carsten Lutz, m.c. schraefel, Bernhard Nebel · Principles of Knowledge Representation and Reasoning · 2010
Constraint satisfaction problems arise in many diverse areas including software and hardware verification, type inference, extended static checking, test-case generation, scheduling, planning, graph problems, among others. The most well-known constraint satisfaction problem is propositional satisfiability SAT. Of particular recent interest is satisfiability modulo theories (SMT), where the interpretation of some symbols is constrained by a background theory. For example, the theory of arithmetic restricts the interpretation of symbols such as: +, ≤, 0, and 1. SMT draws on the most prolific problems in the past century of symbolic logic: the decision problem, completeness and incompleteness of logical theories, and finally complexity theory. In this tutorial, I will describe a brief introduction to the theory behind SAT and SMT solvers, the main techniques, and their many applications. In particular, I will describe how these solvers are used at Microsoft.