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

2 Citations (Scopus)

Abstract

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
PublisherSpringer
Pages159-173
Number of pages15
ISBN (Electronic)9783030134358
ISBN (Print)9783030134341
DOIs
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
https://lata2019.irdta.eu/

Publication series

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

Conference

ConferenceInternational Conference on Language and Automata Theory and Applications 2019
Abbreviated titleLATA 2019
CountryRussian Federation
CitySt. Petersburg
Period26/03/1929/03/19
Internet address

Keywords

  • Boolean satisfiability
  • DFA inference
  • Symmetry breaking

Cite this

Zakirzyanov, I., Morgado, A., Ignatiev, A., Ulyantsev, V., & Marques-Silva, J. (2019). Efficient Symmetry Breaking for SAT-Based minimum DFA inference. In C. Martín-Vide, A. Okhotin, & D. Shapira (Eds.), Language and Automata Theory and Applications: 13th International Conference, LATA 2019 St. Petersburg, Russia, March 26–29, 2019 Proceedings (pp. 159-173). (Lecture Notes in Computer Science ; Vol. 11417 ). Cham Switzerland : Springer. https://doi.org/10.1007/978-3-030-13435-8_12
Zakirzyanov, Ilya ; Morgado, Antonio ; Ignatiev, Alexey ; Ulyantsev, Vladimir ; Marques-Silva, Joao. / Efficient Symmetry Breaking for SAT-Based minimum DFA inference. Language and Automata Theory and Applications: 13th International Conference, LATA 2019 St. Petersburg, Russia, March 26–29, 2019 Proceedings. editor / Carlos Martín-Vide ; Alexander Okhotin ; Dana Shapira. Cham Switzerland : Springer, 2019. pp. 159-173 (Lecture Notes in Computer Science ).
@inproceedings{584c41407bdb41aa9cbb50b4b6106be0,
title = "Efficient Symmetry Breaking for SAT-Based minimum DFA inference",
abstract = "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.",
keywords = "Boolean satisfiability, DFA inference, Symmetry breaking",
author = "Ilya Zakirzyanov and Antonio Morgado and Alexey Ignatiev and Vladimir Ulyantsev and Joao Marques-Silva",
year = "2019",
doi = "10.1007/978-3-030-13435-8_12",
language = "English",
isbn = "9783030134341",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "159--173",
editor = "Carlos Mart{\'i}n-Vide and Alexander Okhotin and Dana Shapira",
booktitle = "Language and Automata Theory and Applications",

}

Zakirzyanov, I, Morgado, A, Ignatiev, A, Ulyantsev, V & Marques-Silva, J 2019, Efficient Symmetry Breaking for SAT-Based minimum DFA inference. in C Martín-Vide, A Okhotin & D Shapira (eds), Language and Automata Theory and Applications: 13th International Conference, LATA 2019 St. Petersburg, Russia, March 26–29, 2019 Proceedings. Lecture Notes in Computer Science , vol. 11417 , Springer, Cham Switzerland , pp. 159-173, International Conference on Language and Automata Theory and Applications 2019, St. Petersburg, Russian Federation, 26/03/19. https://doi.org/10.1007/978-3-030-13435-8_12

Efficient Symmetry Breaking for SAT-Based minimum DFA inference. / Zakirzyanov, Ilya; Morgado, Antonio; Ignatiev, Alexey; Ulyantsev, Vladimir; Marques-Silva, Joao.

Language and Automata Theory and Applications: 13th International Conference, LATA 2019 St. Petersburg, Russia, March 26–29, 2019 Proceedings. ed. / Carlos Martín-Vide; Alexander Okhotin; Dana Shapira. Cham Switzerland : Springer, 2019. p. 159-173 (Lecture Notes in Computer Science ; Vol. 11417 ).

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

TY - GEN

T1 - Efficient Symmetry Breaking for SAT-Based minimum DFA inference

AU - Zakirzyanov, Ilya

AU - Morgado, Antonio

AU - Ignatiev, Alexey

AU - Ulyantsev, Vladimir

AU - Marques-Silva, Joao

PY - 2019

Y1 - 2019

N2 - 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.

AB - 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.

KW - Boolean satisfiability

KW - DFA inference

KW - Symmetry breaking

UR - http://www.scopus.com/inward/record.url?scp=85064036420&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-13435-8_12

DO - 10.1007/978-3-030-13435-8_12

M3 - Conference Paper

SN - 9783030134341

T3 - Lecture Notes in Computer Science

SP - 159

EP - 173

BT - Language and Automata Theory and Applications

A2 - Martín-Vide, Carlos

A2 - Okhotin, Alexander

A2 - Shapira, Dana

PB - Springer

CY - Cham Switzerland

ER -

Zakirzyanov I, Morgado A, Ignatiev A, Ulyantsev V, Marques-Silva J. Efficient Symmetry Breaking for SAT-Based minimum DFA inference. In Martín-Vide C, Okhotin A, Shapira D, editors, Language and Automata Theory and Applications: 13th International Conference, LATA 2019 St. Petersburg, Russia, March 26–29, 2019 Proceedings. Cham Switzerland : Springer. 2019. p. 159-173. (Lecture Notes in Computer Science ). https://doi.org/10.1007/978-3-030-13435-8_12