Hanan Shabana     (Institute of Natural Sciences and Mathematics, Ural Federal University, 51 Lenin aven., Ekaterinburg, Russia, 620000; Faculty of Electronic Engineering, Menoufia University, Egypt)


We approach the problem of computing a D2-synchronizing word of minimum length for a given nondeterministic automaton via its encoding as an instance of SAT and invoking a SAT solver. In addition, we report some of the experimental results obtained when we had tested our method on randomly generated automata and certain benchmarks.


Nondeterministic automata, Synchronizing word, SAT solver

Full Text:



  1. Biere A. Yet another local search solver and lingeling and friends entering the SAT Competition 2014. In: Proceedings of SAT Competition 2014: Solver and Benchmark Descriptions. University of Helsinki, 2014. P. 39–40. URL: http://fmv.jku.at/papers/Biere-SAT-Competition-2014.pdf
  2. de Bondt M., Don H., Zantema H. Lower bounds for synchronizing word lengths in partial automata. Preprint, 2018. DOI: https://arxiv.org/abs/1801.10436
  3. Eén N., Sörensson N. An extensible SAT-solver. Lect. Notes Comput. Sci., Vol. 2919: Theory and Applications of Satisfiability Testing (SAT 2003). 2004. P. 502–518. DOI: 10.1007/978-3-540-24605-3_37
  4. Eén N., Sörensson N. The MiniSat Page. URL: http://minisat.se http://minisat.se
  5. Gomes C.P., Kautz H., Sabharwal A., Selman B. Satisfiability Solvers. Ch. 2. In: Handbook of Knowledge Representation, Elsevier, 2008. P. 89–134. DOI: 10.1016/S1574-6526(07)03002-7
  6. Güniҫen C., Erdem E., Yenigün H. Generating shortest synchronizing sequences using Answer Set Programming. In: Proceedings of Answer Set Programming and Other Computing Paradigms (ASPOCP2013). P. 117–127. https://arxiv.org/abs/1312.6146
  7. Imreh B., Steinby M. Directable nondeterministic automata. Acta Cybernetica. 1999. Vol. 14, no. 1. P. 105–115.
  8. Kisielewicz A., Kowalski J., Szyku la M. Computing the shortest reset words of synchronizing automata. J. Comb. Optim. 2015. Vol. 29, no. 1. P. 88–124. DOI: 10.1007/s10878-013-9682-0
  9. Martyugin P. Synchronization of automata with one undefined or ambiguous transition. Lect. Notes Comput. Sci., Vol. 7381: Implementation and Application of Automata (CIAA 2012). 2012. P. 278–288. DOI: 10.1007/978-3-642-31606-7_24
  10. Rystsov I.K. Polynomial complete problems in automata theory. Inf. Process. Lett. 1983. Vol. 16, no. 3. P. 147–151. DOI: 10.1016/0020-0190(83)90067-4
  11. Rystsov I.K. Asymptotic estimate of the length of a diagnostic word for a finite automaton. Cybernetics. 1980. Vol. 16, no. 1. P. 194–198. DOI: 10.1007/bf01069104
  12. Shabana H., Volkov M.V. Using Sat solvers for synchronization issues in nondeterministic automata. Siberian Electronic Math. Reports. 2018. Vol. 15. P. 1426–1442 URL: http://semr.math.nsc.ru/v15/p1426-1442.pdf
  13. Skvortsov E., Tipikin E. Experimental study of the shortest reset word of random automata. Lect. Notes Comput. Sci., Vol. 6807: Implementation and Application of Automata (CIAA 2011), 2011. P. 290–298. DOI: 10.1007/978-3-642-22256-6_27
  14. Soos M. CryptoMiniSat 2. URL: http://www.msoos.org/cryptominisat2/

DOI: http://dx.doi.org/10.15826/umj.2018.2.011

Article Metrics

Metrics Loading ...


  • There are currently no refbacks.