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:



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

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

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

Eén N., Sörensson N. The MiniSat Page. URL: http://minisat.se http://minisat.se

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

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

Imreh B., Steinby M. Directable nondeterministic automata. Acta Cybernetica. 1999. Vol. 14, no. 1. P. 105–115.

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

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

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

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

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

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

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.