Например, Бобцов

Эмпирическая оценка производительности программных средств решения задачи SAT для синтеза ДКА

Сборник тезисов
Конференция:V Всероссийский конгресс молодых ученых
Раздел:Информационные и интеллектуальные системы и технологии
Рубрика:Технологии программирования, искусственный интеллект, биоинформатика
Год:2016

Эмпирическая оценка производительности программных средств решения задачи SAT для синтеза ДКА

УДК:004.832.2

Аннотация

NP-полная задача построения детерминированного конечного автомата (ДКА) по заданным примерам поведения – одна из наиболее изученных задач в области грамматического вывода. Раннее было показано, что она может быть эффективно сведена к задаче выполнимости булевой формулы (Boolean satisfiability problem, SAT). Позднее в совместной работе автора с В. Ульянцевым и А. Шалыто была представлена модификация данного подхода, позволяющая уменьшить пространство поиска решения задачи SAT при решении задачи синтеза ДКА. Данная модификация основана на нумерации состояний искомого автомата в порядке обхода в ширину. Разработанная модификация позволила значительно улучшить время работы исходного алгоритма. Так как программные средства решения задачи о выполнимости активно развиваются, то производительность данного алгоритма, основанного на сведении, будет улучшаться само по себе, без новых модификаций, что показывает целесообразность выбора конкретного программного средства, решающего данную задачу наилучшим образом. В данной работе проводится эмпирическая оценка производительности программных средств решения задачи SAT для синтеза ДКА по известным примерам поведения.

Материалы конференций