H. Shabana, M. V. Volkov, “Using SAT solvers for synchronization issues in non-deterministic automata”, Sib. Èlektron. Mat. Izv., 2018, Volume 15,Pages <nobr>1426

This article is cited in 1 paper

Discrete mathematics and mathematical cybernetics

Using SAT solvers for synchronization issues in non-deterministic automata

H. Shabana^ab, M. V. Volkov^b

^a Faculty of Electronic Engineering, Menoufia University, Egypt
^b Institute of Natural Sciences and Mathematics, Ural Federal University, Lenina 51, 620000 Yekaterinburg, Russia

Abstract: We approach the problem of computing a $D_{3}$-synchronizing word of minimum length for a given nondeterministic automaton via its encoding as an instance of SAT and invoking a SAT solver. We also present some experimental results.

Keywords: nondeterministic automaton, synchronizing word, SAT, SAT-solver, random automaton.

UDC: 519.713.1, 510.633

MSC: 68Q45

Received January 15, 2018, published November 15, 2018

Language: English

DOI: 10.17377/semi.2018.15.117