Efficient Symmetry Breaking for SAT-Based minimum DFA inference

Ilya Zakirzyanov, Antonio Morgado, Alexey Ignatiev, Vladimir Ulyantsev, Joao Marques-Silva

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

6 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationLanguage and Automata Theory and Applications
Subtitle of host publication13th International Conference, LATA 2019 St. Petersburg, Russia, March 26–29, 2019 Proceedings
EditorsCarlos Martín-Vide, Alexander Okhotin, Dana Shapira
Place of PublicationCham Switzerland
Number of pages15
ISBN (Electronic)9783030134358
ISBN (Print)9783030134341
Publication statusPublished - 2019
Externally publishedYes
EventInternational Conference on Language and Automata Theory and Applications 2019 - St. Petersburg, Russian Federation
Duration: 26 Mar 201929 Mar 2019
Conference number: 13th

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceInternational Conference on Language and Automata Theory and Applications 2019
Abbreviated titleLATA 2019
CountryRussian Federation
CitySt. Petersburg
Internet address


  • Boolean satisfiability
  • DFA inference
  • Symmetry breaking

Cite this