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