Efficient Symmetry Breaking for SAT-Based Minimum DFA Inference

  • Ilya ZakirzyanovEmail author
  • Antonio Morgado
  • Alexey Ignatiev
  • Vladimir Ulyantsev
  • Joao Marques-Silva
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11417)


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.


DFA inference Boolean satisfiability Symmetry breaking 


  1. 1.
    Abela, J., Coste, F., Spina, S.: Mutually compatible and incompatible merges for the search of the smallest consistent DFA. In: ICGI, pp. 28–39 (2004)CrossRefGoogle Scholar
  2. 2.
    Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality networks: a theoretical and empirical study. Constraints 16(2), 195–221 (2011)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun. 25(2), 97–116 (2012)MathSciNetzbMATHGoogle Scholar
  5. 5.
    Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)Google Scholar
  6. 6.
    Biermann, A.W., Feldman, J.A.: On the synthesis of finite-state machines from samples of their behavior. IEEE Trans. Comput. 21(6), 592–597 (1972)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Bugalho, M.M.F., Oliveira, A.L.: Inference of regular languages using state merging algorithms with search. Pattern Recognit. 38(9), 1457–1467 (2005)CrossRefGoogle Scholar
  8. 8.
    Coste, F., Nicolas, J.: Regular inference as a graph coloring problem. In: IWGI (1997)Google Scholar
  9. 9.
    Coste, F., Nicolas, J.: How considering incompatible state mergings may reduce the DFA induction search tree. In: ICGI, pp. 199–210 (1998)Google Scholar
  10. 10.
    Eén, N., Sörensson, N.: Translating Pseudo-Boolean constraints into SAT. JSAT 2(1–4), 1–26 (2006)zbMATHGoogle Scholar
  11. 11.
    Gent, I.P., Nightingale, P.: A new encoding of all different into SAT. In: Workshop on Modelling and Reformulating Constraint Satisfaction Problems, pp. 95–110 (2004)Google Scholar
  12. 12.
    Grinchtein, O., Leucker, M., Piterman, N.: Inferring network invariants automatically. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 483–497. Springer, Heidelberg (2006). Scholar
  13. 13.
    Heule, M.J.H., Verwer, S.: Exact DFA identification using SAT solvers. In: Sempere, J.M., García, P. (eds.) ICGI 2010. LNCS (LNAI), vol. 6339, pp. 66–79. Springer, Heidelberg (2010). Scholar
  14. 14.
    Heule, M., Verwer, S.: Software model synthesis using satisfiability solvers. Empir. Softw. Eng. 18(4), 825–856 (2013)CrossRefGoogle Scholar
  15. 15.
    de la Higuera, C.: A bibliographical study of grammatical inference. Pattern Recognit. 38(9), 1332–1348 (2005)CrossRefGoogle Scholar
  16. 16.
    Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation - International Edition, 2nd edn. Addison-Wesley, Boston (2003)zbMATHGoogle Scholar
  17. 17.
    Lang, K.J.: Faster algorithms for finding minimal consistent DFAs. Technical report, NEC Research Institute (1999)Google Scholar
  18. 18.
    Lang, K.J., Pearlmutter, B.A., Price, R.A.: Results of the Abbadingo one DFA learning competition and a new evidence-driven state merging algorithm. In: Honavar, V., Slutzki, G. (eds.) ICGI 1998. LNCS, vol. 1433, pp. 1–12. Springer, Heidelberg (1998). Scholar
  19. 19.
    Morgado, A., Heras, F., Liffiton, M.H., Planes, J., Marques-Silva, J.: Iterative and core-guided MaxSAT solving: a survey and assessment. Constraints 18(4), 478–534 (2013)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Neider, D.: Applications of automata learning in verification and synthesis. Ph.D. thesis, RWTH Aachen University (2014)Google Scholar
  21. 21.
    Neider, D., Jansen, N.: Regular model checking using solver technologies and automata learning. In: NFM, pp. 16–31 (2013)Google Scholar
  22. 22.
    Oliveira, A.L., Marques-Silva, J.: Efficient algorithms for the inference of minimum size DFAs. Mach. Learn. 44(1/2), 93–119 (2001)CrossRefGoogle Scholar
  23. 23.
    Sinz, C.: Towards an optimal CNF encoding of Boolean cardinality constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 827–831. Springer, Heidelberg (2005). Scholar
  24. 24.
    Trakhtenbrot, B.A., Barzdin, Y.M.: Finite Automata: Behavior and Synthesis. North-Holland Publishing Company, Amsterdam (1973)zbMATHGoogle Scholar
  25. 25.
    Ulyantsev, V., Tsarev, F.: Extended finite-state machine induction using SAT-solver. In: ICMLA, pp. 346–349 (2011)Google Scholar
  26. 26.
    Ulyantsev, V., Zakirzyanov, I., Shalyto, A.: BFS-based symmetry breaking predicates for DFA identification. In: Dediu, A.-H., Formenti, E., Martín-Vide, C., Truthe, B. (eds.) LATA 2015. LNCS, vol. 8977, pp. 611–622. Springer, Cham (2015). Scholar
  27. 27.
    Verwer, S., Hammerschmidt, C.A.: flexfringe: a passive automaton learning package. In: ICSME, pp. 638–642 (2017)Google Scholar
  28. 28.
    Walkinshaw, N., Lambeau, B., Damas, C., Bogdanov, K., Dupont, P.: STAMINA: a competition to encourage the development and assessment of software model inference techniques. Empir. Softw. Eng. 18(4), 791–824 (2013)CrossRefGoogle Scholar
  29. 29.
    Wieman, R., Aniche, M.F., Lobbezoo, W., Verwer, S., van Deursen, A.: An experience report on applying passive learning in a large-scale payment company. In: ICSME, pp. 564–573 (2017)Google Scholar
  30. 30.
    Zakirzyanov, I., Shalyto, A., Ulyantsev, V.: Finding all minimum-size DFA consistent with given examples: SAT-based approach. In: Cerone, A., Roveri, M. (eds.) SEFM 2017. LNCS, vol. 10729, pp. 117–131. Springer, Cham (2018). Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Ilya Zakirzyanov
    • 1
    • 2
    Email author
  • Antonio Morgado
    • 3
  • Alexey Ignatiev
    • 3
    • 4
  • Vladimir Ulyantsev
    • 1
  • Joao Marques-Silva
    • 3
  1. 1.ITMO UniversitySt. PetersburgRussia
  2. 2.JetBrains ResearchSt. PetersburgRussia
  3. 3.Faculty of ScienceUniversity of LisbonLisbonPortugal
  4. 4.ISDCT SB RASIrkutskRussia

Personalised recommendations