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

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 )

Том: 11417

Номер:

Год: 2019

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

Издательство:

Местоположение издательства:

URL:

Проекты:

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: Нет

Публикация в печати: 0