Laboratory of Mathematical Logic at PDMI

Пятница, 14 марта, комната 106. Начало в 16:00.

Докладчик: С. Николенко, А. Сироткин.

Тема: Автоматические доказательства верхних оценок для DPLL-подобных алгоритмов.

Abstract

DPLL-подобные алгоритмы широко используются для доказательства верхних экспоненциальных (но меньших, чем 2^{длина входа}) оценок времени решения задачи пропозициональной выполнимости (SAT). Эти доказательства чаще всего представляют собой элементарные комбинаторные рассуждения. Будет рассказано о попытках авторов доклада автоматизировать эти доказательства.