Заглавная страница

Материал из Кафедра математической кибернетики
Версия от 16:38, 8 февраля 2017; PodymovVV (обсуждение | вклад)

(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)
Перейти к: навигация, поиск

Кафедра математической кибернетики, лаборатория дискретных управляющих систем и их приложений

Официальный сайт кафедры математической кибернетики и лаборатории дискретных управляющих систем факультета ВМК МГУ имени М.В. Ломоносова.

Объявления

18 мая Вниманию студентов 318, 518/1, 518/2 групп! Защита курсовых работ состоится 26 мая (в пятницу) начало в 11:30, ауд. 504,505. Требования к оформлению работы вывешены на доске объявлений кафедры. Образец титульного листа дипломной работы.
5 мая Вниманию студентов 618/1 и 618/2 групп! Пересдача предзащиты (отчете по преддипломной практике) состоится 10 мая (в пятницу) с 15 ч 00 мин до 16 ч 30 мин, ауд. 504.
3 мая Вниманию студентов 418, 618/1 и 618/2 групп! Пересдача предзащиты (отчете по преддипломной практике) состоится 5 мая (в пятницу) с 16 ч 30 мин до 19 ч, ауд. 504. Первыми будут выступать студенты 418 группы.
21 апреля Вниманию студентов 618/1 и 618/2 групп! Появились сведения о предзащите (отчете по преддипломной практике). Предзащита состоится 3 мая (в среду) с 16 ч 30 мин до 18 ч: 618/1 группа - в ауд. 503; 618/2 группа - в ауд. 504.
21 апреля Вниманию студентов 418 группы! Появились сведения о предзащите (отчете по преддипломной практике). Предзащита состоится 3 мая (в среду) с 15 ч до 16 ч 20 мин в ауд. 505.
12 апреля В среду, 12 апреля в 17-00 (обратите внимание на время начала семинара!)

состоится доклад

Vijay Ganesh (University of Waterloo) "On The Unreasonable Effectiveness of Boolean SAT Solvers".

Abstract:

Modern conflict-driven clause-learning (CDCL) Boolean SAT solvers routinely solve very large industrial SAT instances in relatively short periods of time. This phenomenon has stumped both theoreticians and practitioners since Boolean satisfiability is an NP-complete problem widely believed to be intractable. It is clear that these solvers somehow exploit the structure of real-world instances. However, to-date there have been few results that precisely characterize this structure or shed any light on why these SAT solvers are so efficient.

In this talk, I will present results that provide a deeper empirical understanding of why CDCL SAT solvers are so efficient, which may eventually lead to a complexity-theoretic result. Our results can be divided into two parts. First, I will talk about structural parameters that can characterize industrial instances and shed light on why they are easier to solve even though they may contain millions of variables compared to small crafted instances with hundreds of variables. Second, I will talk about internals of CDCL SAT solvers, and describe why they are particularly suited to solve industrial instances.


архив объявлений

Доклады на спецсеминарах

Дискретная математика и математическая кибернетика
Дискретные функции и сложность алгоритмов
Дискретный анализ
Теория управляющих систем и математические модели СБИС и Некоторые вопросы теории управляющих систем
21 апреля 2017 г. ауд. 507 Представление магистерских диссертаций, выполненных студентами 6 курса под руководством доцента Романова Д.С.


Сложность решения дискретных задач
Теоретические проблемы программирования
7 апреля 2017 г. Проверка эквивалентности программ с неинтерпретируемыми функциями и целочисленной арифметикой.

Доклад по статье N.P. Lopes, J. Monteiro "Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic"

Доказательство эквивалентности программ имеет несколько важных приложений, в таких отраслях, как алгоритмы распознавания, регрессионное тестирование, тестирование сделанных компилятором оптимизаций и проверка утечек потоков информации. Несмотря на то что данная тема обладает важными приложениями, наука в проверки программ на эквивалентность не достигла серьёзных успехов за последние десятилетие в виду сложности этой задачи. В рассматриваемой статье предложен первая полуразрешающая процедура для автоматической проверки частичной эквивалентности двух программ, использующих неинтерпретируемые функции и работающих над целочисленной арифметикой (UF + IA). Предлагаемый алгоритм применим, в частности, к программам с вложенными циклами. Вначале проводится преобразование неинтерпретируемых функций (UF) в целочисленные полиномы, которые позволяют точно суммировать циклы с вхождениями UF, использующих рекурсию. Затем алгоритм проверки на эквивалентность переходит к свободным от циклов программам, оперирующих только целыми числами.

Е.М. Винарский, В.В. Подымов



Информация

История

Сотрудники

Лекционные курсы

Спецкурсы

Спецсеминары

Семинары

Учебный план

Расписание

Магистерские программы

Научная работа

Информация для 2-го курса

Конференции

События

Фотографии