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.
CITATION STYLE
Zakirzyanov, I., Morgado, A., Ignatiev, A., Ulyantsev, V., & Marques-Silva, J. (2019). Efficient Symmetry Breaking for SAT-Based Minimum DFA Inference. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11417 LNCS, pp. 159–173). Springer Verlag. https://doi.org/10.1007/978-3-030-13435-8_12
Mendeley helps you to discover research relevant for your work.