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