Using Sat solvers for synchronization issues in non-deterministic automata

Hanan Shabana, Mikhail V. Volkov

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…