Using Sat solvers for synchronization issues in non-deterministic automata
arXiv:1801.05391
Abstract
We approach the problem of computing a -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.
16 pages, 4 figures