|
ИСТИНА |
Войти в систему Регистрация |
ИПМех РАН |
||
О разрешающих стратегиях для резолютивных доказательствдипломная работа (Специалист)
- Научный руководитель: Боков Г.В.
- Автор: Сафонов Георгий Владимирович
- Тип: Специалист
- Организация, в которой проходила защита: МГУ имени М.В. Ломоносова
- Год защиты: 2022
- Аннотация: В дипломной работе показано, что графовые разрешающие стратегии могут быть полиномиально сведены к ограниченному классу графов, представляющих собой семейство ациклических ориентированных графов, множества нелистовых вершин которых линейно упорядочены относительной топологического порядка. Автором была исследована упорядоченная стратегия CDCL алгоритма вместе со стратегиями выбора полученного в результате обучения дизъюнкта (DECISION-L) и стратегиями выбора набора присвоений переменных (NEVER-R). Доказано, что CDCL алгоритм при использовании упорядоченной стратегии вместе с стратегиями DECISION-L и NEVER-R полиномиально эквивалентен упорядоченной резолюции. Что является усилением результата Н. Мулла, Ш. Панга и А. Разборова 2020 года, в котором CDCL алгоритм не был ограничен стратегией NEVER-R.
- Добавил в систему: Боков Григорий Владимирович