Город: Санкт-Петербург Новосибирск Казань Язык: Русский English

SAT and Satisfiability Modulo Theories (R. Bruttomesso, University of Lugano)
Computer Science семинар


Что: Лекция
Когда: Суббота, 18 сентября 2010, 17:20–18:55
Где: ПОМИ РАН
Слайды: csseminar_lecture_180910.pdf

Описание

Satisfiability Modulo Theories (SMT) is the problem of deciding a quantifier-free formula modulo a background theory T. State-of-the-art SMT-Solvers are based on the DPLL(T) model, which efficiently combines a DPLL SAT-Solver, used to handle disjucntive choices, and a Theory Solver, a decision procedure for T, used to solve conjunctions of constraints. In this lecture we review the DPLL approach to SAT and extend it to DPLL(T) approach. Also we examine some useful theories, commonly used in the formal analysis of software, by sketching the main ideas behind the algorithms used to solve them.

Материалы