Tutorial Presentations at the Twelfth International Conference on Principles of Knowledge Representation and Reasoning

摘要

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 proposi-tional 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.