Страница публикации

Efficient Symmetry Breaking for SAT-Based Minimum DFA Inference

Тип публикации: Статья в журнале

Тип материала: Текст

Авторы: Zakirzyanov I., Morgado A., Ignatiev A., Ulyantsev V., Marques-Silva J.

Журнал: Lecture Notes in Computer Science: 13th Intern. Conf. on Language and Automata Theory and Applications (LATA 2019, March 26-29 2019, St. Petersburg )

Язык публикации: english

Серия книг: Lecture Notes in Computer Science

Том: 11417

Номера страниц: 159-173

Количество страниц: 15

Год публикации: 2019

Отчетный год: 2019

DOI: 10.1007/978-3-030-13435-8_12

Аннотация: Inference of deterministic finite automata (DFA) finds a wide range of important practical applications. In recent years, the use of SAT and SMT solvers for the minimum size DFA inference problem (MinDFA) enabled significant performance improvements. Nevertheless, there are many problems that are simply too difficult to solve to optimality with existing technologies. One fundamental difficulty of the MinDFA problem is the size of the search space. Moreover, another fundamental drawback of these approaches is the encoding size. This paper develops novel compact encodings for Symmetry Breaking of SAT-based approaches to MinDFA. The proposed encodings are shown to perform comparably in practice with the most efficient, but also significantly larger, symmetry breaking encodings.

Индексируется WOS: Нет

Индексируется Scopus: Нет

Индексируется УБС: Нет

Индексируется РИНЦ: Да

Индексируется ВАК: Нет

Индексируется CORE: Нет