Теоретический семинар

9 апреля, пятница, 15.15, к.430

Д. Соколов (АФТУ)
Криптографическая стойкость функции Голдрейха

Функция Голдрейха - кандидат в односторонние функции. В докладе будут рассмотрены нижние оценки на время обращения функции Голдрейха при помощи подкласса DPLL алгоритмов - "пьяных" алгоритмов. Будет доказана нижняя экспоненциальная оценка на время работы любого DPLL алгоритма на невыполнимой булевой формуле, полученной по функции Голдрейха, а также показано, что после некоторого числа шагов "пьяного" алгоритма с большой вероятностью формула станет невыполнимой.
Также в докладе будет приведена явная конструкция функции Голдрейха, обеспечивающая указанные оценки.

12 марта, пятница, 15.15, к.430

В. Николаенко (АФТУ)
Перестановочные полиномы

В этом докладе будет рассказано об исследованиях перестановочных биномов над конечными полями. Будет освещен вопрос актуальности исследований в сфере криптографических протоколов. Также будет рассказано о диаграммах Юнга и других характеристиках перестановок. Будут приведены теоретические результаты для колец $Z/(2^nZ)$, рассказано о критериях перестановочности и полученных автором доклада численных и статистических результатах для оценки числа полиномов в зависимости от размера поля.

17 февраля, среда, 14.00, к.430

Д. Соколов (АФТУ)
"Элементарная" конструкция экспандеров

Доклад по статье Noga Alon, Oded Schwartz, Asaf Shapira "An Elementary Construction of Constant-Degree Expanders". В докладе будет рассмотрена простейшая на сегодняшний день конструкция алгебраических экспандеров с константной степенью, которая включает в себя лишь два подстановочных произведения. Так же будет проведен анализ параметров полученного экспандера.

19 марта, пятница, 15.15, к.430

Ю. Беляева (АФТУ)
Гипотеза о песочных часах

Доклад посвящён гипотезе о песочных часах (sandglass conjecture), предложенной в статье Rudolf Ahlswede, Gabor Simonyi "Note on the optimal structure of recovering set pairs in lattices: the sandglass conjecture". Гипотеза говорит о семействах подмножеств конечной решётки, удовлетворяющих двум ограничениям -- "восстанавливающих парах" (recovering pair) подмножеств и предлагает оценку на произведение их мощностей. Данная оценка в общем случае не доказана. В докладе будет рассмотрен частный случай гипотезы для решётки подмножеств конечного множества и доказана наилучшая известная оценка для этого случая представленная в работе Ron Holzman, Janos Korner "Cancellative pairs of families of sets". Также будет изложена идея доказательства гипотезы для решётки представляемой в виде произведения двух цепей.

26 марта, пятница, 15.15, к.430

Ф. Парт (АФТУ)
Параметризованные системы доказательств

Вопрос о равенстве классов co-NP и NP имеет естественную переформулировку в терминах систем доказательств и сложности доказательств. Аналогично, те или иные классы задач с параметром W[t] могут быть отделены от соответствующих им co-классов посредством исследования параметризованных систем доказательств и оценке снизу размера доказательств в таких системах. В докладе будет рассмотрена параметризованная версия tree-like резолюций для задачи ограниченной невыполнимости и приведена классификация (модифицированная теорема Риса) длины доказательств в этой системе для семейств параметризованных противоречий, являющихся записями для конечных моделей формулы логики первого порядка, не имеющей конечных моделей.

1 декабря, вторник, 16:00, к.430

Реализация солвера для логики первого порядка

Средства логики первого порядка в "зоне Златовласки" (Goldilocks Zone)
логического вывода достаточно выразительны, чтобы легко задать даже
сложные свойства, но при этом они достаточно просты для автоматизации.

24 ноября, вторник, 16:00, к.430

Г. Ярославцев (АФТУ)
Выполнимость в теориях (Satisfiability modulo theories)

17 ноября, вторник, 16:00, к.430

И. Монахов (АФТУ)
О верификации и управлении систем реального времени

Моделирование сложных систем, таких как встроенные системы или коммуникационные протоколы, часто требует умения выражать количественные ограничения по времени между событиями

3 ноября, вторник, 16:00, к.430

Г. Ярославцев (АФТУ)
Построение SAT-солверов и их использование

В последние годы технологии, построенные на решении задачи выполнимости булевых формул (SAT), набирают популярность. Программы для решения SAT (SAT-солверы) используются для решения комбинаторных задач, активно применяются в промышленных компаниях, занимающихся